I review the classical conclusions drawn from Gödel’s meta-reasoning establishing an undecidable proposition GUS in standard PA. I note that, for any given set of numerical values of its free variables, every recursive number-theoretic relation can be expressed formally in PA by syntactically different, but formally equivalent, formulas. I argue that this asymmetry yields alternative Representation and Self-reference meta-Lemmas. Gödel’s meta-reasoning can thus be expressed avoiding any appeal to the truth of universally quantified propositions in the standard interpretation M of PA. I argue that this now establishes GUS as decidable, and PA as omega-inconsistent. I argue further that Rosser’s extension of Gödel’s meta-reasoning is invalid, and involves an intuitionistically objectionable deduction.

1. Introduction

1.1 The main argument

We note that, for any given set of natural number values for its free variables, every instantiation of a recursive number-theoretic relation[2], say q(x, y), can, in particular, be expressed ([Me64], p117) in PA by the following two, syntactically different but formally equivalent, propositions[3].

The first is a direct expression of the particular instantiation of the relation as the PA-formula [q(k, m)][4] - since a recursive number-theoretic relation q(x, y) can be expressed as a proposition in only the primitive symbols of PA once the variables x and y are replaced by the numerals [k] and [m][5], that represent the specific natural numbers k and m.

The second is as a formally equivalent formula[6] [Q(k, m)] of PA that is defined in terms of the Gödel-Beta function by the usual Representation meta-Lemma ([Me64], p131). This meta-Lemma establishes that every recursive number-theoretic relation, such as say q(x, y), is instantiationally equivalent to an arithmetical relation Q(x, y) that can be expressed in only the primitive symbols of PA.

Thus, although q(x, y) may not necessarily be reducible to an expression that consists of only the primitive symbols of PA, Q(x, y) is always a well-formed formula of PA.  Further, q(k, m) and  Q(k, m) are equivalent arithmetical propositions that can both be expressed in PA by the formally equivalent PA-propositions [q(k, m)] and [Q(k, m)], respectively, for any given natural numbers k and m. It follows that though the relations q(x, y) and Q(x, y) are “arithmetically” equivalent, they are not “formally” equivalent.

I argue that this asymmetry yields alternative Representation and Self-reference meta-Lemmas that are critical to any exposition of Gödel’s meta-reasoning. This reasoning can now be expressed avoiding any direct appeal to the intuitive truth of propositions of M. I then argue that we can establish GUS as decidable in PA, and PA as omega-inconsistent. I argue further that Rosser's non-formal extension of Gödel’s meta-reasoning is invalid, and involves an intuitionistically objectionable deduction.

1.2 The critical semantic elements of Gödel 's and Rosser's reasoning

I argue that the critical elements in classical expositions (such as [Me64], p145) of Gödel's reasoning involve semantic interpretations in the Representation meta-Lemma, and in Gödel's Self-reference meta-Lemma. Both meta-Lemmas correlate the PA-provability of propositions with the truth of their interpretations in the standard model M (Intuitive Arithmetic) of PA.

1.3 The semantic form of the Representation meta-Lemma

Classically (eg. [Me64], p131, Proposition 3.23), the Representation meta-Lemma essentially asserts, weakly and non-formally, the following:

If f(x₁, x₂, ... , x_n) is a recursive arithmetic relation of M whose arguments are natural numbers, then there is another arithmetic relation F(x₁, x₂, ... , x_n) of M such that, for any given set of natural numbers (k₁, k₂, ... , k_n, k_m) of M:

(a)     if f(k₁, k₂, ... , k_n, k_m) is true in M, then [F(k₁, k₂, ... , k_n, k_m)] is PA-provable, and

(b)     [(E!x_m)F(k₁, k₂, ... , k_n, x_m)] is PA-provable.

1.4  The semantic form of Gödel's Self-reference meta-Lemma

Classical expositions of Gödel’s reasoning (eg. [Me64], p145) define a recursive arithmetic relation q(x, y) that is true in M if and only if x is the Gödel-number of a well-formed formula [H(z)] of PA with a single free variable [z], and y is the Gödel-number of a PA-proof of [H(x)].

So, in its classically semantic form, Gödel’s Self-reference meta-Lemma essentially asserts, weakly and non-formally, the following:

For any given formula [H(z)] of a single variable in PA whose Gödel-number is the natural number h of M, and any natural number j of M, we have, by the definition of q(x, y), that:

(c)     q(h, j) is true in M if, and only if, [H(h)] is PA-provable.

1.5 A non-semantic Representation meta-Lemma

In this essay, I replace the semantic Representation meta-Lemma §1.4 by the following stronger, meta-assertion:

If f(x₁, x₂, ... , x_n) is a recursive arithmetic relation of M whose arguments are natural numbers then, by Hilbert and Bernays Representation meta-Lemma, there is another arithmetic relation F(x₁, x₂, ... , x_n) of M such that, for any given set of natural numbers (k₁, k₂, ... , k_n) of M:

