In Axiom blocks, we register new names and related formulas between themselves to computers. Figure A shows such formality. Marking off with commas (,), we line with new names that are going to be registered after the Axiom. This will be the declaration of names. Figure A states a proposition Nat that indicates "x is a natural number", number 1, a function P1 that makes a number x corresponds with the next number (number+1), 2 variables of Add that signifies addition, and a function Prod that shows multiplication. Except 1, these are used functionally as Add(x,y); however, here, we will only write name parts. Furthermore, in special cases, even when new names do not come up, we sometimes want to only register new relations. In that case, it is acceptable to leave a part of a name statement line blank. Therefore, writing Axiom ; ; is enough.
After it says Formulae ; relations are written every line with labels. There are no restrictions on the number of lines permitted. These formulas are registered to systems and cited with labels later on when needed. For instance, in figure A, a formula such as:
is quoted by label Nat2. Furthermore, this formula means "for all x, if Nat(x) is true, then Nat(P1(x)) is also true".
After writing relations over some lines, put down End Axiom ; and finish this part of the axiom (Axiom block).
It is probably true that there should not be many axiom in one mathematical theory. Even when new names must be declared, many times only the definition is prepared instead of the axiom. Concerning the axiom, an explanation is provided through 2.6-2.10; roughly, when new names can be made by combining old names, it is acceptable to just use the definition rather than the axiom. As a qualifier of certain conditions, the axiom is only used for prescribing new names equationally.
Furthermore, for figure A, the citation is written in the text. The quotation is indicated between /* and /*. Between these symbols, other than */, optional letter lines can be written. The use of quotation is needed like the computer programming to make the texts easier to read.
00010 'Text Natural-Number;
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 */
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]);
00135 ' /* 1 is not represented by x+1 */
00140 ' Nat5: (All F)(F(1)and (All i)(Nat(i)and F(i)
00150 ' imp F(PL(i))) 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 ' NaLem1: (All x)(Nat(x) and not[x=1] imp
00255 ' (Exist y)(Nat(y) and [PL(y)=x]));
Figure A The axiom of the natural number theory, Peano