1  2  3  4  5  6

The following proposition is an exact expression of a fact which can be vaguely formulated in this way: every recursive relation is definable in the system P (interpreted as to content), regardless of what interpretation is given to the formulae of P:

Proposition V: To every recursive relation R(x₁ … x_n) there corresponds an n-place relation-sign r (with the free variables³⁸ u₁, u₂, … u_n) such that for every n-tuple of numbers (x₁ … x_n) the following hold:

  R(x₁ … x_n) ® Bew{Sb[r (u₁ … u_n)|(Z(x₁) … Z(x_n)]} (3)
~R(x₁ … x_n) ® Bew{Neg Sb[r (u₁ … u_n)|(Z(x₁) … Z(x_n)]} (4)

We content ourselves here with indicating the proof of this proposition in outline, since it offers no difficulties of principle and is somewhat involved.³⁹ We prove the proposition for all relations R(x₁ … x_n) of the form: x₁ = f(x₂ … x_n)⁴⁰ (where f is a recursive function) and apply mathematical induction on the degree of f. For functions of the first degree (i.e. constants and the function x+1) the proposition is trivial. Let f then be of degree m. It derives from functions of lower degree f₁ … f_k by the operations of substitution or recursive definition. Since, by the inductive assumption, everything is already proved for f₁ … f_k, there exist corresponding relation-signs r₁ … r_k such that (3) and (4) hold. The processes of definition whereby f is derived from f₁ … f_k (substitution and re-

[187]

cursive definition) can all be formally mapped in the system P. If this is done, we obtain from r₁ … r_k a new relation-sign r⁴¹, for which we can readily prove the validity of (3) and (4) by use of the inductive assumption. A relation-sign r, assigned in this fashion to a recursive relation,⁴² will be called recursive.

We now come to the object of our exercises:
Let c be any class of formulae. We denote by Flg(c) (set of consequences of c) the smallest set of formulae which contains all the formulae of c and all axioms, and which is closed with respect to the relation "immediate consequence of". c is termed w-consistent, if there is no class-sign a such that:

(n)[Sb(a v|Z(n)) Î Flg(c)] & [Neg(v Gen a)] Î Flg(c)

where v is the free variable of the class-sign a.

Every w-consistent system is naturally also consistent. The converse, however, is not the case, as will be shown later.

The general result as to the existence of undecidable propositions reads:

Proposition VI: To every w-consistent recursive class c of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(c) (where v is the free variable of r).

Proof: Let c be any given recursive w-consistent class of formulae. We define:

Bw_c(x) º (n)[n £ l(x) ® Ax(n Gl x) Ú (n Gl x) Î c Ú (Ep,q){0 < p,q < n & Fl(n Gl x, p Gl x, q Gl x)}] & l(x) > 0 (5)

(cf. the analogous concept 44)

x B_c y º Bw_c(x) & [l(x)] Gl x = y (6)

Bew_c(x) º ($y)y B_c x (6.1)

(cf. the analogous concepts 45, 46)

The following clearly hold:

(x)[Bew_c(x) º x Î Flg(c)] (7)

(x)[Bew(x) ® Bew_c(x)] (8)

[188]

We now define the relation:

Q(x,y) º ~{x B_c[Sb(y 19|z(y))]}. (8.1)

Since x B_c y [according to (6), (5)] and Sb(y 19|Z(y)) (according to definitions 17, 31) are recursive, so also is Q(x,y). According to Proposition V and (8) there is therefore a relation-sign q (with the free variables 17, 19) such that

~{x B_c [Sb(y 19|Z(y))]} ® Bew_c[Sb(q 17|Z(x) 19|Z(y))]. (9)

x B_c [Sb(y 19|Z(y))] ® Bew_c[Neg Sb(q 17|Z(x) 19|Z(y))]. (10)

We put

p = 17 Gen q (11)
(p is a class-sign with the free variable 19)

and

r = Sb(q 19|Z(p)) (12)
(r is a recursive class-sign with the free variable 17).⁴³

Then

Sb(p 19|Z(p)) (13)

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

= 17 Gen Sb(q 19|z(p))

= 17 Gen r⁴⁴

[because of (11) and (12)] and furthermore:

Sb(q 17|Z(x) 19|Z(p)) = Sb(r 17|Z(x)) (14)

[according to (12)]. If now in (9) and (10) we substitute p for y, we find, in virtue of (13) and (14):

x B_c (17 Gen r) ® Bew_c[Sb(r 17|Z(x))] (15)

x B_c (17 Gen r) ® Bew_c[Neg Sb(r 17|Z(x))] (16)

[189]

Hence:

1. 17 Gen r is not c-provable.⁴⁵ For if that were so, there would (according to 6.1) be an n such that n B_c (17 Gen r). By (16) it would therefore be the case that:

Bew_c[Neg Sb(r 17|Z(n))]

while–on the other hand–from the c-provability of 17 Gen r there follows also that of Sb(r 17|Z(n)). c would therefore be inconsistent (and, a fortiori, w-inconsistent).

2. Neg(17 Gen r) is not c-provable. Proof: As shown above, 17 Gen r is not c-provable, i.e. (according to 6.1) the following holds: (n) n B_c(17 Gen r). Whence it follows, by (15), that (n) Bew_c[Sb(r 17|Z(n))], which together with Bew_c[Neg(17 Gen r)] would conflict with the w-consistency of c.

Neg(17 Gen r) is therefore undecidable in c, so that Proposition VI is proved.

One can easily convince oneself that the above proof is constructive,^45a i.e. that the following is demonstrated in an intuitionistically unobjectionable way: Given any recursively defined class c of formulae: If then a formal decision (in c) be given for the (effectively demonstrable) propositional formula 17 Gen r, we can effectively state:

1. A proof for Neg(17 Gen r).

2. For any given n, a proof for Sb(r 17|Z(n)), i.e. a formal decision of 17 Gen r would lead to the effective demonstrability of an w-inconsistency.

We shall call a relation (class) of natural numbers R(x₁ … x_n) calculable [entscheidungsdefinit], if there is an n-place relation-sign r such that (3) and (4) hold (cf. Proposition V). In particular, therefore, by Proposition V, every recursive relation is calculable. Similarly, a relation-sign will be called calculable, if it be assigned in this manner to a calculable relation. It is, then, sufficient for the existence of undecidable propositions, to assume of the class c that it is w-consistent and calculable. For the property of being calculable carries over from c to x B_c y (cf. (5), (6))

[190]

and to Q(x,y) (cf. 8.1), and only these are applied in the above proof. The undecidable proposition has in this case the form v Gen r, where r is a calculable class-sign (it is in fact enough that c should be calculable in the system extended by adding c).

If, instead of w-consistency, mere consistency as such is assumed for c, then there follows, indeed, not the existence of an undecidable proposition, but rather the existence of a property (r) for which it is possible neither to provide a counter-example nor to prove that it holds for all numbers. For, in proving that 17 Gen r is not c-provable, only the consistency of c is employed (cf. [189]) and from ~Bew_c(17 Gen r) it follows, according to (15), that for every number x, Sb(r 17|z(x)) is c-provable, and hence that Sb(r 17|Z(x)) is not c-provable for any number.

By adding Neg(17 Gen r) to c, we obtain a consistent but not w-consistent class of formulae c'. c' is consistent, since otherwise 17 Gen r would be c-provable. c' is not however w-consistent, since in virtue of ~Bew_c(17 Gen r) and (15) we have: (x) Bew_cSb(r 17|Z(x)), and so a fortiori: (x) Bew_c'Sb(r 17|Z(x)), and on the other hand, naturally: Bew_c'[Neg(17 Gen r)].⁴⁶

A special case of Proposition VI is that in which the class c consists of a finite number of formulae (with or without those derived therefrom by type-lift). Every finite class a is naturally recursive. Let a be the largest number contained in a. Then in this case the following holds for c:

x Î c º ($m,n)[m £ x & n £ a & n Î a & x = m Th n]

c is therefore recursive. This allows one, for example, to conclude that even with the help of the axiom of choice (for all types), or the generalized continuum hypothesis, not all propositions are decidable, it being assumed that these hypotheses are w-consistent.

In the proof of Proposition VI the only properties of the system P employed were the following:

1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).

2. Every recursive relation is definable in the system P (in the sense of Proposition V).

Hence in every formal system that satisfies assumptions 1 and 2 and is w-consistent, undecidable propositions exist of the form (x) F(x), where F is a recursively defined property of natural numbers, and so too in every extension of such

[191]

a system made by adding a recursively definable w-consistent class of axioms. As can be easily confirmed, the systems which satisfy assumptions 1 and 2 include the Zermelo-Fraenkel and the v. Neumann axiom systems of set theory,⁴⁷ and also the axiom system of number theory which consists of the Peano axioms, the operation of recursive definition [according to schema (2)] and the logical rules.⁴⁸ Assumption 1 is in general satisfied by every system whose rules of inference are the usual ones and whose axioms (like those of P) are derived by substitution from a finite number of schemata.^48a

¹⁶ The addition of the Peano axioms, like all the other changes made in the system PM, serves only to simplify the proof and can in principle be dispensed with.

¹⁷ It is presupposed that for every variable type denumerably many signs are available.

¹⁸ Unhomogeneous relations could also be defined in this manner, e.g. a relation between individuals and classes as a class of elements of the form: ((x₂),((x₁),x₂)). As a simple consideration shows, all the provable propositions about relations in PM are also provable in this fashion.

^18a Thus x " (a) is also a formula if x does not occur, or does not occur free, in a. In that case x " (a) naturally means the same as a.

¹⁹ With regard to this definition (and others like it occurring later), cf. J. Lukasiewicz and A. Tarski, 'Untersuchungen über den Aussagenkalkül', Comptes Rendus des séances de la Soeiété des Sciences et des Lettres de Varsovie XXIII, 1930, Cl. 111.

²⁰ Where v does not occur in a as a free variable, we must put Subst a(v|b) = a. Note that "Subst" is a sign belonging to metamathematics.

²¹ As in PM I, *13, x₁ = y₁ is to be thought of as defined by x₂ " (x₂(x₁) É x₂(y₁)) (and similarly for higher types.)

²² To obtain the axioms from the schemata presented (and in the cases of II, III and IV, after carrying out the permitted substitutions), one must therefore still

1. eliminate the abbreviations
2. add the suppressqd brackets.

Note that the resultant expressions must be "formulae" in the above sense. (Cf. also the exact definitions of the metamathematical concepts on [182]ff.)

²³ c is therefore either a variable or 0 or a sign of the form ¦ … ¦_u where u is either 0 or a variable of type 1. With regard to the concept "free (bound) at a place in a" cf. section I A5 of the work cited in footnote 24.

²⁴ The rule of substitution becomes superfluous, since we have already dealt with all possible substitutions in the axioms themselves (as is also done in J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927).

²⁵ I.e. its field of definition is the class of non-negative whole numbers (or n-tuples of such), respectively, and its values are non-negative whole numbers.

²⁶ In what follows, small italic letters (with or without indices) are always variables for non-negative whole numbers (failing an express statement to the contrary). [Italics omitted.]

²⁷ More precisely, by substitution of certain of the foregoing functions in the empty places of the preceding, e.g. f_k(x₁,x₂) = f_p[f_q(x₁,x₁),f_r(x₂)] (p, q, r ‹ k). Not all the variables on the left-hand side must also occur on the right (and similarly in the recursion schema (2)).

²⁸ We include classes among relations (one-place relations). Recursive relations R naturally have the property that for every specific n-tuple of numbers it can be decided whether R(x₁…x_n) holds or not.

²⁹ For all considerations as to content (more especially also of a metamathematical kind) the Hilbertian symbolism is used, cf. Hilbert-Ackermann, Grundzüge der theoretischen Logik, Berlin 1928.

³⁰ We use [greek] letters c, h, as abbreviations for given n-tuple sets of variables, e.g. x₁, x₂ … x_n.

³¹ We take it to be recognized that the functions x+y (addition) and x.y (multiplication) are recursive.

³² a cannot take values other than 0 and 1, as is evident from the definition of a.

³³ The sign º is used to mean "equivalence by definition", and therefore does duty in definitions either for = or for ~ [not the negation symbol] (otherwise the symbolism is Hilbertian).

³⁴ Wherever in the following definitions one of the signs (x), ($x), ex occurs, it is followed by a limitation on the value of x. This limitation merely serves to ensure the recursive nature of the concept defined. (Cf. Proposition IV.) On the other hand, the range of the defined concept would almost always remain unaffected by its omission.

^34a For 0 < n £ z, where z is the number of distinct prime numbers dividing into x. Note that for n = z+1, n Pr x = 0.

^34b m,n £ x stands for: m £ x & n £ x (and similarly for more than two variables).

³⁵ The limitation n £ (Pr[l(x)]^2x.[l(x)]2 means roughly this: The length of the shortest series of formulae belonging to x can at most be equal to the number of constituent formulae of x. There are however at most l(x) constituent formulae of length 1, at most l(x)-1 of length 2, etc. and in all, therefore, at most ¹¤₂[l(x){l(x)+1}] £ [l(x)]². The prime numbers in n can therefore all be assumed smaller that Pr{[l(x)]²}, their number £[l(x)]² and their exponents (which are constituent formulae of x) £x.

³⁶ Where v is not a variable or x not a formula, then Sb(x v|y) = x.

³⁷ Instead of Sb[Sb[x v|y] z|y] we write: Sb(x v|y w|z) (and similarly for more than two variables).

³⁸ The variables u₁ … u_n could be arbitrarily allotted. There is always, e.g., an r with the free variables 17, 19, 23 … etc., for which (3) and (4) hold.

³⁹ Proposition V naturally is based on the fact that for any recursive relation R, it is decidable, for every n-tuple of numbers, from the axioms of the system P, whether the relation R holds or not.

⁴⁰ From this there follows immediately its validity for every recursive relation, since any such relation is equivalent to 0 = f(x₁ … x_n), where f is recursive.

⁴¹ In the precise development of this proof, r is naturally defined, not by the roundabout route of indicating its content, but by its purely formal constitution.

⁴² Which thus, as regards content, expresses the existence of this relation.

⁴³ r is derived in fact, from the recursive relation-sign q on replacement of a variable by a determinate number (p).

⁴⁴ The operations Gen and Sb are naturally always commutative, wherever they refer to different variables.

⁴⁵ "x is c-provable" signifies: x Î Flg(c), which, by (7), states the same as Bew_c(x).

^45a Since all existential assertions occurring in the proof are based on Proposition V, which, as can easily be seen, is intuitionistically unobjectionable.

⁴⁶ Thus the existence of consistent and not w-consistent c's can naturally be proved only on the assumption that, in general, consistent c's do exist (i.e. that P is consistent).

⁴⁷ The proof of assumption 1 is here even simpler than that for the system P, since there is only one kind of basic variable (or two for J. v. Neumann).

⁴⁸ Cf. Problem III in D. Hilbert's lecture: 'Probleme der Grundlegung der Mathematik', Math. Ann. 102.

^48a The true source of the incompleteness attaching to all formal systems of mathematics, is to be found–as will be shown in Part II of this essay–in the fact that the formation of ever higher types can be continued into the transfinite (cf. D. Hilbert 'Über das Unendliche', Math. Ann. 95, p. 184), whereas in every formal system at most denumerably many types occur. It can be shown, that is, that the undecidable propositions here presented always become decidable by the adjunction of suitable higher types (e.g. of type w for the system P). A similar result also holds for the axiom system of set theory.

Revista Matemáticas, Educación e Internet^â
Derechos Reservados