Constructivity03

◄ Chapter 2 ◄ Index Chapter 4 ►

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 3. Is there an omega-constructive first order Arithmetic?

Contents

3.0. Introduction

3.1. The primitive symbols of a general first order predicate calculus K

3.2. The logical axioms of K

3.3. The rules of inference of K

3.4. Gödel’s formal system PA

3.5. General Arithmetics: weak-GA

3.6. General Arithmetics: strong-GA

3.7. Peano Arithmetics : weak-PA

3.8. Peano Arithmetics : standard PA

3.9. Closed Induction implies open Induction in PA

3.10. Can PA admit models of transfinite ordinals?

3.11. omega-constructive first order Arithmetics

3.12. omega-constructive Arithmetic : omega-GA

3.13. The omega-constructive Peano Arithmetic : omega-PA

3.14. Every model of PA is a model of omega-PA

3.15. The essential difference between PA and omega-PA

3.16. Can omega-PA admit models of transfinite ordinals?

3.17. Can we strengthen omega-PA

3.0. Introduction

In this third section we formally construct and briefly examine various systems of first order Arithmetic. We argue that we cannot use Gödel’s reasoning to prove that every primitive recursive function (Mendelson p120) can be strongly represented formally in all such systems. Hence it does not universally establish the existence of undecidable propositions that are true under interpretation.

We finally construct an omega-constructive system of first order Arithmetic, omega-PA, where we replace the non-constructive closed Induction axiom schema by a constructive, open Induction axiom schema.

We base omega-PA on a modified first order predicate calculus where we replace the strong Generalisation rule of inference I(ii) by a weaker omega-Constructivity rule of inference I(iii).

We show that every model of standard PA is a model of omega-PA. We show further that every primitive recursive function cannot be strongly represented formally in omega-PA if it is simply consistent. So, in omega-PA, Gödel’s reasoning does not establish the existence of undecidable propositions that are true under interpretation.

We argue in this, and the next, section that Gödel mistakenly concluded (Gödel p190-191) that the existence of undecidable propositions that are true under interpretation must follow from his reasoning in all the above formal systems of Arithmetic.

We begin by reviewing in detail Mendelson’s definition (p103) of the system PA. This is essentially the formal system in which Gödel constructed his undecidable propositions.

3.1. The primitive symbols of a general first order predicate calculus K

The system PA is based on a particularisation of the general first order predicate calculus K whose primitive symbols are (Mendelson p57):

'~' (not), '=>' (implies), '(' (left parenthesis), ')' (right parenthesis), ',' (comma), 'x₁, x₂, ...' (denumerably many individual variables), 'A₍_n_,_j₎, (n, j >= 1)' (denumerably many predicate letters), 'f₍_n_,_j₎, (n, j >= 1)' (denumerably many function letters), and 'a_i, (i>= 1)' (denumerably many constants).

3.2. The logical axioms of K

The logical axioms of K are:

K(1) A => (B => A)

K(2) (A => (B => C)) => ((A => B) => (A => C))

K(3) (~B => ~A) => ((~B => A) => B)

K(4) (Ax_i)A(x_i) => A(t), if A(x_i) is a well-formed formula of K and t is a term of K free for x_i in A(x_i).

