Prover9 に

all,exists の inference rules を証明させます．

%for Prover9

(

%LAE
((all y all x (r(y)->q(x,y)))&(all y ((all x q(x,y))->p(y)) ))
->(all y (r(y)->p(y)))

)&(

%weak LAE LAI
(all y ((all x q(x,y))->p(y)) )
<->(all y exists x (q(x,y)->p(y)))

)&(

%LAI
(exists x all y (q(x,y)->p(y)))
->(all y ((all x q(x,y))->p(y)) )

)&(

%LEI
(all x all y (q(x,y)->p(y)))
->(all y (exists x q(x,y))->p(y) )

)&(

%LEE
(all y ((exists x q(x,y))->p(y)) )
->(all x all y (q(x,y)->p(y)))

).

%for Prover9

(

%RAE
(all y ( p(y)-> all x q(x,y)))
->(all x all y (p(y)->q(x,y)))

)&(

%RAI
(all x all y (p(y)->q(x,y)))
->(all y ( p(y)-> all x q(x,y)))

)&(

%REE
((all y ( p(y)-> exists x q(x,y)))&(all y all x (q(x,y)->r(y))))
->(all y (p(y)->r(y)))

)&(

%weak REE REI
(all y ( p(y)-> exists x q(x,y)))
<->(all y exists x (p(y)->q(x,y)))

)&(

%REI
(exists x all y (p(y)->q(x,y)))
->(all y ( p(y)-> exists x q(x,y)))

).