(d)     [f(k₁, k₂, ... , k_n) <=> F(k₁, k₂, ... , k_n)] is PA-provable.

1.6 A non-semantic Self-reference meta-Lemma

Similarly, I replace the semantic Self-reference meta-Lemma §1.5 by the following stronger, meta-assertions:

For any given formula [H(z)] of a single variable in PA whose Gödel-number is the natural number h of M, and any natural number j of M, we have, by the definition of q(x, y), that:

(e)     [q(h, j) => H(h)] is PA-provable;

(f)     If [H(h)] is PA-provable, then [q(h, k)] is PA-provable for some natural number k of M.

1.7 Consequences

I argue that §1.6(d) and §1.7(e) are denumerable sets of non-semantic meta-Lemmas in PA, whilst §1.7(f) is a non-semantic meta-Lemma in the meta-theory of PA.

I also argue that Goedel’s reasoning can be constructively interpreted as implying that, from the PA-provability of [(Ex)H(x)], we may not always assume the existence of some numeral [h] such that [H(h)] is provable in PA. All we may conclude is that ~H(x) may not be a uniformly decidable predicate in M; however, ~H(n) may yet hold in M for any given natural number n - which may be provable meta-mathematically. I argue that such an - intuitionistically objectionable - assumption, is, however, implicit in Rosser's proof of undecidability.

I argue that, by using the meta-Lemmas §1.6 and §1.7 to recast classical expositions of Gödel's and Rosser's semantic proofs of undecidability, we can determine that PA is omega-inconsistent and that Rosser's assumption (as above) is invalid.

Consequently, Gödel's and Rosser's semantic arguments do not yield formally undecidable propositions in PA in a constructive and intuitionistically unobjectionable way.

1.8 Background and conclusions

The above is an extension of earlier arguments questioning various disquieting features of the classical expositions and interpretation of Gödel’s reasoning, such as in Mendelson [Me64].

In Anand [An01], I question the significance, and relevance, of standard PA. I argue the thesis that differing perceptions of the interpretation of Gödel’s meta-reasoning, and conclusions, arise because the system of standard first order Peano Arithmetic PA, in which Gödel’s meta-reasoning is classically considered, is only one - and perhaps not the most representative - of several, significantly differing, systems ([An01], §3.0) that can be defined to formalise our system of Intuitive Arithmetic M of the natural numbers (which we take both as the Arithmetic based on an intuitive interpretation of Dedekind’s formulation of Peano’s Postulates, and as the standard interpretation of any formalisation of these Postulates).

In Anand [An02], I outline in general terms a constructive, and intuitionistically unobjectionable, formalisation PP of our Intuitive Arithmetic M of the natural numbers in which the Axioms and Rules of Inference are recursively definable. I argue that, although Gödel’s undecidable sentence GUS is a well-formed formula in PP ([An02], §3.9), it is an ill-defined proposition that formally reflects the Liar paradox in PP ([An02], §4.5).

In this essay I assume some familiarity with the issues addressed in the above two essays, especially those concerning the asymmetry ([An02], §6.1) between a primitive recursive function of M, and the interpretation in M of its strong representation ([An01], §2.8) in PA. I argue that this asymmetry can also be expressed formally, and use this to develop a formal expression of Gödel’s meta-reasoning to argue that:

(i)      Gödel’s undecidable sentence GUS is actually decidable in PA under a reasonable interpretation of his meta-reasoning that, avoiding any appeal to the truth of propositions of M, is constructive and intuitionistically unobjectionable;

(ii)     PA is not omega-consistent under such interpretation;

(iii)    If we take M to be the standard model for PA, this implies that standard PA is semantically inconsistent under the standard interpretations of Gödel’s meta-reasoning;

(iv)    Rosser’s extension of Gödel’s meta-reasoning, establishing an undecidable proposition RUS in a consistent PA, is invalid under such an interpretation.

2. The formal system PA

2.1. Peano’s Arithmetic PA

We start by noting that, in standard (first order) Peano’s Arithmetic PA, the following Axioms and Rules of Inference (essentially [Me64], p103) can reasonably be taken as our (sole) basis for assigning provability values to the well-formed sentences of PA:

(PA1)     [~(0 = (x+1))]

(PA2)     [~(x = y) => ~((x+1) = (y+1))]

(PA3)     [(x+0) = x]

(PA4)     [(x+(y+1)) = ((x+y)+1)]

(PA5)     [(x*0) = 0]

(PA6)     [(x*(y+1)) = ((x*y)+x)]

2.2. The alphabet S of PA

These formulas and assertions are expressed using only a small set S of undefined, primitive, symbols such as “+” (addition) and “*” (multiplication) only apart from the logical symbols “~”(not), “=>” (implies), “=” (equals), “&” (and), “v” (or), “[(Ax)]” (a special symbol for representing ‘for all x’)[7], “x, y, ...” (variables), “a, b, c, ...” (constants), “[0]” (numeral zero), “[1]” (numeral one), and the two parentheses “(“, “)”.

