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