Appendex 1 Natural Number Theory

Page 1


00010'Text Natural-Number;

00020'Axiom;

00030' Nat, /* Nat(x) is "x is a natural number" */

00040' 1, Pl, /* Pl(x)=x+1 */

00050' Add, /* Add(x,y)=x+y */

00060' Prd; /* Prd(x,y)=x*y */

00070'Formulae;

00080' Nat1: Nat(1); /* 1 is a natural number */

00090' Nat2: (All x)(Nat(x) imp Nat(Pl(x)));

00100' /* x+1 is a natural number if x is so */

00110' Nat3: (All x)(All y)([Pl(x)=Pl(y)] imp [x=y]);

00120' /* x+1=y+1 implies x=y */

00130' Nat4: (All x)(not[Pl(x)=1]); /* 1 is not represented by x+1 */

00140' Nat5: (All F)(F(1)and (All i)(Nat(i)and F(i) imp F(Pl(i)))

00150' imp (All j)(Nat(j) imp F(j)));

00160' /* Mathematical induction */

00170' Nat6: (All x)([Add(x,1)=Pl(x)]);

00180' Nat7: (All x)(All y)([Add(x,Pl(y))=Pl(Add(x,y))]);

00190' /* x+(y+1)=(x+y)+1 */

00200' Nat8: (All x)([Prd(x,1)=x]); /* x*1=x */

00210' Nat9: (All x)(All y)([Prd(x,Pl(y))=Add (Prd(x,y),x)]);

00220' /* x*(y+1)=x*y+x */

00230'End Axiom;

00240'Lemma; /*Pl is onto mapping to natural numbers but 1*/

00250' NaLem 1: (All x)(Nat(x) and not[x=1] imp (Exist y)(Nat(y)
and [Pl(y)=x]));

00260'Proof;

00270' a1: Put f(j)=not[j=1] imp (Exist y)(Nat(y) and [Pl(y)=j]);

00280' a2: [1=1] by EQ;

00290' a3: not[1=1] imp (Exist y)(Nat(y)and[Pl(y)=1]) by LOGIC(a2);

00300' a4: f(1) by FUNF(a1,a3);

00310' a5: (All i)(;

00320' a6: Nat(i) and f(i) imp;

00330' a7: not[Pl(i)=1] imp;

00340' a8: [Pl(i)=Pl(i)] by EQ;

00350' a9: Nat(i) and [Pl(i)=Pl(i)] by LOGIC(a6,a8);

00360' imp (Exist y)(Nat(y) and [Pl(y)=Pl(i)]) by EXIST(a9);

00370' imp f(Pl(i)) by FUNF(a1,a7);

00380' );