## 3.3 ALS (Limitation of All Symbols)

ALS (All-Substitution) limits formulas that are quantitized with all
symbols by certain special names.

Example 1 a1 : (All x)(f(x)) by ....;

..........
a2 : f(a) by ALS (a1) ;
Example 2 a1 : (All x)(All y)(f(x,y) and y(a))

by ......;
..........
a2 : f([c=d], B(k)) and B(k) (a)
by ALS (a1) ;
In example 2, variable y is also a function name (accordingly, such
function form as y(a) appears). Therefore, this is the so called second
level predicate logic, but in THEAX, level is not too much of a problem.
Also, y is replaced by B(k). B is a functional.

Example 3 a1 : (All x)(All y)(u (x,y)) by ..;

..........
a2 : u((All z)(t(z)), True)
by ALS (a1) ;
Also, ALS sometimes gets 2 arguments.
Example 4 a1 : (All x)(f(x) imp g(x)) by ..;

..........
a2 : f(a) by ....;
..........
a3 : g(a) by ALS (a1, a2) ;
Such as this, when ALS's arguments are 2, computers automatically connect
formulas a2 and a3 with imp and inspect if that formula is derived from
a1. Instead of a3 above, writing over 2 lines like the following will have
the same effect.

a 2.5 : f(a) imp g(a) by ALS (a1) ;
a 3 : g(a) by LOGIC (a 2, a 2.5) ;
Furthermore, when the meaning of formulas differ due to, for example,
change of operating order for limiting variables of all symbols, one needs
to be careful because the replacement of variables will not be possible.

Example 5 (Abominable) a1 : (All x)(x and b) by ....;

a2 : a or c and b by ALS(a1) ;
Example 6 (Abominable) a1 : (All f)(f(s) imp g) by ....;

a2 : [c=d] (s) imp g by ALS(a1) ;
Concerning quantitization blocks, sometimes, ALS or later explained
FLW are used in the line following the beginning of a quantitization block.
In many cases, using either one is acceptable. Therefore, in following
formulas,

a1 : (All x)(h(x)) by ....;
a2 : (All x)(;
a3 : h(x) by ALS (a1) ;
we let a1 stay the same and make a2 and a3 like below.

a2 : (All x)(;
a3 : h(x) by FLW (a1) ;
The former means to limit to special x as variables, and the latter
means when connecting the beginning of a2 with the formula a3 and parenthesize
it, it becomes formula a1.