Chapter 4 : The significance of Gödel-numbering in formal systems of Arithmetic

4-01 Introduction

In his paper ‘On Formally Undecidable Propositions of Principia Mathematica and Related Systems I’ [Gödel 1931], Gödel’s intention is to establish, in a formal system of Arithmetic such as the Principia [Whitehead & Russell 1962], the meta-theorem [Gödel 1931 p24] :

Meta-theorem VI : For every omega-consistent primitive recursive class k of FORMULAS, there exists a primitive recursive CLASS EXPRESSION r such that neither vGenr nor Neg( vGenr ) belongs to Flg(k) (where v is the FREE VARIABLE of r).

In Chapter 2, we showed that Gödel’s reasoning, as also that of others such as Herbrand [cf. Davis 1965 p60 footnote 22] and Mendelson [1964 p143] who have based similar results of UNDECIDABILITY on his seminal work on the formal expressibility of primitive recursive functions and relations within S, rests on the invalid implicit assumption that every primitive recursive function and relation can be expressed as a formula of S in terms of (only) the undefined primitive symbols of S.

We showed there that Gödel’s primitive recursive relations xB(y) and Q(x, y), defined by :

xB(y) º Bw(x) & [(L(x)Gl(x) ) = y]

Q(x, y) º ~[xB[Sb(y : (19, z(y)))]]

are not expressible as formulas of S, and hence cannot be Gödel-numbered for an undetermined (free variable) y so as to yield a specific PREDICATE q in S of the two FREE VARIABLES 17 and 19 as (wrongly) assumed by Gödel in his proof of Theorem VI.

In the previous chapter we showed that the above inability to express every primitive recursive relation as a formula of S reflects the fact that not every primitive recursive relation is decidable [Gödel 1931 p20 definition 31 and footnote 36] in S.

We now show, in an intuitionistically unobjectionable way [cf. Gödel 1931 p26 & footnote 45a], that we can construct a primitive recursive CLASS EXPRESSION r in a simply consistent S such that neither vGenr nor Neg(vGenr) is PROVABLE in S (where v is the FREE VARIABLE of r) if we assume merely that Q(x, y) is validly Gödel-numberable.

4-02 The symbolic meta-mathematical reasoning in M

(a) We first assume that we can constructively determine a specific natural number q (a FUNCTION of the two FREE VARIABLES 17 and 19, but independent of the free variables x and y) such that:

╟_M qGdl [~[xB[Sb(y : (19, z(y)))]]]

(b) We can thus constructively determine natural numbers p, r, 17Genr and Neg(17Genr) such that:

╟_M pGdl [(x) ~[xB[Sb(y : (19, z(y)))]]]

╟_M rGdl [~[xB[Sb(p : (19, z(p)))]]]

╟_M (17Genr)Gdl [(x)~[xB[Sb(p : (19, z(p)))]]]

╟_M Neg(17Genr)Gdl [~[(x)~[xB[Sb(p : (19, z(p)))]]]]

╟_S Bew(17Genr)

º_M ├_S (x)~[xB[Sb(p : (19, z(p)))]]

º_M ├_S ~($x)[xB[Sb(p : (19, z(p)))]]

º_M ├_S ~Bew[Sb(p : (19, z(p)))]

®_M ~├_S (x)~[xB[Sb(p : (19, z(p)))]]

®_M ~├_S ~($x)[xB[Sb(p : (19, z(p)))]]

®_M ~├_S ~Bew[Sb(p : (19, z(p)))]

(d) We thus have that, if S is consistent, then :

╟_M qGdl [~[xB[Sb(y : (19, z(y)))]]]

®_M ~╟_S Bew(17Genr)

( If the formula ~[xB[Sb(y : (19, z(y)))]] is Gödel-numberable, then the FORMULA 17Genr is not PROVABLE in a consistent S.)

(e) However, we can also constructively establish that :

╟_S Bew(Neg(17Genr))

º_M ├_S ~[(x)~[xB[Sb(p : (19, z(p)))]]]

º_M ├_S ($x)[xB[Sb(p : (19, z(p)))]]

º_M ├_S Bew[Sb(p : (19, z(p)))]

