2.5 The Structure of Implication Blocks


Other than the quantitization block from the previous section, there are implication blocks, Because blocks, and Put blocks during the theorem demonstrations. First of all, implication blocks are used to lead arguments by assuming some conditions. During the usual mathematical demonstrations, such a sentence as "we assume it is <formula 1>" frequently appears. In THEAX, we express this with a line saying

<Label 1>:<Formula 1> imp;

This is the head of a implication block and it also indicates the beginning. The end of the block is a line that says

imp <Formula 2> by <Inference value>

(<end.implication.line>). Concerning the line of a implication block's head, <Formula 1>gets registered to a table of formulas (udirect). Therefore, using <Label 1>, it is acceptable to quote <Formula 1> in blocks as the demonstrated formula. However, in reality, it does not mean that the formula is demonstrated; therefore, when it reaches the block's end of line, the system deletes <Formula 1> from a table of formulas. Instead, we assemble such a formula as <Label 1>:<Formula 1>imp< Formula 2> and register to a table of formulas ( we also pay attention not to let the order of operations become confused by inserting parentheses properly ). From then on, when we cite by <label 1>, it should be pointing to that assembled formula.

Furthermore, as it is the same case with quantitization blocks, all formulas that appeared in blocks will be deleted from a table of formulas at the end of the blocks. As it is shown above, the end of a block's line starts with imp. One must not put labels on this line. Also, we have to write "by" and put the inference value, and like other lines during the demonstrations, we need to indicate by what reason that line is guided.

The implication block implies the so called irrationality rule. Let us assume that the conclusion formula <formula 2> of an example above is

False.

Then, joining with the previous formula <formula 1>, such a formula as <Label 1>:<formula 1> imp False is demonstrated. Logical proportionally, this is the same with "not <formula 1>". If <formula 1> itself takes a negative form like not <formula 0>, it means that <formula 0> has been demonstrated, and this would truly be irrational logic.

Figure A is an example showing what types of formulas one implication block is demonstrating and figure B is an example of implication blocks being doubled. In fact, this block is included in the quantitization block that starts with an a 1 label. It is fine to have different blocks multiplexed into other kinds of blocks.

01660 'Lemma;/*Simple Commutativity*/

01670 ' NaLem6: (All x)(Nat(x)imp [Add(x,1)=Add(1,x)]);

01680 'Proof;a1: (All x)(;

01690 ' a2:Nat(x) imp;

01700 ' a3: Nat(x)imp [Add(1,x)=P1(x)] by ALS(NaPro1);

01710 ' a4: [Add(1,x)=P1(x)] by LOGIC(a2,a3);

01720 ' a5: [Add(x,1)=P1(x)] by ALS(Nat6);

01730 ' imp [Add(x,1)=Add(1,x)] by EQ(a4,a5);

01740 ' );

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

Figure A The formula a2 points to Nat (x)imp[Add(x,1)=Add(1,x)] that linked lines 1690 and 1730 outside the blocks (after line 1740).

08810 'Proposition;/* x<=y --> Max(x,y)=y */

08820 ' NaPro24: (All x)(All y)(LE(x,y)imp [Max(x,y)=y]);

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

08840 ' a2: LE(x,y) imp;

08845 ' a3: LT(x,y)or [x=y] by FUNF(NaDe3,a2);

08850 ' a4: LT(x,y) imp;

08860 ' imp [Max(x,y)=y] by ALS(NaDe5,a4);

08870 ' a5: [x=y] imp; a6: [Max(x,x)=x] by ALS(NaPro22);

08880 ' imp [Max(x,y)=y] by SUBST(a6,a5);

08890 ' imp [Max(x,y)=y] by LOGIC(a3,a4,a5);

08900 ' );

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

Figure B An example of a connotation block intricated.