◄ Chapter 2

◄ Index

Chapter 4 ►

Chapter 3 : Every primitive recursive relation is not always decidable

3-01    Introduction

G๖del’s reasoning in his paper ‘On Formally Undecidable Propositions of Principia Mathematica and Related Systems I’, 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 critical assumption that every primitive recursive function and relation in Peano’s Arithmetic A can be formally expressed as a formula of S in terms of (only) the undefined primitive symbols of S, and thus is always decidable in S.

In the previous chapter we argued, however, that G๖del’s reasoning does not clearly establish that the primitive recursive relation Q(x, y) of A, defined by :

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

is expressible formally as some formula Q(x, y) of S.

We now consider whether we can fill the lacuna in G๖del’s reasoning by naturally defining, for the purposes of representability and G๖del-numbering, as suggested at the end of that paper :

(i)    Sb(y : (v, x)) = y ;

(ii)   Sb( x : (v, y)) = x ;

(iii)  z(y) = y ;

in case y is a free variable.

We then establish that the above inability to express every primitive recursive relation of A as a formula of S reflects the fact that not every primitive recursive relation of A is decidable [G๖del 1931 : p20 definition 31 and footnote 36] in S under such naturally extended definitions.

3-02    G๖del’s Theorems V and VI

We note firstly that, in his Theorem V, G๖del argues that every n-ary arithmetical primitive recursive relation of A is formally expressible as a formula of S, and so every such representation can be G๖del-numbered to yield a unique n-ary PREDICATE that is PROVABLE in S under suitable substitutions  [G๖del 1931 : p22-23] :

Theorem V :  For every primitive recursive relation R(x1, … , xn) there is an n-ary PREDICATE r (with the FREE VARIABLES u1, … , un) such that, for all n-tuples of numbers (x1, … , xn), we have :

R(x1, … , xn) ฎ Bew[Sb(r : ((u1, z(x1)), … , (un, z(xn))))]

~R(x1, … , xn) ฎ Bew[Neg Sb(r : ((u1, z(x1)), … , (un, z(xn))))]

In  Theorem VI, G๖del then considers the specific primitive recursive relation [G๖del 1931 : p24-26] of A :

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

and - concluding by Theorem V that  Q(x, y) can be represented by some formula Q(x, y) of S that can be G๖del-numbered by a PREDICATE q, and is a FUNCTION of the two FREE VARIABLES 17 and 19, but independent of the two free variables x and y - shows that this yields an UNDECIDABLE SENTENCE 17Genr in S such that both 17Genr and Neg(17Genr) are not PROVABLE in an  w-consistent  S :

Theorem VI :  For every w-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).

3-03    G๖del’s reasoning in Theorem VI

(a)   Now, G๖del’s Theorem V allows him to conclude that there is a PREDICATE  q (which is a FUNCTION of the two FREE VARIABLES 17 and 19) such that the relations :

~ [xB[Sb(y : (19, z(y)))]] ฎ Bew[Sb(q : ((17, z(x)), (19, z(y))))]

xB[Sb(y : (19, z(y)))] ฎ Bew[Neg Sb(q : ((17, z(x)), (19, z(y))))]

hold in A for all pairs of values (x, y).

(b)   He can thus validly define p as the CLASS EXPRESSION with the FREE VARIABLE 19 by :

p = 17Genq,

and r as the primitive recursive CLASS EXPRESSION with the FREE VARIABLE 17 by :

r = Sb(q : (19, z(p))).

(c)   He reasons from these definitions that :

Sb(p : (19, z(p))) = Sb((17Genq) : (19, z(p)))

= 17Gen[Sb(q : (19, z(p)))]

= 17Genr

Sb(q : ((17, z(x)), (19, z(p))))

  = Sb(r : (17, z(x))).

(d)   Substituting p for y in Q(x, y), he uses Theorem V as above and various substitutions to conclude that the relations :

~ [xB(17Genr)] ฎ Bew[Sb(r : (17, z(x)))]

xB(17Genr) ฎ Bew[Neg Sb(r : (17, z(x)))]

hold in A for all values of x.

