1  2  3  4  5  6

[182]

1.

x/y º ($z)[z £ x & x = y.z]³³

x is divisible by y.³⁴

2.

Prim(x) º ~($z)[z £ x & z ¹ 1 & z ¹ x & x/z] & x > 1

x is a prime number.

3.

0 Pr x º 0
(n+1) Pr x º ey [y £ x & Prim(y) & x/y & y > n Pr x]

n Pr x is the n-th (in order of magnitude) prime number contained in x.^34a

4.

0! º 1
(n+1)! º (n+1).n!

5.

Pr(0) º 0
Pr(n+1) º ey [y £ {Pr(n)}! + 1 & Prim(y) & y > Pr(n)]

Pr(n) is the n-th prime number (in order of magnitude).

6.

n Gl x º ey [y £ x & x/(n Pr x)^y & not x/(n Pr x)^y+1]

n Gl x is the n-th term of the series of numbers assigned to the number x (for n > 0 and n not greater than the length of this series).

7.

l(x) º ey [y £ x & y Pr x > 0 & (y+1) Pr x = 0]

l(x) is the length of the series of numbers assigned to x.

8.

x * y º ez [z £ [Pr{l(x)+l(y)}]^x+y & (n)[n £ l(x) ® n Gl z = n Gl x] & (n)[0 < n £ l(y) ® {n+l(x)} Gl z = n Gl y]]

 x * y corresponds to the operation of "joining together" two finite series of numbers.

9.

R(x) º 2^x

R(x) corresponds to the number-series consisting only of the number x (for x > 0).

10.

E(x) º R(11) * x * R(13)

E(x) corresponds to the operation of "bracketing" [11 and 13 are assigned to the basic signs "(" and ")"].

11.

n Var x º ($z)[13 < z £ x & Prim(z) & x = zⁿ] & n ¹ 0

x is a variable of n-th type.

12.

Var(x) º ($n)[n £ x & n Var x]

x is a variable.

13.

Neg(x) º R(5) * E(x)

Neg(x) is the negation of x.

[183]

14.

x Dis y º E(x) * R(7) * E(y)

x Dis y is the disjunction of x and y.

15.

x Gen y º R(x) * R(9) * E(y)

x Gen y is the generalization of y by means of the variable x (assuming x is a variable).

16.

0 N x º x
(n+1) N x º R(3) * n N x

n N x corresponds to the operation: "n-fold prefixing of the sign '¦' before x."

17.

Z(n) º n N [R(1)]

Z(n) is the number-sign for the number n.

18.

Typ₁'(x) º ($m,n){m,n £ x & [m = 1 Ú 1 Var m] & x = n N [R(m)]}^34b

x is a sign of first type.

19.

Typ_n(x) º [n = 1 & Typ₁'(x)] Ú [n > 1 & ($v){v £ x & n Var v & x = R(v)}]

x is a sign of n-th type.

20.

Elf(x) º ($y,z,n)[y,z,n £ x & Typ_n(y) & Typ_n+1(z) & x = z * E(y)]

x is an elementary formula.

21.

Op(x,y,z) º x = Neg(y) Ú x = y Dis z Ú ($v)[v £ x & Var(v) & x = v Gen y]

22.

FR(x) º (n){0 < n £ l(x) ® Elf(n Gl x) Ú ($p,q)[0 < p,q < n & Op(n Gl x,p Gl x,q Gl x)]} & l(x) > 0

x is a series of formulae of which each is either an elementary formula or arises from those preceding by the operations of negation, disjunction and generalization.

23.

Form(x) º ($n){n £ (Pr[l(x)²])^x.[l(x)]2 & FR(n) & x = [l(n)] Gl n}³⁵

x is a formula (i.e. last term of a series of formulae n).

24.

v Geb n,x º Var(v) & Form(x) & ($a,b,c)[a,b,c £ x & x = a * (v Gen b) * c & Form(b) & l(a)+1 £ n £ l(a)+l(v Gen b)]

The variable v is bound at the n-th place in x.

[184]

25.

v Fr n,x º Var(v) & Form(x) & v = n Gl x & n £ l(x) & not(v Geb n,x)

The variable v is free at the n-th place in x.

26.

v Fr x º ($n)[n £ l(x) & v Fr n,x]

v occurs in x as a free variable.

27.

Su x(n|y) º ez {z £ [Pr(l(x)+l(y))]^x+y & [($u,v)u,v £ x & x = u * R(b Gl x) * v & z = u * y * v & n = l(u)+1]}

Su x(n|y) derives from x on substituting y in place of the n-th term of x (it being assumed that 0 < n £ l(x)).

28.

0 St v,x º en {n £ l(x) & v Fr n,x & not ($p)[n < p £ l(x) & v Fr p,x]}
(k+1) St v,x º en {n < k St v,x & v Fr n,x & ($p)[n < p < k St v,x & v Fr p,x]}

k St v,x is the (k+1)-th place in x (numbering from the end of formula x) at which v is free in x (and 0, if there is no such place.)

29.

A(v,x) º en {n £ l(x) & n St v = 0}

A(v,x) is the number of places at which v is free in x.

30.

Sb₀(x v|y) º x

Sb_k+1(x v|y) º Su[Sb_k(x v|y)][(k St v, x)|y)]

