## 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.