2.3 Theorem(Theorem, Lemma, and others)


In a theorem, we demonstrate a new relation that use registered names. At first, we mark the beginning of a theorem block with Theorem;, Lemma;, Proposition;, or Corollary;. (Theax essentially does not distinguish theorem, proposition, or corollary). After Lemma; and so on, we write formulas with labels that should be demonstrated. Following that line of formula, place a line that says Proof; and continue on over some lines with a demonstration part for formulas. Demonstration ends with a line saying Q.E.D.(<label>);.

Demonstration parts are led by a form of new formulas being guided from some demonstrated formulas. For example, in figure A, the 1020th line of formula a4 can be acquired by inserting special values (in here, x and y that are expressed in the same letter) to the restricted variables x and y of the axiom formula of Nat7

(All x)(All y)([Add (x, P1 (y))=P1(Add (x,y))]).

In addition, the 1030th line of formula a4 can be obtained by injecting a special value into Nat6, the axiom formula. The 1040th line of formula a5 can be procured by substituting an equality a4 into formula a3. Thus, according to some regulations (inference regulations), each line is taken one after another from demonstrated lines. There are over ten kinds of these inference regulations as explained in (figure 3).

Systems memorize the already demonstrated formulas. Those are registered in a table of formulas (it is named utable) with labels. Therefore, formulas that come up during an axiom also get registered in this table. In addition, propositions of the theorem that appeared up to that point also get registered. If the formulas that appear during the current theorem demonstration are also appropriate for a deduction, they too get registered. However, when the demonstration reaches Q.E.D. , those theorem prepositions get newly registered in that table and formulas used for the demonstration get deleted from that table. Therefore, it is impossible to use the formulas that appeared during the past theorem demonstration for the current theorem demonstration. The name table (ntable) and the formula table(utable) were explained as tables used in THEAX. These two are theoretically important.

As a characteristic of the demonstration part, sometimes block structure comes off. We are able to divide the demonstration into some blocks and provide added blocks within blocks. For instance in figure A, it is constructed by one quantitization block; however, in figure B the structure gets more complicated because there is a implication block outside the quantitization block and inside of that, there is another quantitization block.

00990 'Lemma;/*Simple associativity*/

01000 ' NaLem4; (All x)(All y)([Add (Add(x,y),1)

01005 ' =Add(x,Add(y,1))]);

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

01020 ' a3: [Add(x,PL(y))=PL(Add(x,y))] by ALS(Nat7);

01030 ' a4: [Add(y,1)=PL(y)] by ALS(Nat6);

01040 ' a5: [Add(x,Add(y,1))=PL(Add(x,y))]

01045 ' by SUBST(a3,a4);

01050 ' a6:[Add(Add(x,y),1)=PL(Add(x,y))]by ALS(Nat6);

01060 ' a7:[Add(Add(x,y),1)=Add(x,Add(y,1))]

01065 ' by EQ(a5,a6);

01070 ' ):

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

Figure A A supplemental theme that suggests combination rule to one kind of addition. It is a kind of the theorem block.

02830 'Lemma;/* 1 is the least number */

02840 ' NaLem9:(All x)(Nat(x)and not[x=1]imp LT(1,x));

02850 'Proof;

02860 ' a1:(All x)(;

02870 ' a2: Nat(x)and not[x=1] imp;

02880 ' a3: (Exist y)(Nat(y)and [PL(y)=x])

02885 ' by ALS(NaLem1,a2);

02890 ' a4: (Exist z)(;

02900 ' a5: Nat(z)and [PL(z)=x] by FLW(a3);

02910 'a6: Nat(z)imp[Add(1,z)=PL(z)] by LOGIC(a5,a6);

02920 ' a7: [Add(1,z)=PL(z)] by LOGIC(a5,a6);

02930 ' a8: Nat(z)and[Add(1,z)=x]by SUBST(a5,a7);

02940 ' );

02950 ' imp LT(1,x) by FUNF(NaDe1,a4);

02960 ' );

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

Figure B A supplemental theme that says 1 is the smallest number. One kind of the theorem block.