## 3. 10 CNST (Elimination of Quantitization Symbols from the Constant
Formulas)

When the predicate logic formulas are constant like below, this function
enables quantitization symbols to be removed from them:

Example 1 a1 : (All x) (p (a)) by .... ;

..........
a2 : p (a) by CNST (a1) ;
Example 2 a1 : (Exist x) (All y) (b and c) by .... ; ..........

a2 : b and c by CNST (a1) ;
These inference rules are not necessary due to the following reasons.
The next one substitutes for the combination of other rules (example 1
can be substituted by ALS).

a2 : (Exist x) ((All y) (b and c)) by ARRN (a1) ;
a3 : (All x) (; a4 : (All y) (b and c) imp (All y) (b and c) by LOGIC
;) ;
a5 : (Exist x) ((All y) (b and c)) imp (All y) (b and c) by EXIM (a3)
;
a6 : (All y) (b and c) by LOGIC (a2,a5) ;
a7 : b and c by ALS (a6) ;