K(5) (Ax_i)(A => B) => (A => (A => (Ax_i)B) if A is a well-formed formula of K containing no free occurences of x_i.

3.3. The rules of inference of K

The rules of inference of K are:

I(i) Modus Ponens: B follows from A and A => B.

I(ii) Strong Generalisation: (Ax_i)A follows from A.

3.4. Gödel’s formal system PA

The particular system of first order predicate calculus that Mendelson uses (p103), to develop Gödel's reasoning in a formal first order Arithmetic, contains:

A(i) a single predicate letter 'A' to represent equality A(t, s) between the terms t and s, which we express as ‘t=s’;

A(ii) one individual constant 'a' which we write as ‘0’;

A(iii) three function letters f, g and h to represent, respectively, the successor of ‘t’, which we write as ‘t'’, addition, which we write as ‘t+s’, and multiplication, which we write as ‘t.s’.

The axioms of Arithmetic that Gödel considered were Dedekind's axioms for number theory, known as Peano's Postulates, which are essentially as below (not necessarily independent):

A(1) (x₁ = x₂) => ((x₁ = x₃) => (x₂ = x₃)

A(2) (x₁ = x₂) => (x₁' = x₂')

A(3) 0 ¹ x₁'

A(4) (x₁' = x₂') => (x₁ = x₂)

A(5) (x₁ + 0) = 0

A(6) (x₁ + x₂') = (x₁ + x₂)'

A(7) x₁.0 = 0

A(8) x₁. x₂' = (x₁. x₂) + x₁

A(9) (x₁ ¹ 0) => (Ex₂)(x₁ = x₂')

and the two meta-axiom schemas (more accurately, rules of inference) of closed and open Induction:

A(10) For any wff F(x) of PA, from (F(0) and (Ax)(F(x)) => F(x')), we may conclude (Ax)F(x)

A(11) For any wff F(x) of PA, from (F(0) and (F(x)) => F(x')) we may conclude F(x)

3.5. General Arithmetics : weak-GA

If we eliminate strong Generalisation I(ii), closed Induction A(10) and open Induction A(11) from PA, we obtain a weak first order general Arithmetic, weak-GA.

Weak-GA is thus the axioms A(1) to A(9) 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, with only the Modus Ponens rule of inference I(i).

Since all axioms of weak-GA are provable in PA, every interpretation and model of PA is an interpretation and model of weak-GA.

However, in the absence of strong Generalisation I(ii), and closed Induction A(10), the argument of §2.13, establishing the strong representability of every recursive function, cannot be carried out in weak-GA.

So, in weak-GA, Gödel’s reasoning does not establish the existence of undecidable propositions that are true under interpretation.

3.6. General Arithmetics : strong-GA

If we strengthen weak-GA by adding the strong Generalisation rule of inference I(ii), we arrive at a stronger first order general Arithmetic, strong-GA.

Strong-GA is thus the axioms A(1) to A(9) 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, with both the Modus Ponens rule of inference I(i) and the strong Generalisation rule of inference I(ii).

Since all axioms of strong-GA are provable in PA, every interpretation and model of PA is an interpretation and model of strong-GA.

However, in the absence of closed Induction A(10), the argument of §2.13, establishing the strong representability of every recursive function, still cannot be carried out in strong-GA.

So, in strong-GA, Gödel’s reasoning does not establish the existence of undecidable propositions that are true under interpretation.

3.7. Peano Arithmetics : weak-PA

If we add closed Induction A(10) to weak-GA, we arrive at a weak first order Peano Arithmetic, weak-PA.

Weak-PA is thus the axioms A(1) to A(10) 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, with only the Modus Ponens rule of inference I(i).

Since all axioms of weak-PA are provable in PA, every interpretation and model of PA is an interpretation and model of weak-PA.

However, in the absence of strong Generalisation I(ii), the argument of §2.13, which establishes the strong representability of every recursive function, cannot be carried out in weak-PA.

Hence, in weak-PA also, Gödel’s reasoning does not establish the existence of undecidable propositions that are true under interpretation.

We note also that it is not obvious whether weak-PA proves weak-Induction A(11).

3.8. Peano Arithmetics : Standard PA

We arrive at the standard first order Peano Arithmetic, standard PA, used by Gödel, when we add strong Generalisation I(ii) to weak-PA.

Standard PA is thus the axioms A(1) to A(10) 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, with both the rules of inference, Modus Ponens I(i), and strong Generalisation I(ii).

Since standard PA establishes the strong representability of every recursive function, we are now able to formally derive Gödel’s undecidable propositions in standard PA.

However, as we have argued in the earlier sections, strong representability now admits closed well-formed formulas that refer to totalities, under interpretation, which are not reflected in the intuitive Arithmetic that is intended to be formalised by standard PA.

3.9. Closed Induction implies open Induction in PA

We note that, in standard PA, closed Induction A(10) implies open Induction A(11).

Thus, from the closed Induction axiom schema A(10) in standard PA:

Standard PA proves: (F(0) & Standard PA proves: (Ax)(F(x) => F(x+1)))

=> Standard PA proves: (Ax)F(x)

we have that if:

Standard PA proves: F(0) & Standard PA proves: F(x) => F(x+1)

then:

Standard PA proves: F(x) => F(x+1)

Standard PA proves: (Ax)(F(x) => F(x+1)) ... Gen

Standard PA proves: F(0) & Standard PA proves: (Ax)(F(x) => F(x+1))

Standard PA proves: (Ax)F(x)

Standard PA proves: F(x)

We thus have that:

Standard PA proves: F(0) & Standard PA proves: (F(x) => F(x+1)))

=> Standard PA proves: F(x)

Hence standard PA proves the open Induction axiom schema A(11), and so PA and standard PA are identical.

3.10. Can PA admit models of transfinite ordinals?

Now we note that:

PA proves: x+1 = 1+x

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

It follows that Cantor’s transfinite ordinal-Arithmetic CA, in which omega is a term for which we have that “omega +1” is not equal to “1+ omega”, is not a model of PA.

3.11. omega-constructive first order Arithmetics

We next define a range of omega-constructive first order systems of Arithmetic, by introducing an intuitionistically unobjectionable omega-Constructivity rule of inference:

I(iii) omega-Constructivity: From [“x is a numeral” => F(x)] we may conclude (Ax)F(x).

Since “x is a numeral” is recursively definable, we note that I(iii) is a recursively definable rule of inference that is equivalent to the concept of omega-constructivity introduced in “Chapter 1. First order Arithmetic is not omega-constructive”.

3.12. omega-constructive Arithmetic : omega-GA

If we strengthen weak-GA by adding the omega-Constructivity rule of inference I(iii), we arrive at a formal system of constructive omega-GA.

omega-GA is thus the axioms A(1) to A(9) 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).

Since all axioms of omega-GA are provable in PA, every interpretation and model of PA is an interpretation and model of omega-GA.

Also, in the absence of strong Generalisation I(ii), and closed Induction A(10), the argument of §2.13, establishing the strong representability of every recursive function, cannot be carried out in omega-GA.

However, as we have shown in the earlier section, “Chapter 1. First order Arithmetic is not omega-constructive”, in any system of Arithmetic with the omega-Constructivity rule of inference I(iii), the assumption that every recursive function can be strongly represented leads to inconsistency in the system.

Hence, in omega-GA, Gödel’s reasoning does not establish the existence of undecidable propositions that are true under interpretation.

3.13. The omega-constructive Peano Arithmetic : omega-PA

If we now add open Induction A(11) to omega-GA, we arrive at a constructive formal system of Peano’s Arithmetic, omega-PA.

omega-PA is thus axioms A(1) to A(9), 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).

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.

We note that the open Induction axiom schema A(11) permits us to constructively establish in omega-PA, for open well-formed formulas F(x) for which we can prove both the well-formed formulas F(0) and F(x) => F(x+1), that the well-formed formula F(x) is provable, and so necessarily well-defined.

3.14. Every model of PA is a model of omega-PA

Since all axioms of omega-PA are provable in PA, every interpretation and model of PA is an interpretation and model of omega-PA.

Clearly, even though omega-PA does not prove closed Induction A(10), it is, intuitively, a natural and constructive formalisation of Peano’s Arithmetic.

Moreover, Gödel’s reasoning does not establish the existence of undecidable propositions in omega-PA in a constructive and intuitionistically unobjectionable way, as he intended (Gödel 1931 p189).

3.15. The essential difference between PA and omega-PA

We note that the essential difference between PA and omega-PA lies simply in their respective meta-assertions about the nature and scope of the valid consequences[1] amongst the elements of the domain of each system under interpretation.

Thus the strong Generalisation rule of inference, for instance, asserts that, if F(x) is provable, then (x)F(x) is provable, and so, under every interpretation, the range of values for which the predicate ‘F’ is satisfied can be referred to as a well-defined totality.

In other words, the predicate ‘F’ is asserted, Platonistically, to be a characteristic of every element of the domain under every interpretation, irrespective of whether the element corresponds to any constructive representation within the formal system PA or not.

In contrast, the meta-rule of omega-Constructivity rule of inference is the weaker, constructive, and intuitionistically unobjectionable assertion that, if F(x) is provable, this only implies that the predicate ‘F’ is asserted to be a provable characteristic of every element of the domain under interpretation that has a constructive representations within the formal system omega-PA.

3.16. Can omega-PA admit models of transfinite ordinals?

We note that Cantor’s transfinite ordinal-Arithmetic, CA, contains the system of natural numbers and so, in the absence of strong Generalisation, all the axioms of omega-PA translate into true statements, in CA, about only the sub-domain N of natural numbers.

Thus CA is a model of omega-PA.

This reflects the fact that omega-PA permits transfinite interpretations in which relations that hold in any denumerable sub- domain of the interpretation may not hold in the entire domain of the interpretation.

For instance, although:

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

we also have:

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

3.17. Can we strengthen omega-PA

This raises the natural question: At which point does omega-PA loose both its non-constructive character, and its power to permit transfinite interpretations as above?

In other words, can we strengthen omega-PA, and extend the range of its provable well-formed formulas under interpretation, without losing its essentially constructive, and intuitionistically unobjectionable character?

In the next section, we address this question.

◄ Index ◄ Contents ◄ Chapter 1 ◄ Chapter 2

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

(Updated : Sunday 3^rd March 2002 12:14:08 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.