VON NEUMANN’S CONSISTENCY PROOF

AbstractWe consider the consistency proof for a weak fragment of arithmetic published by von Neumann in 1927. This proof is rather neglected in the literature on the history of consistency proofs in the Hilbert school. We explain von Neumann’s proof and argue that it fills a gap between Hilbert’s consistency proofs for the so-called elementary calculus of free variables with a successor and a predecessor function and Ackermann’s consistency proof for second-order primitive recursive arithmetic. In particular, von Neumann’s proof is the first rigorous proof of the consistency of an axiomatization of the first-order theory of a successor function.

Download Full-text

More on definable sets of p-adic numbers

Journal of Symbolic Logic ◽

10.2307/2274581 ◽

1988 ◽

Vol 53 (3) ◽

pp. 912-920 ◽

Cited By ~ 2

Author(s):

Philip Scowcroft

Keyword(s):

Cross Section ◽

Quantifier Elimination ◽

Order Theory ◽

Model Completeness ◽

First Order ◽

First Order Theory ◽

Ordered Fields ◽

Definable Sets ◽

The Cross ◽

Primitive Recursive

To eliminate quantifiers in the first-order theory of the p-adic field Qp, Ax and Kochen use a language containing a symbol for a cross-section map n → pn from the value group Z into Qp [1, pp. 48–49]. The primitive-recursive quantifier eliminations given by Cohen [2] and Weispfenning [10] also apply to a language mentioning the cross-section, but none of these authors seems entirely happy with his results. As Cohen says, “all the operations… introduced for our simple functions seem natural, with the possible exception of the map n → pn” [2, p. 146]. So all three authors show that various consequences of quantifier elimination—completeness, decidability, model-completeness—also hold for a theory of Qp not employing the cross-section [1, p. 453; 2, p. 146; 10, §4]. Macintyre directs a more specific complaint against the cross-section [5, p. 605]. Elementary formulae which use it can define infinite discrete subsets of Qp; yet infinite discrete subsets of R are not definable in the language of ordered fields, and so certain analogies between Qp and R suggested by previous model-theoretic work seem to break down.To avoid this problem, Macintyre gives up the cross-section and eliminates quantifiers in a theory of Qp written just in the usual language of fields supplemented by a predicate V for Qp's valuation ring and by predicates Pn for the sets of nth powers in Qp (for all n ≥ 2).

Download Full-text

Analysis without actual infinity

Journal of Symbolic Logic ◽

10.2307/2273760 ◽

1981 ◽

Vol 46 (3) ◽

pp. 625-633 ◽

Cited By ~ 20

Author(s):

Jan Mycielski

Keyword(s):

Natural Science ◽

Order Theory ◽

Finite Part ◽

Consistency Proof ◽

Actual Infinity ◽

First Order ◽

Finite Models ◽

First Order Theory ◽

Potential Applications

AbstractWe define a first-order theory FIN which has a recursive axiomatization and has the following two properties. Each finite part of FIN has finite models. FIN is strong enough to develop that part of mathematics which is used or has potential applications in natural science. This work can also be regarded as a consistency proof of this hitherto informal part of mathematics. In FIN one can count every set; this permits one to prove some new probabilistic theorems.

Download Full-text

A lattice of interpretability types of theories

Journal of Symbolic Logic ◽

10.2307/2272134 ◽

1977 ◽

Vol 42 (2) ◽

pp. 297-305 ◽

Cited By ~ 10

Author(s):

Jan Mycielski

Keyword(s):

Order Theory ◽

Partial Ordering ◽

First Order ◽

First Order Theory ◽

Relative Consistency ◽

Infinite Distributivity ◽

Closed Fields ◽

Image Position ◽

Interpretability Type ◽

Consistency Proofs