The non-terminating series of numerals “[0], [0+1], [(0+1)+1], [((0+1)+1)+1], ...”, is taken as formally representing, in PA, the various non-terminating, intuitive, natural number series such as “0, 1, 10, 11, ...” (in binary format), or “0, 1, 2, 3, ...” (in the more common decimal format).

2.3. Rules of Inference in PA

We take as our (only) means for deriving other provable assertions in PA, from the basic Axioms (PA1-6), the standard first order logical axioms ([Me64], p57), and the following Rules of Inference, namely Modus Ponens, Induction and Generalisation:

(PAR1)      Modus Ponens: From [F] and [F => G] we may conclude [G], where [F] and [G] are any well-defined formulas of PA;

(PAR2)      Induction: From [F(0)] and [(Ax)(F(x) => F(x+1))] we may conclude [(Ax)F(x)];

(PAR3)      Generalisation: From [F(x)] we may conclude [(Ax)F(x)].

3. The significance of the formal system PA

3.1. Meta-assertions about PA can be expressed in PA

We note that, as described by Gödel, terms such as “well-formed formula”, “well-formed proposition” and “proof sequence” can be formally defined in the language of PA. We can thus express meta-assertions about PA such as “ ‘[F(x)]’ is a well-formed formula in PA”, “ ‘[(Ax)F(x)]’ is a well-formed proposition in PA”, “ ‘[F(x)]’ is a provable formula in PA”, “ ‘[(Ax)F(x)]’ is a provable proposition in PA” and “The ‘Gödel’ proposition is not provable in PA”, amongst others, as equivalent arithmetical assertions in PA (Gödel 1931, pp.14).

3.2. Provability in PA

We note that Gödel defines a well-formed formula P of M as provable in PA if and only if there is a finite proof sequence, consisting of well-formed formulas of PA, each of which is either an Axiom (PA1-6), or an immediate consequence of the preceding provable well-formed formulas by the Rules of Inference (PAR1-3), and where P is the final well-formed formula in the sequence. The Axioms (PA1-6) are, of course, all provable well-formed formulas in PA by definition ([Go31], p13).

The provable propositions in PA are characterised by the fact that they are all provable well-formed formulas without variables, such as “[(Ax)F(x)]”, expressed using only the small set of primitive, undefined symbols of the alphabet S.

3.3. Recursive functions of M are not directly expressible in PA

The significance of the alphabet S selected for expressing provable propositions of M is that many significant number-theoretic functions of M such as “n!” (factorial), “m^n” (exponential), “m/n” (division), “n is a prime number”, amongst others, are defined recursively, and recursive functions are constructively computable ([Me64], p237).

Thus we note that n!, for instance, is defined by:

(i)      0! = 1

(ii)     (n+1)! = (n+1)*(n!) for all natural numbers n.

Now, for a given natural number n, any expression involving n! can clearly be reduced in a finite number of steps to an expression that consists of only the symbols of the alphabet S, eg. “3! = 5” to “3*(2*(1*(1))) = 5”. Thus, in this case, “3! = 5” can be viewed simply as a shorthand notation (i.e. another name, or definition) for the assertion “3*(2*(1*(1))) = 5”.

However, if we attempt to eliminate the symbol “!” on the right hand side of (ii) for an unspecified x, we soon discover that “x!” is not directly reducible to a form that is expressible in only the symbols of the alphabet S.

The question thus arises: Can we locate a general expression FACT(x) of M that is expressible in only the alphabet S, and is such that its values are identical to those of x! whenever a natural number n is substituted for x?

3.4. A non-semantic Representation meta-Lemma

(a)  This issue is addressed, and answered indirectly[8], by a meta-Lemma of Hilbert and Bernays, which establishes that every recursive number-theoretic relation definable in M, say f(x) = y where f(x) is a recursive number-theoretic function of M, is indeed instantiationally equivalent to another, uniquely defined, arithmetical relation [F(x, y)] of M that can be represented in PA (i.e. F(x, y) is a well-formed formula of M that is expressible in only the alphabet S), such that (cf. [Me64], p118-120):

(i)      For any given natural numbers k and m, [(f(k) = m) <=> F(k, m)] is PA=provable;

(ii)     [(E!y)F(k, y)] is PA-provable; [9]

where [n] denotes the numeral in PA that represents the natural number n of M, and "E!" denotes uniqueness of the existential assertion.

(b)  We note that (a)(i) expresses a denumerable set of Lemmas in PA since, for given natural numbers k and m, any recursive number-theoretic proposition such as “f(k) = m” can be expressed as a proposition “f(k) = m” in terms of the alphabet S only. It is thus a valid well-formed formula of PA that is decidable[10] in PA, since f(k) is a constructively computable function of M ([Me64], p231).

For instance, if f(n) is the factorial function n!, then, as mentioned above in §3.3, the proposition “3! = 5” of M can also be expressed as “3*(2*(1*(1))) = 5”, which is the interpretation in M of the decidable PA-proposition [3*(2*(1*(1))) = 5].

3.5. Gödel-numbering

