## 3.4 EXIST (Adding Exist Symbols)

EXIST works just the opposite way from ALS. Each Example below corresponds
with examples of ALS(§3. 3).

Example 1 a1 : f(a) by ....;

.........
a2 : (Exist x) (f(x)) by EXIST (a1) ;
Example 2 a1 : f([c=d] , B(k) and B(k) (a) by....;..........

a2 : (Exist x)(Exist y)(f (x,y) and y(a)) by EXIST (a1) ;
Example 3 a1 : u((All z) (t(z)), True) by ..;

..........
a2 : (Exist x) (Exist y) (u (x,y)) by Exist (a1) ;
Therefore, if we form a formula by substituting a formula of only registered
names into variables, a formula made by restricting variables with exist
symbols is also structured. This implies the opposet of ALS's case (in
a sense that it quantitizes unquantitized formulas); however, in reality,
work that the THEAX system conducts is also opposite of ALS's work. This
is done by reversing the conditional formula (formula 1 of the example
above) and the conclusion formula (formula 2 of the example above) before
anything else and changing the new conditional formula (previous conclusion
formula) of Exist into All. After that, we inspect if the conclusion formula
(previous conditional formula) can be actually guided by using the routine
of ALS.