1  2  3  4  5  6

2

We proceed now to the rigorous development of the proof sketched above, and begin by giving an exact description of the formal system P, for which we seek to demonstrate the existence of undecidable propositions. P is essentially the system obtained by superimposing on the Peano axioms the logic of PM¹⁶ (numbers as individuals, relation of successor as undefined basic concept).

The basic signs of the system P are the following:

I. Constants: "~" (not), "Ú" (or), """ (for all), "0" (nought), "¦" (the successor of), "(", ")" (brackets).

II. Variables of first type (for individuals, i.e. natural numbers including 0): "x₁", "y₁", "z₁", …

Variables of second type (for classes of individuals): "x₂", "y₂", "z₂", …

Variables of third type (for classes of classes of individuals): "x₃", "y₃", "z₃", …

and so on for every natural number as type.¹⁷

Note: Variables for two-termed and many-termed functions (relations) are superfluous as basic signs, since relations can be defined as classes of ordered pairs and ordered pairs again as classes of classes, e.g. the ordered pair a,b by ((a),(a,b)), where (x,y) means the class whose only elements are x and y, and (x) the class whose only element is x.¹⁸

[177]

By a sign of first type we understand a combination of signs of the form:

a, ¦a, ¦¦a, ¦¦¦a … etc.

where a is either 0 or a variable of first type. In the former case we call such a sign a number-sign. For n > 1 we understand by a sign of n-th type the same as variable of n-th type. Combinations of signs of the form a(b), where b is a sign of n-th and a a sign of (n+1)-th type, we call elementary formulae. The class of formulae we define as the smallest class¹⁹ containing all elementary formulae and, also, along with any a and b the following: ~(a), (a)Ú(b), x"(a) (where x is any given variable).^18a We term (a)Ú(b) the disjunction of a and b, ~(a) the negation and (a)Ú(b) a generalization of a. A formula in which there is no free variable is called a propositional formula (free variable being defined in the usual way). A formula with just n free individual variables (and otherwise no free variables) we call an n-place relation-sign and for n = 1 also a class-sign.

By Subst a(v|b) (where a stands for a formula, v a variable and b a sign of the same type as v) we understand the formula derived from a, when we replace v in it, wherever it is free, by b.²⁰ We say that a formula a is a type-lift of another one b, if a derives from b, when we increase by the same amount the type of all variables appearing in b.

The following formulae (I-V) are called axioms (they are set out with the help of the customarily defined abbreviations: ., É, º, ($x), =,²¹ and subject to the usual conventions about omission of brackets)²²:

I.

1. ~(¦x₁ = 0)
2. ¦x₁ = ¦y₁ É x₁ = y₁
3. x₂(0).x₁ " (x₂(x₁) É x₂(fx₁)) É x₁ " (x₂(x₁))

[178]

II. Every formula derived from the following schemata by substitution of any formulae for p, q and r.

1. p Ú p É p
2. p É p Ú q
3. p Ú q É q Ú p
4. (p É q) É (r Ú p É r Ú q)

III. Every formula derived from the two schemata

1. v " (a) Ú Subst a(v|c)
2. v " (b É a) Ú b É v " (a)

by making the following substitutions for a, v, b, c (and carrying out in I the operation denoted by "Subst"): for a any given formula, for v any variable, for b any formula in which v does not appear free, for c a sign of the same type as v, provided that c contains no variable which is bound in a at a place where v is free.²³

IV. Every formula derived from the schema

1. ($u)(v " (u(v) º a))

on substituting for v or u any variables of types n or n + 1 respectively, and for a a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).

V. Every formula derived from the following by type-lift (and this formula itself):

1. x₁ " (x₂(x₁) º y₂(x₁)) Ú x₂ = y₂.

This axiom states that a class is completely determined by its elements.

A formula c is called an immediate consequence of a and b, if a is the formula (~(b)) Ú (c), and an immediate consequenee of a, if c is the formula v " (a), where v denotes any given variable. The class of provable formulae is defined as the smallest class of formulae which contains the axioms and is closed with respect to the relation "immediate consequence of".²⁴

The basic signs of the system P are now ordered in one-to-one correspondence with natural numbers, as follows:

[179]

"0" … 1
"¦" … 3
"~" … 5
"Ú" … 7
""" … 9
"(" … 11
")" … 13