We note next that every expression [F], constructed by concatenation from the primitive, undefined symbols of S, can be assigned a unique natural number of M, which we term as the "Gödel-number” of the expression [F] ([Go31], p13).

Now Gödel has established ([Go31], p17-22) that we can define a recursive arithmetic relation prf(x, y) in M (Gödel’s ‘yBx’), constructed out of 44 “simpler” recursive arithmetic functions and relations, such that, for any given natural numbers k and m, prf(k, m) is true in M if and only if m is the Gödel-number of a finite proof sequence PRF in PA for some well-formed formula [K] in PA whose Gödel-number is k.

However, as we argue in §3.4(b), for any given natural numbers k and m, [prf(k, m)] is also provable in PA if and only if m is the Gödel-number of a finite proof sequence PRF in PA for some well-formed formula [K] in PA whose Gödel-number is k.

3.6. Gödel’s formal Self-reference Lemmas

From the recursive arithmetic relation prf(x, y), we can thus define another recursive arithmetic relation q(x, y) (Mendelson’s W₁(x, y),[Me64], p143) in M which is similarly true in M if and only if x is the Gödel-number of a well-formed formula [H(z)] of PA with a single free variable [z], and y is the Gödel-number of a proof of [H(x)] in PA.

Hence the constructive self-reference, which lies at the core of Gödel's meta-reasoning, is that, since [q(h, j)] is a PA-formula for any given natural numbers h, j, it is provable in PA if and only if the expression J in PA, whose Gödel number is j, is a proof sequence in PA of the well-formed proposition [H(h)] of PA, where h is the Gödel-number of the formula [H(z)] in PA containing only one free variable. More precisely, if [H(z)] is as defined above, we have that, by definition:

(i)      For any given natural number j, PA proves: [q(h, j) => H(h)];

(ii)     If [H(h)] is PA-provable, then there is some natural number j such that [q(h, j)] is PA-provable.

We note, firstly, that whilst (i) is a denumerable set of Lemmas in PA, (ii) is actually a meta-Lemma in the meta-theory of PA. Further that, here also, as argued in §3.4(b), (i) and (ii) hold since, for given natural numbers h and j, any recursive number-theoretic expression such as q(h, j) can also be expressed directly in terms of the alphabet S only. It can thus be shown to be a valid, decidable, well-formed formula of PA.

4. Gödel’s meta-reasoning

4.1. The two basic Lemmas and GUS

Now, by the Representation meta-Lemmas, the recursive arithmetic relation q(x, y) is also instantiationally equivalent to another, uniquely defined, well-formed arithmetic relation Q(x, y), such that:

(i)      For any given natural numbers k and m, [q(k, m) <=> Q(k, m)] is PA-provable.

If p is the Gödel-number of the well-formed formula [(Ay)(~Q(x, y))], we consider the well-formed “Gödelian” proposition GUS expressed by [(Ay)(~Q(p, y))].

By Gödel's Self-reference meta-Lemmas, we then have that:

(ii)     For any given natural number j, [q(p, j) => (Ay)(~Q(p, y))] is PA-provable;

(iii)    If [(Ay)(~Q(p, y))] is PA-provable, then there is some natural number r such that [q(p, j)] is PA-provable.

4.2. Gödel’s semantic meta-mathematical proof of undecidability[11]

(a) We assume firstly that r is the Gödel-number of some proof-sequence R in PA for the proposition [(Ay)(~Q(p, y))]. It then follows from Gödel’s Self-reference lemma §4.1(iii) that q(p, r) is true in M. By the Representation Lemmas §4.1(i), this implies that [Q(p, r)] is provable in PA. However, assuming standard logical axioms for PA, from the provability of [(Ay)(~Q(p, y))] in PA, we have that [~Q(p, r)] is provable in PA. It follows that there is no natural number r that is the Gödel-number of a proof-sequence R in PA for the proposition [(Ay)(~Q(p, y))]. Hence, by §4.1(ii), q(p, r) is not true in M for any r, and so [(Ay)(~Q(p, y))] is not provable in PA.

(b) We assume next that r is the Gödel-number of some proof-sequence R in PA for the proposition [~(Ay)(~Q(p, y))]. However, we have by §4.2(a) that q(p, r) is not true in M for any r, and so, by §4.1(i), [~Q(p, r)] is provable in PA for all r. Assuming that PA is omega-consistent, it follows that [~(Ay)(~Q(p, y))] is not provable in PA.

(  Note: We define PA as omega-consistent if and only if there is no formula ‘[F(x)]’ such that ‘(n)PA proves: [F(n)]’ and ‘PA proves: [~(Ax)F(x)]’.)

(c) The classical conclusion drawn from the above is that, if PA is omega-consistent, then the proposition [(Ay)(~Q(p, y))] is undecidable in PA, since neither [(Ay)(~Q(p, y))] nor [~(Ay)(~Q(p, y))] is provable in PA ([Me64], pp.143-144).

