Constructivity01

◄ Contents ◄ Index Chapter 2 ►

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 1. First order Arithmetic is not omega-constructive

Contents

1.0. Introduction

1.1. Introducing omega-constructivity : omega-PA

1.2. The significance of omega-constructivity

1.3. Constructive PA should be intuitive

1.4. Differentiating between omega-constructivity and omega-completeness

1.5. The relevance of omega-constructivity

1.6. prf'(x, y) is a Turing decidable predicate

1.7. The Representation Theorem

1.8. Can PA be both simply consistent and omega-constructive?

1.9. Consequences of the omega-constructivity of omega-PA

1.10. The meta-mathematical inconsistency in omega-PA

1.11. A simply consistent PA is neither omega-constructive, nor omega-complete

1.12. What is the significance of the omega-incompleteness of PA?

1.13. The Gödelian argument

1.14. omega-provable propositions and PA

1.15. What kind of propositions are omega-provable?

1.16. The Platonistic axiom of reducibility and PA

1.17. What is the significance of: (Ax)F(x) is omega-provable?

1.18. Why is first order Arithmetic not omega-constructive?

1.0. Introduction

We take as our primary reference Mendelson’s first order exposition of the essentially second order formal system and various revolutionary concepts introduced by Gödel in his original paper “On formally undecidable propositions of Principia Mathematica and related systems I”.

We also borrow some content, and style of presentation, from Karlis Podnieks’ proof of Goedel’s incompleteness theorem in his e-textbook “Around Goedel’s Theorem”.[1]

We take as our starting point the systems of first order predicate calculus and first order Arithmetic defined by Mendelson (p57 & p102).

We introduce the concept of omega-constructivity, and show that standard first order Arithmetic PA is not omega-constructive.

1.1. Introducing omega-constructivity : omega-PA

We say that a simply consistent formal system of standard first order Arithmetic PA is omega-constructive if and only if it is not the case that, for any well-formed formula F(x₁, x₂, x₃, ... , x_n) of PA, we can have both:

(i) ~(PA proves: F(x₁, x₂, x₃, ... , x_n)), and

(ii) (Ax₁, Ax₂, Ax₃, ..., Ax_n)(PA proves: F(x₁, x₂, x₃, ... , x_n)), where the domain of x_i is the set of natural numbers.

In other words, we cannot have a situation where a well-formed formula such as F(x) is unprovable in PA, but F(1), F(2), F(3), ... are all provable, if PA is both simply consistent and omega-constructive, where n denotes the numeral representing[2] the natural number n in the formal system PA.

We name such an omega-constructive PA system ‘first order omega-Arithmetic’, and refer to it as omega-PA.

1.2. The significance of omega-constructivity

This definition implicitly reflects the thesis that an infinite, compound, meta-assertion such as "F(1) is provable in PA & F(2) is provable in PA & F(3) is provable in PA & ..." is simply a convenient way of expressing and visualising the meta-assertion “F(n) is provable in PA for all n”, where n is intuitively taken to range over the natural numbers.

1.3. Constructive PA should be intuitive

We argue that, in a constructive formal system of PA that is intended to formalise the natural numbers - where the intended domain of x under interpretation contains, and preferably consists only of, elements that correspond to the numerals that represent the natural numbers in the formal system - the meta-assertion “F(x) is provable in PA” should intuitively translate as equivalent to “F(n) is provable in PA for all n”, where n is intuitively taken to range over the natural numbers.

So a formal system that is not omega-constructive is counter-intuitive.

1.4. Differentiating between omega-constructivity and omega-completeness

We note the difference between omega-constructivity and omega-completeness.

PA is said to be omega-complete if and only if there is a no well-formed formula F(x) with one free variable such that:

(i) ~( PA proves: (Ax)F(x)), and

(ii) (An)( PA proves: F(n)), where the domain of n is the set of natural numbers.

Now, in our intended formal system PA of the natural numbers, an infinite, compound, meta-assertion such as "F(1) is provable in PA & F(2) is provable in PA & F(3) is provable in PA & ... " can also be intuitively asserted as a consequence of a meta-proof of the generalization "(Ax)(F(x) is provable in PA)".

However, we need to consider the possibility that, under interpretation, such a PA may admit an infinite domain for x that is not denumerable, or that the generalisation "(Ax)(F(x)" may be a well-formed formula, but an ill-defined proposition under interpretation (which could be the case if F(x) either represents, or translates under interpretation as, a vague predicate).

It follows that, under our intended formalisation, the denumerable meta-assertion "F(1) is provable in PA & F(2) is provable in PA & F(3) is provable in PA & ..." cannot be assumed to conversely yield a proof of '(Ax)F(x)’ in PA.

So a system that is not omega-complete is not necessarily counter-intuitive.

1.5. The relevance of omega-constructivity