From the above G๖del finally concludes, meta-mathematically, that 17Genr and Neg(17Genr) are not PROVABLE [G๖del 1931 : p25-26] in an w-consistent S, and so 17Genr is UNDECIDABLE in S.

3-04    Implicit assumptions underlying G๖del’s meta-proof of Theorem VI

A feature of G๖del’s meta-reasoning in the above, critical for establishing that Neg(17Genr) is not PROVABLE [G๖del 1931 : p26(2)], is his implicit meta-assumption that a formula holds in A for every set of values of the free variables that occur in it if and only if its closure holds in A.

Also, as argued in the previous chapter, G๖del’s above reasoning rests on the (unproven) implicit assumption that the primitive recursive relation of A :

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

can be represented in S for an undetermined (free variable) y by some formal expression Q(x, y) which can be G๖del-numbered.

3-05   Is  Q(x, y) decidable

(a)   We therefore consider the weaker question of whether G๖del’s primitive recursive relation [G๖del 1931 : p24(8.1)] :

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

is alternatively decidable [G๖del 1931 : p26], which would be sufficient for his reasoning to hold.

(b)   We thus assume that there is some DECIDABLE PREDICATE q (which is a FUNCTION of the FREE VARIABLES 17 and 19, but independent of the free variables x and y) such that the following hold in A for all pairs of values (x, y) [G๖del 1931 : p25(9) & (10)] :