(d)  By §4.2(a), we have that [~Q(p, r)] is provable in PA for all natural numbers r. We thus have that ~Q(p, y) is true in M for all y (since the domain of M is expressible in PA, and every provable proposition of PA is true in M). It now follows by our definition of quantification in M (ignoring this point lends validity to Lucas’ Gödelian argument) that “(Ay)(~Q(p, y))” can be asserted as a true proposition in M.

(e)  It is only in this sense that, although [(Ay)(~Q(p, y))] is not provable in PA, Gödel was able to assert “(Ay)(~Q(p, y))” as a true proposition in M. However, I argue here that the truth of the latter proposition in M is clearly of a definitional nature, and a formal consequence of the Axioms and Rules of Inference of PA.

(f)  I argue that the curious conclusion (e) reflects the fact that, in the presence of a Generalisation Rule of Inference, we cannot correspondingly postulate (or define) formally that [(Ay)(~Q(p, y))] follows as a provable proposition in PA from the provability of [~Q(p, r)] in PA for all natural numbers r, if PA is assumed consistent [Anand 2001, §1.11].

4.3. A non-semantic expression of Gödel’s meta-proof of undecidability

(a)  Now we note that we can also express the above meta-reasoning non-semantically as the meta-deduction:

(i)         PA proves: [(Ay)(~Q(p, y))];

... Hypothesis

(ii)        If [(Ay)(~Q(p, y))] is PA-provable, then there is some natural number r such that [q(p, r)] is PA-provable;

... By the Self-reference meta-lemmas §4.1(iii)

(iii)       Hence there is some natural number r such that [q(p, r)] is PA-provable;

 ... From (i) and (ii) by Modus Ponens in the meta-theory

(iv)       Now, for any given natural number r, [q(p, r) <=> Q(p, r)] is PA-provable;

... By the Representation lemmas §4.1(i)

(v)        Hence there is some natural number, r, such that [Q(p, r)] is PA-provable;

... From (iii) and (iv) by Modus Ponens, assuming (i)

(vi)       PA proves: [(Ey)Q(p, y)];

... From (v) by the logical axioms of PA, assuming (i)

(vii)      PA proves: [(Ay)(~Q(p, y)) => (Ey)(~Q(p, y))];

... Tautology

(viii)     PA proves: [(Ey)(~Q(p, y))];

... From (i) and (vii) by Modus Ponens

Curiously, avoiding the meta-inference that “PA proves: [(i) => (vi)]” (by appealing to a Deduction Theorem in the meta-theory), the classical conclusion drawn from the above is that, since (vi) contradicts (viii), [(Ay)(~Q(p, y))] is not provable in a consistent PA, i.e.:

(ix)       PA does not prove: [(Ay)(~Q(p, y))].

... assuming PA is consistent

(b)  We also have the further classical meta-deduction:

(i)         PA proves: [~(Ay)(~Q(p, y))];

... Hypothesis

(ii)        PA proves: [(Ey)Q(p, y)];

... From (i) by definition

