Constructivity04

◄ Chapter 3 ◄ Index Chapter 5 ►

Beyond Gödel

Simply consistent constructive systems of first order Peano’s Arithmetic that do not yield undecidable propositions by Gödel’s reasoning

(A compiled copy of Chapters 1 to 6 can be downloaded as a .pdf file from http://arxiv.org/abs/math/0201059.)

Chapter 4. Are there stronger omega-constructive systems of first order Arithmetic?

Contents

4.0. Introduction

4.1. An omega-constructive first order Arithmetic

4.2. omega-PA

4.3. Some features of omega-PA

4.4. The difference between PA and omega-PA

4.5. omega₁-PA

4.6. The conflict with model theory

4.7. Introducing the omega-Specification rule of inference

4.8. A yet stronger omega-calculus : omega₂-PA

4.9. The Generalisation rule of inference holds for omega₂-PA

4.10. We cannot infer Gödel’s conclusions from his reasoning in omega₂-PA

4.11. Does Gödel’s reasoning hold even when his conclusions do not?

4.0. Introduction

In this fourth section we begin by briefly reviewing the main arguments of the earlier sections.

We then consider whether, and how, we may strengthen omega-PA.

We use Parikh’s form of the Kreisel-Parson’s conjecture to constructively qualify quantification. This now allows a constructive formal system to refer to selective properties of non-constructive elements under interpretation

We finally construct a strong omega₂-PA, and show that the axioms, interpretations and models of strong omega₂-PA, and the axioms, interpretations and models of PA, are identical, but have significantly different consequences.

We conclude that the formal undecidability of Arithmetical propositions that are true under interpretation is a characteristic not of any relations that are Platonistically inherent in any Arithmetic of the natural numbers, but of the particular formalisation chosen to represent the Arithmetic.

4.1. An omega-constructive first order Arithmetic

We argued in §1 and §2 that an omega-constructive system of Arithmetic is inconsistent with standard first order predicate calculus PA with strong Generalisation.

4.2. omega-PA

In §3 we defined omega-PA, where we eliminated the closed Induction axiom schema A(10) of PA, and replaced the strong Generalisation rule of inference I(ii) of PA by the weaker omega-Constructivity rule of inference I(iii).

4.3. Some features of omega-PA

We then argued that every model of PA is a model of omega-PA.

We argued further that every primitive recursive function cannot be strongly represented in omega-PA.

We also argued that omega-PA is intuitively a more natural and constructive formal system of Peano’s Arithmetic than PA.

We argued that Gödel’s reasoning does not establish the existence of undecidable propositions in omega-PA, which are true under interpretation, in a constructive and intuitionistically unobjectionable way, as he intended (Gödel p189).

4.4. The difference between PA and omega-PA

We argued in §3.15 that the essential difference between PA and omega-PA lay in their respective meta-assertions about the nature and scope of the valid consequences amongst the elements of the domain of each system under interpretation.

We then posed the question: Can we strengthen omega-PA so that every model of a stronger omega-PA is a model of PA?

4.5. omega₁-PA

If we now add the closed Induction axiom schema A(10) to omega-PA, we arrive at a stronger, yet still constructive, formal system of Peano Arithmetic, omega₁-PA.

omega₁-PA is thus axioms A(1) to A(11) of first order Arithmetic, as specified in §3.4, added to a first order predicate calculus A(i) to A(iii), as specified in §3.4, along with the Modus Ponens rule of inference I(i) and the omega-Constructivity rule of inference I(iii).

Thus PA and omega₁-PA have identical axioms, with identical interpretations and models. Prima facie, though, omega₁-PA is an intuitively more natural and constructive formalisation of Peano’s Arithmetic than PA.

Since the assumption that every recursive function can be strongly represented in any system of Arithmetic with the omega-Constructivity rule of inference I(iii) leads to inconsistency in the system, it follows that Gödel’s reasoning does not hold in any interpretation of omega₁-PA.

Further, although omega₁-PA now proves the closed Induction axiom schema A(11), in the absence of the strong Generalisation rule of inference I(ii) of PA, we still cannot conclude either of:

omega₁-PA proves: ‘Closed Induction’ => ‘Open Induction’ holds in omega₁-PA

‘Open Induction’ holds in omega₁-PA => omega₁-PA proves: ‘Closed Induction’

whereas in PA we have both:

PA proves: ‘Closed Induction’ => ‘Open Induction’ holds in PA

‘Open Induction’ holds in PA => PA proves: ‘Closed Induction’

4.6. The conflict with model theory

Now, although PA and omega₁-PA have identical axioms, with identical interpretations and models, the difference in their rules of inference yield differing consequences amongst the well-formed formulas of the two formal systems, and hence amongst corresponding statements under interpretation.

The difference is reflected in the fact that Cantor’s transfinite ordinal Arithmetic CA is not a model of PA, since:

PA proves: x+1 = 1+x

PA proves: (Ax)(x+1 = 1+x).

However, in omega₁-PA, we have that, as in omega-PA:

omega₁-PA proves: x+1 = 1+x

~(omega₁-PA proves: (Ax)(x+1 = 1+x)).

Further, in the absence of strong Generalisation, all the theorems of omega₁-PA translate into true statements, in Cantor’s transfinite ordinal-Arithmetic CA, about only the sub-domain N of natural numbers.

Thus CA is a model of omega₁-PA.

This appears to conflict with the implicit Platonistic thesis that it is the axioms of a formal system that essentially determine the logical consequences in the interpretation.

4.7. Introducing the omega-Specification rule of inference

Can we strengthen omega₁-PA further?

We consider introducing Parikh’s form of the Kreisel-Parson’s conjecture in omega₁-PA as a means for specifying essentially the conditions under which the closure of a provable, open, well-formed formula in omega₁-PA yields a provable, closed, well-formed formula of omega₁-PA:

I(iv) omega-Specification: (Ax)F(x) is provable in PA if, for each natural number n, there is a proof in PA of F(n), and its Gödel-number is less than some natural number k that is independent of n.

4.8. A yet stronger omega-calculus : omega₂-PA

We thus arrive at a yet stronger, constructive, formulation of the first order predicate calculus, omega₂-calculus.

omega₂-PA is now the axioms A(1) to A(11) of first order Arithmetic, as specified in §3.4, added to a first order predicate calculus A(i) to A(iii), as specified in §3.4, along with the Modus Ponens rule of inference I(i), the omega-Constructivity rule of inference I(iii) and the omega-Specification rule of inference I(iv).

Thus PA and omega₁-PA, omega₂-PA all have identical axioms, with identical interpretations and models. Again, omega₂-PA appears intuitively a more natural and constructive formalisation of Peano’s Arithmetic than PA.

We note that, as in PA, we now have that:

omega₂-PA proves: x+1 = 1+x

omega₂-PA proves: (Ax)(x+1 = 1+x)

So, like PA, omega₂-PA too does not admit Cantor’s transfinite ordinals in any model.

Thus, though omega₂-PA and omega₁-PA are both constructive and have identical axioms, these too have significantly different logical consequences, highlighting again the apparent conflict with the implicit Platonistic thesis that it is the axioms of a formal system that essentially determine the logical consequences.

4.9. The Generalisation rule of inference holds for omega₂-PA

We note that, in omega₂-PA, as in PA, the strong Generalisation rule of inference I(ii) holds, since we now have the meta-equivalence:

omega₂-PA proves: F(x) <=> omega₂-PA proves: (Ax)F(x)

It follows that, in omega₂-PA, as in PA, we have:

omega₂-PA proves: ‘Closed Induction’ <=> ‘Open Induction’ holds in omega₂-PA

4.10. We cannot infer Gödel’s conclusions from his reasoning in omega₂-PA

However, omega₂-PA retains the constructive and intuitionistically unobjectionable nature inherited from omega-PA.

Thus, in sharp contrast to PA, omega₂-PA does not admit the strong representation of every recursive function, and so Gödel’s reasoning establishing the existence of undecidable propositions cannot be carried out in omega₂-PA.

This follows from the fact that, if f(x, y) is a recursive function that is represented by a omega₂-PA well-formed formula F(x, y, z), then the formal provability of (E₁x₃)F(k, m, x₃) is the intuitive assertion (cf. §2.9) that, for any given natural numbers k and m, we can always construct some (non-unique) pair of natural numbers u, v such that the Beta-function β(u, v, i) represents the first m terms, i.e. f'(k, 0), f'(k, 1), ... , f'(k, m), that are common to every primitive recursive function such as f'(x₁, x₂) that is formally represented by F(x₁, x₂, x₃).

To prove this for any given F(x₁, x₂, x₃), and given natural numbers k and m, we can determine a suitable Turing machine that will actually construct the sequence f'(k, 0), f'(k, 1), ... , f'(k, m) uniquely in order to verify the assertion.

Clearly we can choose a k such that the number of terms in the above sequence, and so the Gödel-number of any Turing-computable proof, exceeds any given natural number k₁.

It follows that, in omega₂-PA, we cannot assume that if the Gödel-number of a proof of:

(E₁x₃)F(x₁, x₂, x₃)

is less than a given natural number k₁, then the Gödel-number of a proof of:

(E₁x₃)F(x+1, x₂, x₃)

will also not exceed k₁.

We cannot thus assume that:

omega₂-PA proves: (E₁x₃)F(x₁, x₂, x₃) => (E₁x₃)F(x+1, x₂, x₃).

Hence we cannot assume that the argument of §2.13 will establish strong representability for every recursive function F(x₁, x₂, x₃), as is necessary for Gödel’s reasoning to hold.

In fact, since the assumption that every recursive function can be strongly represented in any system of Arithmetic with the omega-Constructivity rule of inference I(iii) leads to inconsistency in the system, it follows that Gödel’s conclusions do not logically follow from his reasoning in any interpretation of omega₂-PA.

We once more have the apparent conflict with the implicit Platonistic thesis that it is the axioms of a formal system that essentially determine the logical consequences in the interpretation.

4.11. Does Gödel’s reasoning hold even when his conclusions do not?

The question arises: When can we infer Gödel’s conclusions from his reasoning?

◄ Index ◄ Contents ◄ Chapter 1 ◄ Chapter 2

◄ Chapter 3 ▲ Chapter 4 Chapter 5 ► Conclusions ► Web_links ►

(Updated : Friday 11^th January 2002 2:35:51 AM by re@alixcomsi.com)

References

Burbanks, Andrew. (e-seminar) Fast-Growing Functions and Unprovable Theorems.

<Ord’ls : http://www.maths.bris.ac.uk/~maadb/research/seminars/online/fgfut/fgfut09.html>

Davis, M (ed.). 1965. The Undecidable. Raven Press, New York.

Franzén, Torkel. Provability and Truth.

< Home page : http://www.sm.luth.se/~torkel/>

Friedman, Harvey. 1997. Unprovable theorems in discrete mathematics.

Gödel, Kurt. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Also in M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

<1931 Paper : http://www.ddc.net/ygg/etext/godel/godel3.htm>

< Beta-function : http://www.ddc.net/ygg/etext/godel/godel3.htm - LEMMA1>

< See remarks on p189 : http://www.ddc.net/ygg/etext/godel/godel3.htm - 16>

<Eqn. 8.1 : http://www.ddc.net/ygg/etext/godel/godel3.htm - EQ8.1>

<cf. Recursive definition #17 : http://www.ddc.net/ygg/etext/godel/godel3.htm - DEF17>

<cf. Proposition V : http://www.ddc.net/ygg/etext/godel/godel3.htm#PROP-V>

Gödel, Kurt. 1934. On undecidable propositions of formal mathematical systems. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

Lucas, J. R. The Gödelian argument.

<Gödelian argument : http://www.leaderu.com/truth/2truth08.html>

Mendelson, Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton.

Parikh, Rohit. 1973. On the length of proofs. In Trans. AMS, 177, 29-36

Parsons, Charles D. 1995. Platonism and mathematical intuition in Kurt Gödel's thought. In The Bulletin of Symbolic Logic, Volume 1, Issue 1, March 1995.

<1995 Article : http://www.math.ucla.edu/~asl/bsl/0101-toc.htm>

Peregrin, Jaroslav. 1997. Language and its Models: Is Model Theory a Theory of Semantics?

< cf. also Models : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/models-html.html>

<cf. also Quantifier : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node8.html>

<cf. also Basis : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node5.html>

< cf. also Consequence : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node11.html>

< cf. also Truth : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node3.html>

< cf. also Language : http://www.hf.uio.no/filosofi/njpl/vol2no1/models/node2.html>

Podnieks, Karlis. 2001. Around Goedel's Theorem.