3. 9 DMOR (De Morgan)


DMOR is constructed by turning the formula of De Morgan, which relates to the predicate logic, into inference rules.

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

.........
a2 : (Exist x) (not f(x)) by DMOR (a1) ;

Example 2 a1 : not (Exist x) (All y) (Exist z) (f(x,y,z)) by .... ;

.........
a2 : (All x) (Exist y) (All z) (not f(x,y,z)) by DMOR (a1) ;
Also, opposit of these will be inferred with the same DMOR.

Example 3 a1 : (Exist x) (not f(x)) by ... ;

.........
a2 : not (All x) (f(x)) by DMOR (a1) ;

Thus, when writing not f(x) in each example, f(x) should not be limited to the function form and any formulas will be acceptable if they do not confuse the operating order (<factor>) by putting not. For instance, [a=b], (All u), (g(u,x)), and not A(x) are acceptable.

Furthermore, the rule DMOR is not necessary because, for example, example 1 above can be substituted by a combination of other rules such as the ones below.

a2 : not (Exist x) (not f(x)) imp ;
a3 : (Exist x) (not f(x)) imp True by LOGIC (a2) ;
a4 : (All x) (not f(x) imp True) by EXIM (a3) ;
a5 : (All x) ( ;
a6 : not f(x) imp True by ALS (a4) ;
     a7 : f(x) by LOGIC (a6) ;

);

imp False by LOGIC(a1, a5) ;
a8 : (Exist x) (not f(x)) by LOGIC (a2) ;

Therefore, a8 corresponds with a2 of example 1.