®_M ├_S (x)~[xB[Sb(p : (19, z(p)))]]

®_M ├_S ~($x)[xB[Sb(p : (19, z(p)))]]

®_M ~├_S Bew[Sb(p : (19, z(p)))]

(f) Hence, if S is consistent, then we also have that :

╟_M qGdl [~[xB[Sb(y : (19, z(y)))]]]

®_M ~╟_S Bew(Neg(17Genr))

( If the formula ~[xB[Sb(y : (19, z(y)))]] is Gödel-numberable, then the FORMULA Neg(17Genr) is not PROVABLE in a consistent S.)

4-03 The verbose meta-mathematical reasoning in M

(a) We first assume explicitly, as Gödel does implicitly in the meta-proof of his Meta-Theorem VI [Gödel 1931 p24-25], that a specific PREDICATE q (which is a FUNCTION of the two FREE VARIABLES 17 and 19, but independent of the free variables x and y) can be determined as the unique Gödel-number of the primitive recursive relation Q(x, y) defined by:

Q(x, y) º_S ~[xB[Sb(y : (19, z(y)))]].

(b) ╟_M qGdl [~[xB[Sb(y : (19, z(y)))]]]

We thus assume that [Gödel 1931 p13-14] the PREDICATE q corresponds in S to the primitive recursive relation ~[xB[Sb(y : (19, z(y)))]] of S.

If p=17Genq, we also have that [Gödel 1931 p13-14] the PREDICATE p corresponds in S to the primitive recursive relation (x)~[xB[Sb(y : (19, z(y)))]].

(d) ╟_M rGdl [~[xB[Sb(p : (19, z(p)))]]]

If r=Sb(q : (19, z(p))), we further have that [Gödel 1931 p13-14] the PREDICATE r corresponds in S to the primitive recursive relation ~[xB[Sb(p : (19, z(p)))]] of S.

(e) ╟_M (17Genr)Gdl [(x)~[xB[Sb(p : (19, z(p)))]]]

We thus have that [Gödel 1931 p13-14] the PREDICATE 17Genr corresponds in S to the primitive recursive relation (x)~[xB[Sb(p : (19, z(p)))]] of S.

(f) ╟_M Neg(17Genr)Gdl [~[(x)~[xB[Sb(p : (19, z(p)))]]]]

Similarly, we have that [Gödel 1931 p13-14] the PREDICATE Neg(17Genr) corresponds to the primitive recursive relation ~[(x)~[xB[Sb(p : (19, z(p)))]]] of S.

(g) ╟_S Bew(17Genr) º_M ├_S (x)~[xB[Sb(p : (19, z(p)))]]

º_M ├_S ~($x)[xB[Sb(p : (19, z(p)))]]

º_M ├_S ~Bew[Sb(p : (19, z(p)))]