31.

Sb(x v|y) º Sb_A(v,x)(x v|y)³⁶

Sb(x v|y) is the concept Subst a(v|b), defined above.³⁷

32.

x Imp y º [Neg(x)] Dis y
x Con y º Neg{[Neg(x)] Dis [Neg(y)]}
x Aeq y º (x Imp y) Con (y Imp x)
v Ex y º Neg{v Gen [Neg(y)]}

33.

n Th x º en {y £ x^(xn) & (k) £ l(x) ® (k Gl x £ 13 & k Gl y = k Gl x) Ú (k Gl x > 13 & k Gl y = k Gl x.[1 Pr(k Gl x)]ⁿ)]}

n Th x is the n-th type-lift of x (in the case when x and n Th x are formulae).

To the axioms I, 1 to 3, there correspond three determinate numbers, which we denote by z₁, z₂, z₃, and we define:

34.

Z–Ax(x) º (x = z₁ Ú x = z₂ Ú x = z₃)

[185]

35.

A₁-Ax(x) º ($y)[y £ x & Form(y) & x = (y Dis y) Imp y]

x is a formula derived by substitution in the axiom-schema II, 1. Similarly A₂-Ax, A₃-Ax, A₄-Ax are defined in accordance with the axioms II, 2 to 4.

36.

A-Ax(x) º A₁-Ax(x) Ú A₂-Ax(x) Ú A₃-Ax(x) Ú A₄-Ax(x)

x is a formula derived by substitution in an axiom of the sentential calculus.

37.

Q(z,y,v) º ($n,m,w)[n £ l(y) & m £ l(z) & w £ z & w = m Gl x & w Geb n,y & v Fr n,y]

z contains no variable bound in y at a position where v is free.

38.

L₁-Ax(x) º ($v,y,z,n){v,y,z,n £ x & n Var v & Typ_n(z) & Form(y) & Q(z,y,v) & x = (v Gen y) Imp [Sb(v|z)]}

x is a formula derived from the axiom-schema III, 1 by substitution.

39.

L₂-Ax(x) º ($v,q,p){v,q,p £ x & Var(v) & Form(p) & v Fr p & Form(q) & x = [v Gen (p Dis q)] Imp [p Dis (v Gen q)]}

x is a formula derived from the axiom-schema III, 2 by substitution.

40.

R-Ax(x) º ($u,v,y,n)[u, v, y, n £ x & n Var v & (n+1) Var u & u Fr y & Form(y) & x = u $x {v Gen [[R(u)*E(R(v))] Aeq y]}]

x is a formula derived from the axiom-schema IV, 1 by substitution.

To the axiom V, 1 there corresponds a determinate number z₄ and we define:

41.

M-Ax(x) º ($n)[n £ x & x = n Th z₄]

42.

Ax(x) º Z-Ax(x) Ú A-Ax(x) Ú L₁-Ax(x) Ú L₂-Ax(x) Ú R-Ax(x) Ú M-Ax(x)

x is an axiom.

43.

Fl(x y z) º y = z Imp x Ú ($v)[v £ x & Var(v) & x = v Gen y]

x is an immediate consequence of y and z.

[186]

44.

Bw(x) º (n){0 < n £ l(x) ® Ax(n Gl x) Ú ($p,q)[0 < p,q < n & Fl(n Gl x, p Gl x, q Cl x)]} & l(x) > 0

x is a proof-schema (a finite series of formulae, of which each is either an axiom or an immediate consequence of two previous ones).

45.

x B y º Bw(x) & [l(x)] Gl x = y

x is a proof of the formula y.

46.

Bew(x) = (Ey)y B x

x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.]

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