We consider first-order logic only. A theory S will be called locally interpretable in a theory T if every theorem of S is interpretable in T. If S is locally interpretable in T and T is consistent then S is consistent. Most known relative consistency proofs can be viewed as local interpretations. The classic examples are the cartesian interpretation of the elementary theorems of Euclidean n-dimensional geometry into the first-order theory of real closed fields, the interpretation of the arithmetic of integers (rational numbers) into the arithmetic of positive integers, the interpretation of ZF + (V = L) into ZF, the interpretation of analysis into ZFC, relative consistency proofs by forcing, etc. Those interpretations are global. Under fairly general conditions local interpretability implies global interpretability; see Remarks (7), (8), and (9) below.We define the type (interpretability type) of a theory S to be the class of all theories T such that S is locally interpretable in T and vice versa. There happen to be such types and they are partially ordered by the relation of local interpretability. This partial ordering is of lattice type and has the following form:The lattice is distributive and complete and satisfies the infinite distributivity law of Brouwerian lattices:We do not know if the dual lawis true. We will show that the lattice is algebraic and that its compact elements form a sublattice and are precisely the types of finitely axiomatizable theories, and several other facts.

Download Full-text

The Consistency of Arithmetic

The Australasian Journal of Logic ◽

10.26686/ajl.v18i5.6906 ◽

2021 ◽

Vol 18 (5) ◽

pp. 289-379

Author(s):

Robert Meyer

Keyword(s):

Elementary Proof ◽

Order Theory ◽

Transfinite Induction ◽

Consistency Proof ◽

First Order ◽

First Order Theory ◽

Formal Program ◽

The One ◽

Range Of Variation ◽

Made In

This paper offers an elementary proof that formal arithmetic is consistent. The system that will be proved consistent is a first-order theory R♯, based as usual on the Peano postulates and the recursion equations for + and ×. However, the reasoning will apply to any axiomatizable extension of R♯ got by adding classical arithmetical truths. Moreover, it will continue to apply through a large range of variation of the un- derlying logic of R♯, while on a simple and straightforward translation, the classical first-order theory P♯ of Peano arithmetic turns out to be an exact subsystem of R♯. Since the reasoning is elementary, it is formalizable within R♯ itself; i.e., we can actually demonstrate within R♯ (or within P♯, if we care) a statement that, in a natural fashion, asserts the consistency of R♯ itself. The reader is unlikely to have missed the significance of the remarks just made. In plain English, this paper repeals Goedel’s famous second theorem. (That’s the one that asserts that sufficiently strong systems are inadequate to demonstrate their own consistency.) That theorem (or at least the significance usually claimed for it) was a mis- take—a subtle and understandable mistake, perhaps, but a mistake nonetheless. Accordingly, this paper reinstates the formal program which is often taken to have been blasted away by Goedel’s theorems— namely, the Hilbert program of demonstrating, by methods that everybody can recognize as effective and finitary, that intuitive mathematics is reliable. Indeed, the present consistency proof for arithmetic will be recognized as correct by anyone who can count to 3. (So much, indeed, for the claim that the reliability of arithmetic rests on transfinite induction up to ε0, and for the incredible mythology that underlies it.)

Download Full-text

Decidability and undecidability of theories with a predicate for the primes

Journal of Symbolic Logic ◽

10.2307/2275227 ◽

1993 ◽

Vol 58 (2) ◽

pp. 672-687 ◽

Cited By ~ 7

Author(s):

P. T. Bateman ◽

C. G. Jockusch ◽

A. R. Woods

Keyword(s):

General Result ◽

Order Theory ◽

Second Order ◽

The Other ◽

Linear Case ◽

Natural Numbers ◽

Successor Function ◽

First Order ◽

First Order Theory

AbstractIt is shown, assuming the linear case of Schinzel's Hypothesis, that the first-order theory of the structure 〈ω; +, P〉, where P is the set of primes, is undecidable and, in fact, that multiplication of natural numbers is first-order definable in this structure. In the other direction, it is shown, from the same hypothesis, that the monadic second-order theory of 〈ω S, P〉 is decidable, where S is the successor function. The latter result is proved using a general result of A. L. Semënov on decidability of monadic theories, and a proof of Semënov's result is presented.

Download Full-text