2.7 Definition Blocks and Put Blocks


Definition is an important concept like axiom and theory. However, in the case of demonstrating a concept that is only used in demonstrating a certain theory, its importance is thought to be a rank lower. In THEAX, the former definition is done by a definition block (<def.block>), and the latter definition is done by a Put block (<Put.block>). However, they are essentially the same. Definition blocks are structured by some Put blocks. Also, when definitions are done by definition blocks, they are accepted throughout the text. If they are done by Put blocks, they would be only accepted during demonstrations.

Definition blocks are in the same line as axiom blocks and theorem blocks and their form looks like this:

Definition;

End Def;

Therefore, the form is such that more than one put blocks are in between the Definition and End Def. Figure A is an example of definition blocks.

Put blocks are explained in more detail in a later chapter, but the fact that they are utilized in definition blocks and during theory demonstrations is explained above. Figure B is an example that was used during the demonstrations.

When put blocks are used during demonstrations, if they are in other blocks (such as quantitization blocks or implication blocks), the effect of that definition becomes more limited. Consequently, the effect not only reaches outside the demonstrations, but also outside the blocks.

02690 'Definition;/* Def. of inequality, Less than */

02700 ' NaDe1: Put LT(x,y)=(Exist z)(Nat(z)and[Add(x,z)=y]);

02710 ' NaDe2: Put GT(x,y)=(Exist z)(Nat(z)and[Add(y,z)=x]);

02720 'End Def;

02730 '

02740 'Lemma;/* (x is greater than y)=(y is Less than x)*/

02750 ' NaLem8: (All x)(All y)([GT(x,y)=LT(y,x)]);

Figure A An example of a definition block. There are two put blocks (NaDe1, NaDe2) in a definition block that starts with line 2690.

01950 'Lemma;/*Commutativity of Addition*/

01960 ' NaLem7: (All x)(All y)(Nat(x) and Nat(y) imp

01965 ' [Add(x,y)=Add(y,x)]);

01970 'Proof;a1: (All x)(All y)(;

01980 ' a2: Nat(x)and Nat(y)imp;

01990' a3: Put f(n)=[Add(x,n)=Add(n,x)];

02000 ' a4: Nat(x)imp[Add(x,1)=Add(1,x)] by ALS(NaLem6);

02010 ' a5: [Add(x,1)=Add(1,x)] by LOGIC(a2,a4);

02020 ' a6: f(1) by FUNF(a3,a5);

02030 ' a7: (All s)(;

02040 ' a8: Nat(s)and f(s) imp;

02050 ' a9: f(s) by LOGIC(a8);

02060 ' a10: [Add(x,s)=Add(s,x)] by FUNF(a3,a9);

02070 ' a11: [Add(s,PL(x))=PL(Add(s,x))] by ALS(Nat7);

02080 ' a12:[Add(s,PL(x))=PL(Add(x,s))] by SUBST(a11,a10);

02090 ' a13: [Add(x,PL(s))=PL(Add(x,s))] by ALS(Nat7);

02100 ' a14:Nat(s)and Nat(x)imp[Add(s,PL(x))=Add(PL(s),x)]

02110 ' by ALS(NaPro2);

02120 ' a15: [Add(s,PL(x))=Add(PL(s),x)]

02125 ' by LOGIC(a2,a8,a14);

02130 ' a16:[Add(x,PL(s))=Add(PL(s),x)]by EQ(a13,a12,a15);

02140 ' imp f(PL(s)) by FUNF(a3,a16);

02150 ' );

02160 ' a17:f(1)and(All s)(Nat(s)and f(s)imp f(PL(s)))imp

02170 ' (All j)(Nat(j)imp f(j)) by ALS(Nat5);

02180 ' a18: (All j)(Nat(j)imp f(j))by LOGIC(a6,a7,a17);

02190 ' a19: Nat(y)imp f(y) by ALS(a18);

02200 ' a20: f(y) by LOGIC(a2,a19);

02210 ' imp [Add(x,y)=Add(y,x)] by FUNF(a3,a20);

02220 ' );

02230 'Q.E.D.(a1);

Figure B An example of a put block during a demonstration. It is line1990(a3). The effect of this put block only extends within this demonstration. Moreover, the effect also does not reach outside the implication block(lines from 1980 to 2210), where this put sentence is placed.