1459

1 
(* Title: FOL/ex/quant

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
FirstOrder Logic: quantifier examples (intuitionistic and classical)


7 
Needs declarations of the theory "thy" and the tactic "tac"


8 
*)


9 


10 
writeln"File FOL/ex/quant.";


11 


12 
goal thy "?p : (ALL x y.P(x,y)) > (ALL y x.P(x,y))";


13 
by tac;


14 
result();


15 


16 


17 
goal thy "?p : (EX x y.P(x,y)) > (EX y x.P(x,y))";


18 
by tac;


19 
result();


20 


21 


22 
(*Converse is false*)


23 
goal thy "?p : (ALL x.P(x))  (ALL x.Q(x)) > (ALL x. P(x)  Q(x))";


24 
by tac;


25 
result();


26 


27 
goal thy "?p : (ALL x. P>Q(x)) <> (P> (ALL x.Q(x)))";


28 
by tac;


29 
result();


30 


31 


32 
goal thy "?p : (ALL x.P(x)>Q) <> ((EX x.P(x)) > Q)";


33 
by tac;


34 
result();


35 


36 


37 
writeln"Some harder ones";


38 


39 
goal thy "?p : (EX x. P(x)  Q(x)) <> (EX x.P(x))  (EX x.Q(x))";


40 
by tac;


41 
result();


42 
(*6 secs*)


43 


44 
(*Converse is false*)


45 
goal thy "?p : (EX x. P(x)&Q(x)) > (EX x.P(x)) & (EX x.Q(x))";


46 
by tac;


47 
result();


48 


49 


50 
writeln"Basic test of quantifier reasoning";


51 
(*TRUE*)


52 
goal thy "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


53 
by tac;


54 
result();


55 


56 


57 
goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))";


58 
by tac;


59 
result();


60 


61 


62 
writeln"The following should fail, as they are false!";


63 


64 
goal thy "?p : (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))";


65 
by tac handle ERROR => writeln"Failed, as expected";


66 
(*Check that subgoals remain: proof failed.*)


67 
getgoal 1;


68 


69 
goal thy "?p : (EX x. Q(x)) > (ALL x. Q(x))";


70 
by tac handle ERROR => writeln"Failed, as expected";


71 
getgoal 1;


72 


73 
goal thy "?p : P(?a) > (ALL x.P(x))";


74 
by tac handle ERROR => writeln"Failed, as expected";


75 
(*Check that subgoals remain: proof failed.*)


76 
getgoal 1;


77 


78 
goal thy


79 
"?p : (P(?a) > (ALL x.Q(x))) > (ALL x. P(x) > Q(x))";


80 
by tac handle ERROR => writeln"Failed, as expected";


81 
getgoal 1;


82 


83 


84 
writeln"Back to things that are provable...";


85 


86 
goal thy "?p : (ALL x.P(x)>Q(x)) & (EX x.P(x)) > (EX x.Q(x))";


87 
by tac;


88 
result();


89 


90 


91 
(*An example of why exI should be delayed as long as possible*)


92 
goal thy "?p : (P > (EX x.Q(x))) & P > (EX x.Q(x))";


93 
by tac;


94 
result();


95 


96 
goal thy "?p : (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)";


97 
by tac;


98 
(*Verify that no subgoals remain.*)


99 
uresult();


100 


101 


102 
goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))";


103 
by tac;


104 
result();


105 


106 


107 
writeln"Some slow ones";


108 


109 


110 
(*Principia Mathematica *11.53 *)


111 
goal thy "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))";


112 
by tac;


113 
result();


114 
(*6 secs*)


115 


116 
(*Principia Mathematica *11.55 *)


117 
goal thy "?p : (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))";


118 
by tac;


119 
result();


120 
(*9 secs*)


121 


122 
(*Principia Mathematica *11.61 *)


123 
goal thy "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))";


124 
by tac;


125 
result();


126 
(*3 secs*)


127 


128 
writeln"Reached end of file.";


129 
