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) ;