To see the relevance of omega-constructivity to PA, we consider in §1.5 to §1.7 the primitive recursive (Mendelson p120) predicate prf'(u, y), which we define[3] as true if and only if u is the Gödel-number (Podnieks 2001 Section 5.2) of a well-formed formula F(x₁, x₂, x₃, ... , x_n) of PA, containing the free variables x₁, x₂, x₃, ... , x_n, and y is the Gödel-number of a proof in PA of F(u, x₂, x₃, ... , x_n).

1.6. prf'(x, y) is a Turing decidable predicate

Now we can construct a Turing machine that, given any u and v, will decode (Podnieks 2001 Excercise 5.3) u into F(x₁, x₂, x₃, ... , x_n), check whether x₁ occurs in it, construct F(u, x₂, x₃, ... , x_n) by replacing x₁ wherever it occurs by u, decode v, check if v is a proof sequence, and finally check to see if F(u, x₂, x₃, ... , x_n) is the last well-formed formula in the proof sequence coded by v.

Thus prf'(x, y) is a Turing-decidable predicate.

1.7. The Representation Theorem

By Podnieks Representation Theorem (Section 3.3) we can therefore construct a PA-formula PRF'(x, y) expressing the predicate prf'(x, y) such that, for any given k₁, k₂:

(i) prf'(k₁, k₂) is true => PA proves: PRF'(k₁, k₂), and

(ii) ~prf'(k₁, k₂) is true => PA proves: ~PRF'(k₁, k₂).

We let r be the Gödel-number of ~PRF'(x₁, x₂).

We consider the well-formed formula ~PRF'(r, x₂).

Now, from the definition of prf'(u, y), it follows that[4]:

(iii) prf'(r, y) is true <=> y is the Gödel-number of a proof in PA of ~PRF'(r, x₂).

1.8. Is PA both simply consistent and omega-constructive?

In §1.8 to §1.11, we next address the question : Can PA be both simply consistent and omega-constructive?

Let us assume that it is, and that omega-PA proves ~PRF'(r, x₂), so that some natural number k is the Gödel-number of this proof.

Then, by §1.7(iii), prf'(r, k) is true and hence,

omega-PA proves: PRF'(r, k).

However, by our premise, we have that,

omega-PA proves: ~PRF'(r, x₂), and so

omega-PA proves: ~PRF'(r, k).

Therefore, since omega-PA is assumed simply consistent, it follows that ~PRF'(r, x₂) cannot be proved in omega-PA.

1.9. Consequences of the omega-constructivity of omega-PA

We thus have from the omega-constructivity of omega-PA that it is not the case that:

(An)(omega-PA proves: ~PRF'(r, n)).

Now, since prf'(x, y) is primitive recursive, if ~prf'(r, y) is true for all y, it follows meta-mathematically from §1.7(ii) that:

(An)(omega-PA proves: ~PRF'(r, n)).

So, if it is not the case that,

(An)(omega-PA proves: ~PRF'(r, n)),

then it is not the case that,

~prf'(r, y) is true for all y.

Hence we have, meta-mathematically, that:

~prf'(r, k) is false for some k,

prf'(r, k) is true,

omega-PA proves: ~PRF'(r, x₂).

1.10. The meta-mathematical inconsistency in omega-PA

We have thus demonstrated that if PA is assumed both simply consistent and omega-constructive, then we have the meta-mathematical inconsistency:

(i) omega-PA proves: ~PRF'(r, x₂)

=> ~(omega-PA proves: ~PRF'(r, x₂)), and

(ii) ~(omega-PA proves: ~PRF'(r, x₂))

=> omega-PA proves: ~PRF'(r, x₂).

1.11. A simply consistent PA is neither omega-constructive, nor omega-complete

So, if standard first order Arithmetic PA is assumed simply consistent, then it cannot be omega-constructive in the sense defined above in §1.1.

Since, in standard first order Arithmetic PA, we have that:

PA proves: F(x) <=> PA proves: (Ax)F(x),

it follows that standard first order Arithmetic PA is, additionally, not omega-complete.

1.12. What is the significance of the omega-incompleteness of PA?

Now, if standard first order Arithmetic PA is assumed simply consistent, then there is the well-formed formula ~PRF'(r, x₂) with one free variable such that:

(i) ~(PA proves: (Ax₂)~PRF'(r, x₂)), and

(ii) (An)(PA proves: ~PRF'(r, n)).

The question arises: What is the significance of such omega-incompleteness of PA?

To get some indirect perspective on this question, let us for a moment consider the Gödelian argument.

1.13. The Gödelian argument

One interpretation, of the Gödelian argument as offered by J.R.Lucas, is the thesis that there is some non-mechanistic element - knowledge of which is Platonistically available to human intelligence but cannot be reflected in any machine intelligence - that is involved in establishing that a well-formed formula such as (x)F(x) is formally unprovable in PA, yet translates into a true proposition under interpretation in the standard model.

However, if the foregoing arguments are simply non-constructive and intuitionistically objectionable, but not non-mechanistic, then the Platonistic elements of the reasoning are built into the formal logic itself, and can be built equally rigorously, independent of any model, into machine intelligence.

1.14. omega-provable propositions in PA

Thus if we introduce:

~(PA proves: (Ax)F(x)) & (An)(PA proves: F(n))

as the meta-definition of:

‘(Ax)F(x)’ is omega-provable in PA,

we can reasonably argue that PA establishes the meta-assertions:

‘(Ax₂)~PRF'(r, x₂)’ is omega-provable in PA,

‘~PRF'(r, n)’ is provable in PA for every natural number n,

‘~PRF'(r, n)’ is true for every natural number n in every model of PA,

‘(An)~PRF'(r, n)’ is true in every model of PA,

although PA is unable to prove (Ax₂)~PRF'(r, x₂), and even though (Ax)~PRF'(r, x) may not hold true in every model of PA.

1.15. What kind of propositions are omega-provable?

The question arises: What makes a proposition such as (Ax)F(x) omega-provable?

An obvious possibility, as remarked earlier, is that F(x) may be a well-formed formula, but translate under interpretation into a vague or ill-defined predicate similar to the paradoxical self-referential constructions that give rise to the various linguistic, logical and mathematical antinomies.

We note that Gödel’s aim in his 1931 paper “On formally undecidable propositions of Principia Mathematica and related systems I” was not to eliminate the antinomies, but to eliminate imprecision of expression in the concepts of truth and proof by rigorously formalising (Gödel 1931 p176) first order logic and Arithmetic.

Accordingly, in his 1934 lecture notes (Davis p46) “On undecidable propositions of formal mathematical systems”, Gödel notes that “We shall depend on the theory of types as our means for avoiding paradox”.

So, although F(x) may be provable for any given x, the provability of (Ax)F(x) may, in some interpretation, involve an implicit reference to an ill-defined totality of all x that satisfy F(x).

In such a case, assuming the provability of (Ax)F(x) must yield a contradiction from which we can either conclude the inconsistency of PA, or deduce the unprovability of (Ax)F(x) in a simply consistent PA.

The latter conclusion could also then imply the Platonistic existence of some model of PA in which (Ax)~PRF'(r, x) does not hold true, even though (An)~PRF'(r, n) is true in every model of PA.

Clearly, in this case, the omega-provability of arithmetical assertions is better viewed as a reflection of the ‘vagueness or ill-definedness’ of some predicate inherent in their construction, where the range of values for which the predicate is satisfied under interpretation does not form a well-defined totality that can be validly referenced within a logical proposition.

1.16. The Platonistic axiom of reducibility and PA

A second possibility (not unrelated to the first) is that the formal system itself may have been defined Platonistically.

Thus the meta-equivalence in standard first order Arithmetic PA, that:

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

can also be viewed as reflecting elements of the Platonistic Axiom of Reducibility of the Principia (or the Comprehension Axiom of set theory : Gödel 1931 p178).

It essentially meta-postulates that the closure of every provable well-formed formula of PA containing free variables yields a provable well-formed formula of PA.

In every interpretation, the above can be taken to assert that if, for a well-formed formula F(x), x satisfies F(x) whenever x is representable in the formal system, then we can conclude (Ax)F(x) in the interpretation, and hence that the domain of x is well-defined (i.e. it forms a well-defined set in set theory) under the interpretation.[5]

1.17. What is the significance of: (Ax)F(x) is omega-provable?

To sum up, we note that, if (Ax)F(x) is omega-provable, then the following hold.

(i) ‘~(PA proves: (Ax)F(x))’ holds meta-mathematically.

This can be taken to intuitively imply either that there is some model of PA in which there is a non-constructive element (interpreted Platonistically) in the domain of x that is not representable in PA, and is such that it does not satisfy the predicate F(x), or that the totality of values for which the predicate ‘F’ holds over the domain of x in some model of PA is ill-defined.

(ii) ‘(An)(PA proves: F(n))’ holds meta-mathematically, where the domain of n is the set N of natural numbers.

This intuitively implies that, in every model of PA, the predicate F(x) is satisfied constructively by every interpretation of the numeral n in the domain of x.

(iii) ‘(Ax)(PA proves: F(x))’ holds meta-mathematically.

This includes (ii), but intuitively implies additionally that if, in any model of PA, there is (interpreted Platonistically) some element in the domain of x that is not an interpretation of the numeral n, but is otherwise representable in PA, then it necessarily satisfies F(x).

1.18. Why is first order Arithmetic not omega-constructive?

The choice of our formal system of first order Arithmetic may thus depend on whether it is our (tacit) intent to deny validity to well-formed formulas that reflect ill-defined elements under every interpretation, or to admit them as well-formed formulas and accept the intuitively artificial conclusion that they are formally unprovable, but translate into true propositions under interpretation.

The question arises: Assuming PA corresponds to the latter alternative, can we suitably modify PA so that, similar to the development of standard set theory ZF, we arrive at a PA system where we prevent the representation of predicates with ill-defined totalities of the values that satisfy them under interpretation, and where we eliminate the non-constructive elements that underlie the logic of PA?

In the next section, we therefore address the question: Why is standard first order Arithmetic PA not omega-constructive?

◄ Index ◄ Contents ▲ Chapter 1 Chapter 2 ►

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

(Updated : Saturday 12th January 2002 3:07:09 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.

<Goedel's Incompleteness Theorem : http://www.ltn.lv/~podnieks/gt5.html - BM5_3>

<Formula-number : http://www.ltn.lv/~podnieks/gt5.html - BM5_2>

<Self-reference lemma : http://www.ltn.lv/~podnieks/gt5.html - BM5_2>

Rosmaita, Brian J. Minds, machines, and metamathematics: constraints on the mathematical objection to mechanism.

Web resources

Free On-line Dictionary of Computing.

<cf. constructive : http://lgxserve.ciseca.uniba.it/lei/foldop/foldoc.cgi?query=constructive>

<Cmprhn. axiom : http://ase.isu.edu/ase01_07/ase01_07/bookcase/ref_sh/foldoc/99/8.htm>

Free On-line Dictionary of Philosophy.

Glossary of First-Order Logic.

<cf. Meta... : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - metalanguage>

<Intrprttn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - interpretation>

<Omega-comp. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - omegacom>

<Denum. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - denumerableset>

<Rcrsv. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - recursivefunction>

<Cptbl. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - computablefunction>

<Std. set theory : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - settheory>

<Gödel-number : http://www.earlham.edu/~peters/courses/logsys/glossary.htm#gnumbering>

<Well-formed formula : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - wff>

<Rprsntn. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - repfunction>

<Exstnc. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - existenceproof>

<Cnst. pr. : http://www.earlham.edu/~peters/courses/logsys/glossary.htm - constructiveproof>

Internet Encyclopedia of Philosophy

Larry Hauser’s Mostly Modern Philosophical Glossary.

MacTutor History of Mathematics archive

MathPages

Stanford Encyclopedia of Philosophy.

<cf. also Non-constructive : http://plato.stanford.edu/entries/mathematics-constructive/ - 2>

<cf. also Constructive : http://plato.stanford.edu/entries/mathematics-constructive/ - 1>

<cf. also Platonism : http://plato.stanford.edu/entries/mathphil-indis/ - 1>

Web Dictionary of Cybernetics and Systems

xrefer

<cf. Formalism : http://www.xrefer.com/entry/552091>

[1] Where possible, words and phrases have been hyper-linked to references, with detailed locations or further hyperlinks to the Internet, for consistency in definitions and meanings, or for expanding on their possible meanings-in-usage in a wider context.

Pointing your cursor at a word or phrase will indicate if the word or phrase has been hyper-linked to another reference (the cursor should change shape in most browsers).

Clicking once (default used whilst composing this paper) will bring up the cross-linked reference on the screen.

Use the ‘Back’ button ‘<=’ on the browser toolbar at the top of the screen (not any of the ‘◄’ buttons in the document) to return to the original hyper-linked word or phrase in the text.

[2] See also Gödel (Gödel 1931 Def17).

[3] This definition is based on the predicate W₁(u,y) used by Mendelson (p143) in his proof of Gödel’s undecidability theorem. It corresponds to Gödel’s (1931 p188 eqn 8.1) primitive recursive predicate xB(Sb(y : (19, z(y)))).

[4] This meta-mathematical equivalence seems to be the counter-part of Podnieks formal self-reference lemma.

[5] This indicates that we may need to formally distinguish between the meta-statement ‘F(x) is provable’, and the meta-statement ‘(x)F(x) is provable’. The former may reasonably be taken to intuitively assert that a well-formed formula ‘F(x)’ is provable for any given, even if unspecified, element x of every domain in every model. The latter, however, is intuitively the stronger assertion that ‘F(x)’ is provable for every element x of any domain; it implicitly postulates that the domain of x, in every model, is a well-defined totality for the predicate ‘F’, and so it can be validly referenced in a logical proposition. Equating the two can thus be viewed as unreasonable, and so counter-intuitive.

◄ Index ▲ Chapter 1 Bibliography ► Web_links ►

(Updated : Saturday 12th January 2002 3:07:41 AM by re@alixcomsi.com)