It now follows that [Gödel 1931 p13-14; p22 #46] the formula Bew(17Genr) holds in S, and so the FORMULA 17Genr is PROVABLE in S, if and only if the formula (x)~[xB[Sb(p : (19, z(p)))]] that corresponds to 17Genr is provable in S; and hence if and only if both the equivalent formulas ~($x)[xB[Sb(p : (19, z(p)))]] and ~Bew[Sb(p : (19, z(p)))] are also provable in S.

(h) ├_S ~Bew[Sb(p : (19, z(p)))]

®_M ~├_S (x)~[xB[Sb(p : (19, z(p)))]]

®_M ~├_S ~($x)[xB[Sb(p : (19, z(p)))]]

®_M ~├_S ~Bew[Sb(p : (19, z(p)))]

Now we have that [Gödel 1931 p13-14] the formula ~Bew[Sb(p : (19, z(p)))] is provable in S only if the formula (x)~[xB[Sb(y : (19, z(y)))]] that corresponds to p in S is not provable in S when we substitute the NUMERAL z(p) for the VARIABLE 19 in p.

Hence the formula ~Bew[Sb(p : (19, z(p)))] is provable in S only if the equivalent formulas (x)~[xB[Sb(p : (19, z(p)))]], ~($x)[xB[Sb(p : (19, z(p)))]] and ~Bew[Sb(p : (19, z(p)) )] are not provable in S.

(i) [╟_S Bew(17Genr)]

®_M [├_S ~Bew[Sb(p : (19, z(p)))]

®_M ~├_S ~Bew[Sb(p : (19, z(p)))]]

We thus have that [Gödel 1931 p13-14] if the formula Bew(17Genr) holds in S, then S is inconsistent.

(j) ~╟_S Bew(17Genr)

We conclude that, if we assume [Gödel 1931 p24-25] that a specific PREDICATE q (which is a FUNCTION of the two FREE VARIABLES 17 and 19, but independent of the free variables x and y) can be determined as the Gödel-number of the primitive recursive relation ~[xB[Sb(y : (19, z(y)))]], then the FORMULA 17Genr is not PROVABLE in a consistent S.

(k) ╟_S Bew(Neg(17Genr)

º_M ├_S ~[(x)~[xB[Sb(p : (19, z(p)))]]]

º_M ├_S ($x)[xB[Sb(p : (19, z(p)))]]

º_M ├_S Bew[Sb(p : (19, z(p)))]

We next see that [Gödel 1931 p13-14 ; p22 #46] the formula Bew(Neg(17Genr)) holds in S, and hence the FORMULA Neg(17Genr) is PROVABLE in S, if and only if the formula ~[(x)~[xB[Sb(p : (19, z(p)))]]] that corresponds to Neg(17Genr) is provable in S; and so if and only if both the equivalent formulas ($x)[xB[Sb(p : (19, z(p)))]] and Bew[Sb(p : (19, z(p)))] are also provable in S.

(l) ├_S Bew[Sb(p : (19, z(p)))]

®_M ├_S (x)~[xB[Sb(p : (19, z(p)))]]

®_M ├_S ~($x)[xB[Sb(p : (19, z(p)))]]

®_M ~├_S Bew[Sb(p : (19, z(p)))]

However, we then have that [Gödel 1931 p13-14] the formula Bew[Sb(p : (19, z(p)))] is provable in S only if the formula (x)~[xB[Sb(y : (19, z(y)))]] that corresponds to p in S is provable in S when we substitute the NUMERAL z(p) for the VARIABLE 19 in p.

It follows that the formula Bew[Sb(p : (19, z(p)))] is provable in S only if the equivalent formulas (x)~[xB[Sb(p : (19, z(p)))]], ~($x)[xB[Sb(p : (19, z(p)))]] and ~Bew[Sb(p : (19, z(p)))] are all provable in S, which would imply that S is inconsistent.

(m) ~╟_S Bew(Neg(17Genr))

We conclude that if we assume [Gödel 1931 p24-25] that a specific PREDICATE q (which is a FUNCTION of the two FREE VARIABLES 17 and 19, but independent of the free variables x and y) can be determined as the Gödel-number of the primitive recursive relation ~[xB[Sb(y : (19, z(y)))]], then the FORMULA Neg(17Genr) is not PROVABLE in a consistent S.

4-04 Conclusions

Gödel’s reasoning in his Meta-Theorem VI holds constructively, in an intuitionistically unobjectionable way [Gödel 1931 p26], in a consistent S - where we do not use his Theorem V and where S need not be assumed omega-consistent - to essentially yield the following:

Meta-theorem G-I : If the primitive recursive relation ~[xB[Sb(y : (19, z(y)))]] can be validly Gödel-numbered within a simply consistent formal system S of Arithmetic, then there is a primitive recursive CLASS EXPRESSION r such that neither vGenr nor Neg(vGenr) is PROVABLE in S (where v is the FREE VARIABLE of r and vGenr translates as ‘vGenr is not PROVABLE in S’).

◄ Index ◄ Title ◄ Copyright ◄ Dedication ◄ Preface ◄ Contents ◄ Chapter 1 ◄ Chapter 2

◄ Chapter 3 ▲ Chapter 4 Chapter 5 ► References ► Roots ► Bibliography ► Web_links ►

◄ Questioning Gödel’s Theorems (Dec 2000) ◄ Beyond Gödel (Oct 2001)

(Updated : 10/18/01 9:48:48 AM by re@alixcomsi.com)