The following examples from Benson Mates' book "Elementary Logic" are part of the test suite for my theorem prover. If you want to try them out for yourself, please copy and paste them to the input area of the prover. Note that some of these examples need Mates' algorithm for deriving and may require a sufficient amount of time.
all(x,all(y,F(x,y)))<->all(y,all(x,F(x,y)))
exist(x,exist(y,F(x,y)))<->exist(y,exist(x,F(x,y)))
exist(x,all(y,F(x,y)))->all(y,exist(x,F(x,y)))
all(x,F(x)&G(x)) <-> (all(x,F(x)) & all(x,G(x)))
(all(x,F(x)) v all(x,G(x))) -> all(x,F(x)v G(x))
(all(x,F(x)) v all(x,G(x))) -> all(x,F(x) v G(x))
exist(x,F(x)&G(x)) -> (exist(x,F(x)) & exist(x,G(x)))
exist(x,F(x) v G(x)) <-> (exist(x,F(x)) v exist(x,G(x)))
all(x,P v F(x)) <-> (P v all(x,F(x)))
~(all(x,P v F(x)) <-> (P v all(x,F(x))))
all(x,P->F(x)) <-> (P->all(x,F(x)))
exist(x,P & F(x)) <-> (P & exist(x,F(x)))
exist(x,P v F(x)) <-> P v exist(x,F(x))
exist(x,P->F(x)) <-> P->exist(x,F(x))
all(x,F(x)->P) <-> exist(x,F(x))->P
all(x,F(x)->P) <-> exist(x,F(x))->P
all(x,P & F(x)) <-> (P & all(x,F(x)))
exist(x,F(x)->P) <-> (all(x,F(x)) -> P)
all(x,exist(y,F(x) & G(y))) (all(x,F(x)) & exist(y,G(y)))
all(x,exist(y,F(x)&G(y))) exist(y,all(x,F(x)&G(y)))
all(x,F(x)) v exist(y,G(y)) <->\ all(x,exist(y,F(x) v G(y)))
all(x,exist(y,F(x)v G(y))) exist(y,all(x,F(x)v G(y)))
all(x,exist(y,F(x)->G(y))) exist(y,all(x,F(x)->G(y)))
all(x,exist(y,all(z,exist(w,~F(x,y)v F(w,z)))))
exist(x,exist(y, ~I(x,y) & all(z,I(z,x) v I(z,y)) )) exist(x,exist(y,~I(x,y))) & all(x,all(y,all(z,(I(x,y) v I(x,z)) v I(y,z))))
~(alle(x1,ein(x2,ein(x3,alle(x4,ein(x5,F(x2,x1,x5) & ~F(x4,x3,x5)))))))Note that this proposition is not a theorem, but shows a bug in the tableau methods of my prover. Thanks to Timm Lampert for making me aware of this bug.
2012-03-31 01:19:53
christian.gottschall@posteo.de