(iii)       Now, for any given natural number r, [q(p, r) => (Ay)(~Q(p, y)] is PA-provable;

... By the Self-reference lemmas §4.1(ii)

(iv)       Whence, for any given natural number r, [~(Ay)(~Q(p, y) => ~q(p, r)] is PA-provable;

... From (iii) by the logical axioms of PA

(v)        And, so, for any given natural number r, [~q(p, r)] is PA-provable;

... From (i) and (iv) by Modus Ponens

(vi)       Also, for any given natural number r, [q(p, r) <=> Q(p, r)] is PA-provable;

... By the Representation lemmas §4.1(i)

(vii)      And, so, for any given natural number r, [~q(p, r) <=> ~Q(p, r)] is PA-provable;

... From (vi) by the logical axioms of PA

(viii)     It follows that, for any given natural number r, [~Q(p, r)] is PA-provable;

... From (v) and (vii) by Modus Ponens, assuming (i)

Since (i) and (viii) contradict the omega-consistency of PA, the further conclusion drawn classically from the above reasoning is that [~(Ay)(~Q(p, y))] too is not provable in an omega-consistent PA, i.e.:

(ix)       PA does not prove: [~(Ay)(~Q(p, y))].

... Assuming PA is omega-consistent.

So we have the classical conclusion drawn from Gödel’s above meta-reasoning that GUS is an undecidable proposition in an omega-consistent PA.

5. Can GUS be decidable, and PA omega-inconsistent?

However, as noted in §4.3(a)(viii), it can also be argued reasonably in the meta-theory of PA, assuming p is the Gödel-number of the well-formed formula [(Ay)(~Q(x, y))], that:

(i)      For any given natural number r:

PA proves: [q(p, r) => (Ay)(~Q(p, y))];

... By the Self-reference lemmas §4.1(ii)

(ii)     PA proves: [(Ay)(~Q(p, y))] => (Er)PA proves: [q(p, r)];

... By the Self-reference meta-lemmas §4.1(iii)

(iii)    Also, for any given natural number r, [q(p, r) <=> Q(p, r)] is PA-provable;

... By the Representation lemmas §4.1(i)

(iv)    Hence, if [(Ay)(~Q(p, y))] is PA-provable, then there is some natural number r such that [Q(p, r)] is PA-provable;

... From (ii) and (iii)

(v)     It follows that, if [(Ay)(~Q(p, y))] is PA-provable, then [(Ey)Q(p, y)] is PA-provable;

... From (iv) by the logical axioms of PA

(vi)    PA proves: [(Ay)(~Q(p, y)) => (Ey)Q(p, y)];

... From (v) by the Deduction theorem

(vii)   PA proves: [(Ay)(~Q(p, y)) => ~(Ay)(~Q(p, y))];

... From (vi) by definition

(viii)  PA proves: [~(Ay)(~Q(p, y))];

... From (vii) assuming PA is consistent

We can thus alternatively, and prima facie quite reasonably, conclude from Gödel’s meta-reasoning that, if PA is consistent, then ~(Ay)(~Q(p, y)) is a theorem of PA, and not an undecidable proposition in PA.

Now we also have that:

(ix)    PA proves: [(Ey)Q(p, y)];

... From (viii) by definition

(x)     Also, for any given natural number r, [~(Ay)(~Q(p, y) => ~q(p, r)] is PA-provable;

... From (i) by the logical axioms of PA

(xi)    Hence, for any given natural number r, [~q(p, r)] is PA-provable;

... From (viii) and (x) by Modus Ponens

(xii)   Further, for any given natural number r, [~q(p, r) <=> ~Q(p, r)] is PA-provable;

... By the Representation lemmas §4.1(i)

(xiii)  And, so, for any given natural number r, [~Q(p, r)] is PA-provable.

... From (xi) and (xii) by Modus Ponens

Thus, from (viii) and (xiii), we may further conclude that a consistent PA is not omega-consistent.

6. Standard PA is semantically inconsistent

On this interpretation of Gödel’s meta-reasoning, it follows that, in every model M of PA, (Ey)Q(p*, y) is a true proposition in M, even though Q(p*, r*) would be false for every r* in M that is the interpretation of a numeral r of PA.

If M is taken to be the classical standard interpretation of PA, then both ~(Ay)(~Q(p, y) and (Ay)(~Q(p, y) interpret as true propositions in M, and the above meta-reasoning then implies that standard PA is semantically inconsistent[12].

7. Is Rosser’s undecidable proposition established constructively?

The question now arises: Are other undecidable propositions also formally derivable in PA on the above interpretation of Gödel’s meta-reasoning?

We address only one instance of this question by considering Mendelson’s version ([Me64], p144-146) of Rosser’s extension of Gödel’s meta-reasoning, where he seeks to establish an undecidable proposition RUS in a consistent, standard PA.

7.1. Rosser’s Self-reference Lemmas

Rosser reasoning is that, along with the recursive arithmetic relation  q(x, y), we can also define a recursive number-theoretic relation s(x, y) in M which is provable in PA if and only if x is the Gödel-number of a well-formed formula [H(z)] of PA with a single free variable [z], and y is the Gödel-number of a proof of [~H(x)] in PA.

Since [s(h, j)] too is expressible in PA for given natural numbers h, j, it also is provable in PA if and only if the expression J in PA, whose Gödel number is j, is a proof sequence in PA of the well-formed proposition [~H(h)] of PA, where h is the Gödel-number of the formula [H(z)] in PA.

More precisely, if [H(z)] is as defined above, we have that, by definition:

(i)      For any given natural number j, [s(h, j) => ~H(h)] is PA-provable;

(ii)     If [~H(h)] is PA-provable, then there is some natural number j such that [s(h, j)] is PA-provable.

7.2. Rosser’s undecidable proposition RUS

Now, by Hilbert and Bernays Representation meta-Lemma, the recursive relation s(x, y) too is instantiationally equivalent to another, uniquely defined, well-formed arithmetical relation S(x, y), so that:

(i)      For any given natural numbers k and m, [s(k, m) <=> S(k, m)] is PA-provable.

If u is the Gödel-number of the well-formed formula [(Ay)(Q(x, y) => (Ez)(z=<y & S(x, z)))][13], we consider then the well-formed Rosser proposition RUS expressed by [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))].

Clearly, by definition, we have the denumerable set of Rosser’s non-semantic Self-reference meta-Lemmas:

(ii)     For any given natural number j, [q(u, j) => (Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is PA-provable;

(iii)    If [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is PA-provable, then there is some natural number j such that [q(u, j)] is PA-provable;

(iv)    For any given natural number j, [s(u, j) => ~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))];

(v)     If [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is PA-provable, then there is some natural number j such that [s(u, j)] is PA-provable.

7.3. Rosser’s semantic meta-mathematical proof of undecidability

(a) We assume now that r is the Gödel-number of some proof sequence R in PA for the proposition [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))]. It then follows from Rosser’s Self-reference meta-Lemma §7.2(iii) that q(u, r) is true in M. Also, by the Representation meta-Lemmas §4.1(i), this implies that [Q(u, r)] is provable in PA. However, assuming standard logical axioms for PA, from the provability of [(Ay)(Q(u, y)  => (Ez)(z=<y & S(u, z)))] in PA, we have that [Q(u, r) => (Ez)(z=<r & S(u, z))] is provable in PA and, by Modus Ponens, that [(Ez)(z=<r & S(u, z)))] is provable in PA. Now, since PA is consistent, and [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is provable in PA, it follows there is no proof in PA of [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))]. So, by §7.2(iv), s(u, n) is not true in M for any natural number n, and so ~s(u, n) is true in M for every natural number n. Hence, by §7.2(i), [~S(u, n)] too is provable in PA for every natural number n. We thus have, by the standard logical axioms of PA, that [~(Ez)(z=<r & S(u, z))] is provable in PA. Since this contradicts our earlier derivation, it follows that [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is not provable in a consistent PA.

(b) We assume next that r is the Gödel-number of some proof-sequence R in PA for the proposition [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))]. By §7.2(v), we then have that s(u, r) is true in M. Hence, by §7.2(i), [S(u, r)] is provable in PA. However, if PA is consistent, we have by §7.3(a) that there is no proof sequence in PA for [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))], and so, by §7.2(iii), ~q(u, n) is true in M for every natural number n. Hence, by §4.1(i), [~Q(u, n)] is provable in PA for all natural numbers n.

