2.4 The structure of the Quantitization Block


We explained that the theorem and other demonstrations adopt the block structure; however, to elucidate more explicitly, quantitization blocks start with such a logical line as:

a1 : (All x)(All y)(Exist z)(:

It is one block after this line, however, that the end of that block is a logical line with only such parentheses :

) :

(Do not put labels in this line). The meaning of this block is that variables x, y, and z are treated as proper nouns registered in the name table. This block is advantageous for, for example, transformation inside a quantitized formula.

When the head of a quantitization block, such as a1 appears, the system actually registers variables x, y, and z to the name table (ntable). Therefore, it is possible to use x, y, and z in each line of the blocks similar to Nat1 and Add which were declared by an axiom.

Further, as an important warning on the whole, one must not utilize unregistered (to the name table) names of variables or functions at any time. However, such a restricted variable such as x in this formula, (All x)(f (x)) is an exception. This x is, and will not be registered to a name table.

If a quantitization block ends at a line with only a right parenthesis, the system will delete x, y, and z that were registered in a name table up to that point. Therefore, from that point on, one will not be permitted to use x, y, and z in the same sense within the blocks.

After pulling out of blocks, if we cite labels of the blocks' head (as example a1 above), that means the last formula in blocks with attached head quantitization symbol was quoted (figure A).

In addition, after pulling out of the blocks, we cannot cite formulas in the middle of blocks. The only formulas during demonstrations that can be cited are the ones that are already registered in a formula table (udirect). Also in blocks, formulas that are correctly recommended get registered to this table. However, when they reach the right parenthesis at the end of the blocks, all of these formulas get deleted and instead, as explained in figure A, formulas that quote lables of the blocks' heads get registered .

05130 'Proposition ;/* x

05135 ' NaPro10:(All x)(LT(x,PL(x)));

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

05150 ' a2: [Add(x,1)=PL(x)] by ALS(Nat6);

05160 ' a3: Nat(1)and[Add(x,1)=PL(x)] by LOGIC(a2,Nat1);

05170 ' a4: (Exist z)(Nat(z)and[Add(x,z)=PL(x)])

05175 ' by EXIST(a3);

05180 ' a5: LT(x,PL(x)) by FUNF(NaDe1,a4);

05190 ' );

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

Figure A The demonstration of X < X + 1. If we cite label a1, it means that we specified the same formula with NaPro 10 that tied a 1's " (All X) (" and a 5's " LT (x, P1 (x))" and end of ") " together. The a1 in Q.E.D.(a 1); of the end of the demonstration emphasizes that it is the same with the formula of NaPro 10 that should be demonstrated by the formula a1.