Furthermore, variables of type n are given numbers of the form pⁿ (where p is a prime number > 13). Hence, to every finite series of basic signs (and so also to every formula) there corresponds, one-to-one, a finite series of natural numbers. These finite series of natural numbers we now map (again in one-to-one correspondence) on to natural numbers, by letting the number 2ⁿ₁, 3ⁿ₂ … p_kⁿ_k correspond to the series n₁, n₂, … n_k, where p_k denotes the k-th prime number in order of magnitude. A natural number is thereby assigned in one-to-one correspondence, not only to every basic sign, but also to every finite series of such signs. We denote by F(a) the number corresponding to the basic sign or series of basic signs a. Suppose now one is given a class or relation R(a₁,a₂,…a_n) of basic signs or series of such. We assign to it that class (or relation) R'(x₁,x₂,…x_n) of natural numbers, which holds for x₁, x₂, … x_n when and only when there exist a₁, a₂, … a_n such that x_i=F(a_i) (i=1,2,…n) and R(a₁,a₂,…a_n) holds. We represent by the same words in italics those classes and relations of natural numbers which have been assigned in this fashion to such previously defined metamathematical concepts as "variable", "formula", "propositional formula", "axiom", "provable formula", etc. The proposition that there are undecidable problems in the system P would therefore read, for example, as follows: There exist propositional formulae a such that neither a nor the negation of a are provable formulae.

We now introduce a parenthetic consideration having no immediate connection with the formal system P, and first put forward the following definition: A number-theoretic function²⁵ f(x₁,x₂,…x_n) is said to be recursively defined by the number-theoretic functions y(x₁,x₂,…x_n-1) and m(x₁,x₂,…x_n+1), if for all x₂, … x_n, k²⁶ the following hold:

f(0,x₂,…x_n) = y(x₂,…x_n)
f(k+1,x₂,…x_n) = m(k,f(k,x₂,…x_n),x₂,…x_n). (2)

A number-theoretic function f is called recursive, if there exists a finite series of number-theoretic functions f₁, f₂, … f_n which ends in f and has the property that every function f_k of the series is either recursively defined

[180]

by two of the earlier ones, or is derived from any of the earlier ones by substitution,²⁷ or, finally, is a constant or the successor function x+1. The length of the shortest series of f_i, which belongs to a recursive function f, is termed its degree. A relation R(x₁,x₂,…x_n) among natural numbers is called recursive,²⁸ if there exists a recursive function f(x₁,x₂,…x_n) such that for all x₁, x₂, … x_n

R(x₁,x₂,…x_n) º [f(x₁,x₂,…x_n) = 0]²⁹.

The following propositions hold:

I. Every function (or relation) derived from recursive functions (or relations) by the substitution of recursive functions in place of variables is recursive; so also is every function derived from recursive functions by recursive definition according to schema (2).

II. If R and S are recursive relations, then so also are ~R, R Ú S (and therefore also R & S).

III. If the functions f(c) and y(h) are recursive, so also is the relation: f(c) = y(h).³⁰

IV. If the function f(c) and the relation R(x,h) are recursive, so also then are the relations S, T

S(c,h) ~ ($x)[x £ f(c) & R(x,h)]
T(c,h) ~ (x)[x £ f(c) ® R(x,h)]

and likewise the function y

y(c,h) = ex [x £ f(c) & R(x,h)]

where ex F(x) means: the smallest number x for which F(x) holds and 0 if there is no such number.

Proposition I follows immediately from the definition of "recursive". Propositions II and III are based on the readily ascertainable fact that the number-theoretic functions corresponding to the logical concepts ~, Ú, =

a(x), b(x,y), g(x,y)

namely

a(0) = 1; a(x) = 0 for x ¹ 0
b(0,x) = b(x,0) = 0; b(x,y) = 1, if x, y both ¹ O

[181]

g(x,y) = 0, if x = y; g(x,y) = 1, if x ¹ y

are recursive. The proof of Proposition IV is briefly as follows: According to the assumption there exists a recursive r(x,h) such that

R(x,h) º [r(x,h) = 0].

We now define, according to the recursion schema (2), a function C(x,h) in the following manner:

C(0,h) = 0

C(n+1,h) = (n+1).a + C(n,h).a(a)³¹

where

a = a[a(r(0,h))].a[r(n+1,h)].a[C(n,h)].

C(n+1,h) is therefore either = n+1 (if a = 1) or = C(n,h) (if a = 0).³² The first case clearly arises if and only if all the constituent factors of a are 1, i.e. if

~R(O,h) & R(n+1,h) & [C(n,h) = 0].

From this it follows that the function C(n,h) (considered as a function of n) remains 0 up to the smallest value of n for which R(n,h) holds, and from then on is equal to this value (if R(0,h) is already the case, the corresponding C(x,h) is constant and = 0). Therefore:

y(c,h) = C(f(c),h)
S(c,h) º R[y(c,h)),h)]

The relation T can be reduced by negation to a case analogous to S, so that Proposition IV is proved.

The functions x+y, x.y, x^y, and also the relations x ‹ y, x = y are readily found to be recursive; starting from these concepts, we now define a series of functions (and relations) 1-45, of which each is defined from the earlier ones by means of the operations named in Propositions I to IV. This procedure, generally speaking, puts together many of the definition steps permitted by Propositions I to IV. Each of the functions (relations) 1-45, containing, for example, the concepts "formula", "axiom", and "immediate consequence", is therefore recursive.

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