(i)      We thus have, by the standard logical axioms of PA, that [y=<r => ~Q(u, y)] is provable in PA;

We consider now the following deduction:

(1)     [r=<y];

... Hypothesis

(2)     [S(u, r)];

... By (b) above

(3)     [r=<y & S(u, r)];

... From (1) and (2), Tautology

(4)     [(Ez)(z=<y & S(u, z))];

... From (3) by the logical axioms of PA

(ii)     From (1)-(4), by the Deduction Theorem, we have that [r=<y => (Ez)(z=<y & S(u, z))] is provable in PA;

(iii)    Now, by the logical axioms of PA, we have that [y=<r v r=<y] is provable in PA;

(iv)    From (i)-(iii), also by the logical axioms of PA, we now have that [~Q(u, y) v (Ez)(z=<y & S(u, z))] is provable in PA;

(v)     We have further, again by the logical axioms of PA, that [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z))] is provable in PA.

However, this contradicts our assumption that the proposition [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is provable in PA.

The classical conclusion from the above meta-reasoning is that [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] too is not provable in a consistent PA, and so RUS is undecidable in PA ([Me64], p146).

7.4. A non-semantic expression of Rosser’s meta-proof of undecidability

However, we note that the Rosser’s above, semantic, meta-reasoning presumes omega-consistency. This is exposed when the argument is expressed non-semantically as below.

(a)  Now, the first half of the argument can be expressed as:

(i)         PA proves: [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))];

... Hypothesis

 (ii)       If [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is PA-provable, then there is some natural number, r, such that [q(u, r)] is PA-provable;

... By the Self-reference meta-Lemma §7.2(iii)

(iii)       There is some natural number, r, such that [q(u, r)] is PA-provable;

 ... From (i) and (ii) by Modus Ponens in the meta-theory

(iv)       For any given natural number r, [q(u, r) <=> Q(u, r)] is PA-provable;

... By the Representation meta-Lemmas §4.1(i)

(v)        There is some natural number, r, such that [Q(u, r)] is PA-provable;

... From (iii) and (iv) by Modus Ponens, assuming (i)

(vi)       For any given natural number r, [Q(u, r) => (Ez)(z=<r & S(u, z))] is PA-provable;

... From (i) by the logical axioms of PA

(vii)      There is some natural number, r, such that [(Ez)(z=<r & S(u, z))] is PA-provable;

... From (v) and (vi) by Modus Ponens, assuming (i)

(viii)     PA does not prove: [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))];

... From (i), assuming PA is consistent

(ix)       For any given natural number r, [~s(u, r))] is PA-provable;

... From (i) by the Self-reference meta-Lemmas §7.2(iv)

(x)        For any given natural number r, [~S(u, r)] is PA-provable;

... From (ix) by the Representation meta-Lemmas §7.2(i), assuming (i)

(xi)       For any given natural number r, [(Az)(z=<r => ~S(u, z))] is PA-provable;

... From (x) by the logical axioms of PA, assuming (i)

(xii)      For any given natural number r, [~(Ez)(z=<r & S(u, z))] is PA-provable;

... From (xi) by the logical axioms of PA, assuming (i)

Since (xii) contradicts (vii), the classical conclusion from this meta-reasoning is that:

(xiii)     PA does not prove: [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))].

... Assuming PA is consistent

(b)  The second half of the argument is essentially:

(i)         PA proves: [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))];

... Hypothesis

(ii)        If [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))] is PA-provable, then there is some natural number, r, such that [s(u, r)] is PA-provable;

... By the Self-reference meta-Lemma §7.2(v)

(iii)       There is some natural number, r, such that [s(u, r)] is PA-provable;

 ... From (i) and (ii) by Modus Ponens in the meta-theory

