1,721,304 research outputs found
APPROXIMATING BEPPO LEVI’S PRINCIPIO DI APPROSSIMAZIONE
Full text linkWe try to recast in modern terms a choice principle conceived by Beppo Levi, who called it the Approximation Principle (AP). Up to now, there was almost no discussion about Levi’s contribution, due to the quite obscure formulation of AP the author has chosen. After briefly reviewing the historical and philosophical surroundings of Levi’s proposal, we undertake our own attempt at interpreting AP. The idea underlying the principle, as well as the supposed faithfulness of our version to Levi’s original intention, are then discussed. Finally, an application of AP to a property of metric spaces is presented, with the aim of showing how AP may work in contexts where other forms of choice are commonly at use
On Scott’s semantics for many-valued logic
No full textThe semantics in ordered abelian groups Scott proposed for Łukasiewicz’s many-valued logic fails to be sound for one direction of one of the rules Scott gave for implication. We show this by a counterexample Urquhart has used to justify that in his own semantics, every formula has to have a least point at which it is valid. While this condition would make Scott’s semantics sound, it would cause a problem with its completeness. The question arises whether one can still amend Scott’s semantics so as to make it both sound and complete or better stick to Urquhart’s semantics anyway
Reifying dynamical algebra: maximal ideals in countable rings, constructively
No full textThe existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as “implies 0 = 1”) we
show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). By a
functional recursive definition we obtain a maximal ideal in the sense that the quotient ring is a residue field (every noninvertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). Krull’s lemma for the related notion of prime ideal follows by passing to rings of fractions. By employing a construction variant of set-theoretic forcing due to Joyal and Tierney, we expand our treatment to arbitrary rings and establish a connection with dynamical algebra: We recover the dynamical approach to maximal ideals as a parametrized version of the celebrated double negation translation. This connection allows us to give formal a priori criteria elucidating the scope of the dynamical method. Along the way we do a case study for proofs in algebra with minimal logic, and generalize the construction to arbitrary inconsistency predicates. A partial Agda formalization is available at an accompanying repository
An iterative constructive Hilbert basis theorem
No full textA sequential characterisation of Noetherian carries over in constructive algebra from a commutative ring to the univariate polynomial ring; coherence of the base ring is only needed for the multivariate case
Well quasi-orders, better quasi-orders, and monomial ideals
No full textBesides a self-contained introduction into well quasi-orders and better quasi-orders, the focus is on how these concepts lead in a neat and quick way to some well-known facts regarding monomials and monomial ideals of a polynomial ring over a field. Not uninteresting connections emerge, such as a direct path to Dickson’s lemma for monomial ideals from Higman’s theorem for monoids of terms in the vein of Hilbert’s basis theorem in iterative form
CONSERVATION AS TRANSLATION
No full textGlivenko's theorem says that classical provability of a propositional formula entails intuitionistic provability of the double negation of that formula. This stood right at the beginning of the success story of negative translations, indeed mainly designed for converting classically derivable formulae into intuitionistically derivable ones. We now generalise this approach: simultaneously from double negation to an arbitrary nucleus; from provability in a calculus to an inductively generated abstract consequence relation; and from propositional logic to any set of objects whatsoever. In particular, we give sharp criteria for the generalisation of classical logic to be a conservative extension of the one of intuitionistic logic with double negation
The basic Zariski topology
Full text linkWe present the Zariski spectrum as an inductively generated basic topology à la Martin-Löf and Sambin. Since we can thus get by without considering powers and radicals, this simplifies the presentation as a formal topology initiated by Sigstam. Our treatment includes closed subspaces and basic opens: that is, arbitrary quotients and singleton localisations. All the effective objects under consideration are introduced by means of inductive
definitions. The notions of spatiality and reducibility are characterized for the class of Zariski formal topologies, and their nonconstructive content is pointed out: while spatiality implies classical logic, reducibility corresponds to a fragment of the Axiom of Choice in the form of Russell’s Multiplicative Axiom
ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION
No full textCompleteness and other forms of Zorn’s Lemma are sometimes invoked for semantic proofs of conservation in relatively elementary mathematical contexts in which the corresponding syntactical conservation would suffice. We now show how a fairly general syntactical conservation theorem that covers plenty of the semantic approaches follows from an utmost versatile criterion for conservation given by Scott in 1974. To this end we work with multi-conclusion entailment relations as extending single- conclusion entailment relations. In a nutshell, the additional axioms with disjunctions in positive position can be eliminated by reducing them to the corresponding disjunction elimi- nation rules, which in turn prove admissible in all known mathematical instances. In deduction terms this means to fold up branchings of proof trees by way of properties of the relevant mathematical structures. Applications include the syntactical counterparts of the theorems or lemmas known under the names of Artin–Schreier, Krull–Lindenbaum, and Szpilrajn. Related work has been done before on individual instances, e.g., in locale theory, dynamical algebra, formal topology and proof analysis
`Kronecker's density theorem and irrational numbers in constructive reverse mathematics'
No full textTo prove Kronecker’s density theorem in Bishop-style constructive analysis one needs to define an irrational number as a real number that is bounded away from each rational number. In fact, once one understands “irrational” merely as “not rational”, then the theorem becomes equivalent to Markov’s principle. To see this we undertake a systematic classification, in the vein of constructive reverse mathematics, of logical combinations of “rational” and “irrational” as predicates of real numbers
A General Glivenko–Gödel Theorem for Nuclei
No full textGlivenko’s theorem says that, in propositional logic, classical provability of a formula entails intuitionistic provability of double negation of that formula. We generalise Glivenko’s theorem from double negation to an arbitrary nucleus, from provability in a calculus to an inductively generated abstract consequence relation, and from propositional logic to any set of objects whatsoever. The resulting conservation theorem comes with precise criteria for its validity, which allow us to instantly include Gödel’s counterpart for first-order predicate logic of Glivenko’s theorem. The open nucleus gives us a form of the deduction theorem for positive logic, and the closed nucleus prompts a variant of the reduction from intuitionistic to minimal logic going back to Johansson
- …