~ [xB[Sb(y : (19, z(y)))]] ฎ Bew[Sb(q : ((17, z(x)), (9, z(y)))]

[xB[Sb(y : (19, z(y)))]] ฎ Bew[Neg Sb(q : (17, z(x)), (19, z(y)))].

(c)   We set [cf. G๖del 1931 : p25(12)] :

r' = Sb(q: (19, z(q)))

(r' is a  primitive recursive CLASS EXPRESSION with the  FREE VARIABLE 17)

(d)   We note that [cf. G๖del 1931 : p25(13)] :

Sb(q : (17, z(x)), (19, z(q))) = Sb(r' : (17, z(x)))

(e)   Substituting q for y in ง3-05(b) above, we conclude that the following relations hold  [cf. G๖del 1931 : p25(15) & (16)] in A for all values of x :

(i)    ~ [xB (r')] ฎ Bew[Sb(r' : (17, z(x)))]

(ii)   [xB(r')] ฎ Bew[Neg Sb(r' : (17, z(x)))].

3-06    ‘r'  is provable in S’ บ M ‘r'  is not provable in S’

(a)   By the extended definitions  ง3-01(i-iii), we have that :

(i)    (x)Bew[Sb(r' : (17, z(x)))] บ (x)Bewr'  holds in A,

whence it follows that :

(ii)   (x)Bewr' บ Bewr' holds in A,

and so :

(ii)   (x)Bew[Sb(r' : (17, z(x)))] บ Bewr' holds in A.

 (This translates under interpretation as the meta-postulation by definition that a formula is provable in S for every set of values of the free variables that occur in it if and only if it is provable in S, expressed symbolically in the meta-theory  M of S by :

(x1) … (xn)├SR(x1, … , xn) บM ├SR(x1, … , xn).

(b)   We also meta-postulate explicitly that a  formula holds  in  S  for every set of  values  of the  free variables  that occur in it if and only if its  closure holds  in  S.

(  This postulate is implicitly assumed by G๖del in the meta-proof of his meta-Theorem VI  [G๖del 1931 : p26(2)]  to establish that  Neg (17Genr)  is not  PROVABLE  in  S, and is expressed symbolically in the meta-theory  M  of  S  by :

(x1) … (xn) ╟ S R(x1, … , xn)

 บM  ╟ S (x1) … (xn)R(x1, … , xn).

(c)   We then have that :

(i)         r'  is not  PROVABLE

By definition, we have that  r'  is  PROVABLE  if and only if   x B (r')  holds for some  value  of  x.

However, by ง3-05(e)(ii), we have that, if  nB(r')  holds, then  Bew [ Neg Sb ( r' : (17, z(n)) ) ]  also holds, thus contradicting the  PROVABILITY  of  r'.

Hence  x B (r')  does not hold  for any  value  of  x, and so both  Bew r'  and - by  ง3-01(i-iii)  and  ง3-06(a)  above -  (x) Bew [ Sb ( r' : (17, z(x)) ) ]  do not hold, and  r'  is not  PROVABLE.

(ii)        r'  is  PROVABLE

By  ง3-06(c)(i), we have that  r'  is not  PROVABLE, hence  ~ (x) Bew [ Sb ( r' : (17, z(x)) ) ]  holds, and  ~ x B (r')  holds  for all  values  of  x.

However, by  ง3-05(e)(i),  Bew [ Sb ( r' : (17, z(x)) ) ]  then  holds  for all  values  of  x.

Hence, by  ง3-06(b), (x) Bew [ Sb ( r' : (17, z(x)) ) ]  holds - contradicting  ง3-06(c)(i) - and so  r'  is  PROVABLE.

3-07  Conclusions

Now the meta-postulate  ง3-06(b) - crucial for the meta-proof of G๖del’s  meta-Theorem VI - is intuitively taken to  hold  in any traditional formal system such as the  Principia Mathematica.

It follows that G๖del’s  primitive recursive relation :

Q (x, y )   บ   ~ [ x B [ Sb ( y : (19, z(y)) ) ] ]

is not  decidable, and so G๖del’s  meta-Theorem VI, and its consequences, cannot be established in such  systems.

3-08.  Alternative formal structures

Some interesting consequences follow if we choose, instead, to deny the meta-postulate  ง3-06(b).

(a)   We then arrive at alternative  formal systems  S'  which contain  formulas  such as  F(x)  that are  provable  for all constructible values of  x, but where  ~ (x) F(x)  is also  provable.

(b)   Such  formal systems  S'  of  Arithmetic  would then have the richness in language needed to  formally  express a statement concerning the totality of an essentially transfinite domain of  individuals  of  S'  within  S'  without appeal to any  Platonistic  elements.

(c)   Intuitionist limitations on the postulation and use of non-finitary elements and non-constructive arguments in such  formal systems  would now apply not to the  formal system  S'  and its interpretations, but to the postulation and use of non-finitary elements and non-constructive arguments in its meta-theory  M'.

(d)   The meta-statement  ‘ ‘F(x)’  holds  in  S'  for all  values  of  x’, denoted in  M'  by  (x)╟ S F(x),  would correspond in any interpretation  A'  of such an  S'  to the intuitive denumerable compound meta-statement :

‘ ‘F(1)’  holds  in  A'’  and  ‘ ‘F(2)’  holds  in  A'’  and  ‘ ‘F(3)’  holds  in  A'’ ...

where  ‘1’, ‘2’, ‘3’, ... range over  the constructible individuals of  A'  only.

(e)   The meta-statement  ‘ ‘(x)F(x)’  holds in  S' ’, denoted in  M'  by  ╟S (x)F(x), would correspond in  A'  to the intuitive, possibly non-denumerable, compound meta-statement :

‘ ‘F(a)’  holds  in  A'’  and  ‘ ‘F(b)’  holds  in  A'’  and  ‘ ‘F(c)’  holds  in  A'’ ...

where  ‘a’, ‘b’, ‘c’, ... range over the entire, possibly non-denumerable, domain of individuals of  A'.

(f)    The equivalent meta-statements  ‘ ‘F(x)’  is  provable  in  S'  for all  values  of  x’, denoted in  M'  by  (x) ├S F(x),  and  ‘ ‘F(x)’  is  provable  in  S' ’, denoted in  M'  by  ├SF(x) would both correspond in  A'  to the intuitive denumerable compound meta-statement :

‘ ‘F(1)’  is  provable  in  A'’  and  ‘ ‘F(2)’  is  provable  in  A'’  and  ‘ ‘F(3)’  is  provable  in  A'’ ...

where  ‘1’, ‘2’, ‘3’, ... range over the constructible individuals of  A'  only.

(g)   The meta-statement  ‘ ‘(x)F(x)’  is  provable  in  S' ’, denoted in the meta-theory  M'  of  S'  by  ├S (x)F(x), however, has no obvious intuitive interpretation!

◄ 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)