(iv)       For any given natural number n, [s(u, n) <=> S(u, n)] is PA-provable;

... By the Representation meta-Lemmas §7.2(i)

(v)        There is some natural number, r, such that [S(u, r)] is PA-provable;

... From (iii) and (iv) by Modus Ponens, assuming (i)

(vi)       For any given natural number n, [~q(u, n)] is PA-provable;

 ... From (i) and §7.2(iii) assuming PA is consistent

(vii)      For any given natural number n, [~q(u, n) <=> ~Q(u, n)] is PA-provable;

... By the Representation meta-Lemmas §4.1(i)

(viii)     For any given natural number n, [~Q(u, n)] is PA-provable;

... From (vi) and (vii) by Modus Ponens, assuming (i)

(ix)       For any given natural number n, [(Az)(z=<n => ~Q(u, z))] is PA-provable;

... From (viii) by the logical axioms of PA, assuming (i)

(x)(1)      There is some natural number, r, such that [r=<y] is PA-provable;

... Theorem of PA

(x)(2)      There is some natural number, r, such that [S(u, r)] is PA-provable;

... From (v) above, assuming (i)

(x)(3)      There is some natural number, r, such that [r=<y & S(u, r)] is PA-provable;

... From (1) and (2), assuming (i) – Invalid deduction

(x)(4)      PA proves: [(Ez)(z=<y & S(u, z))];

... From (3), assuming (i)

(xi)       There is some natural number, r, such that [r=<y => (Ez)(z=<y & S(u, z)))] is PA-provable;

... From (x)(1) and (x)(4) by the Deduction Theorem, assuming (i)

(xii)      For any given natural number r, [y=<r v r=<y] is PA-provable;

... Theorem of PA

(xiii)     PA proves: [~Q(u, y) v (Ez)(z=<y & S(u, z))];

... From (ix), (xi) and (xii), by the logical axioms of PA

(xiv)     PA proves: [(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))];

... From (xiii), by the logical axioms of PA, Modus Ponens and Generalisation, assuming (i)

Since (xiv) contradicts (i), the classical conclusion drawn from the above is that:

(xv)      PA does not prove: [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))].

... Assuming that PA is consistent

Now we note that the above meta-reasoning is based on the invalid deduction in (x)(3). This appeals to the implicitly Platonistic assumption that, if we assume that PA proves: [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))], then we can also conclude that PA proves: [S(u, r)] for some unspecified, but specific, natural number r, as in §7.3(b)(i)(2).

However, from the assertion “PA proves: [~(Ay)(Q(u, y) => (Ez)(z=<y & S(u, z)))]” and Rosser’s Self-reference meta-Lemmas §7.2(ii)-(iv), we may constructively only conclude the non-specific meta-mathematical assertion “There is some natural number, r, such that [S(u, r)] is PA-provable”, as in (v) above. We may not further introduce “PA proves: [S(u, r)]” for a specific r, as in §7.3(b)(i)(2), except as an additional premise[14] in the application of the Deduction Theorem[15]. Consequently, this would not yield the inference (xi) as Rosser intended. So the formal deduction of §7.3(b)(ii) from §7.3(b)(i)(1)-(4) can, reasonably, be held as invalid in any non-semantic meta-reasoning such as (x)(1)-(4) above.

8. Conclusion

(a) We can thus, reasonably, conclude that the classical interpretations of Gödel’s and Rosser’s meta-arguments do not unequivocally establish undecidable sentences in any formal system in which:

(i)      The proper Axioms and Rules of Inference are recursively definable;

(ii)     Every recursive relation is representable.

(b) We can also reasonably conclude further that:

(i)      Gödel’s undecidable sentence GUS is actually decidable in PA under a reasonable interpretation of his meta-reasoning that, avoiding any appeal to the truth of propositions of M, is constructive and intuitionistically unobjectionable;

(ii)     PA is not omega-consistent under such interpretation;

(iii)    If we take M to be the standard model for PA, this implies that standard PA is semantically inconsistent under the standard interpretations of Gödel’s meta-reasoning;

(iv)    Rosser’s extension of Gödel’s meta-reasoning, establishing an undecidable proposition RUS in a consistent PA, is invalid under such an interpretation.

References

 

[An01]    Anand, Bhupinder Singh. 2001. Beyond Gödel: Simply constructive systems of first order Peano’s Arithmetic that do not yield undecidable propositions by Gödel’s reasoning. (Web essay).

 

<Web page: http://alixcomsi.com/Constructivity_abstracts.htm>

 

[An02]    Anand, Bhupinder Singh. 2002. Paradox regained: Life beyond Gödel’s shadow. Alix Comsi, Mumbai (Web essay).

 

<Web page: http://alixcomsi.com/Constructivity_preamble_Rev1.htm>

 

[Go31]    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.

 

<Web version: http://www.ddc.net/ygg/etext/godel/godel3.htm>

 

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

 

(Updated: Tuesday, 21^st June 2005, 1:14:08 AM IST, by re@alixcomsi.com)