21426

1 
(* Title: LK/Quantifiers.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Classical sequent calculus: examples with quantifiers.


7 
*)


8 


9 
theory Quantifiers


10 
imports LK


11 
begin


12 


13 
lemma " (ALL x. P) <> P"


14 
by fast


15 


16 
lemma " (ALL x y. P(x,y)) <> (ALL y x. P(x,y))"


17 
by fast


18 


19 
lemma "ALL u. P(u), ALL v. Q(v)  ALL u v. P(u) & Q(v)"


20 
by fast


21 


22 


23 
text "Permutation of existential quantifier."


24 


25 
lemma " (EX x y. P(x,y)) <> (EX y x. P(x,y))"


26 
by fast


27 


28 
lemma " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))"


29 
by fast


30 


31 
(*Converse is invalid*)


32 
lemma " (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)Q(x))"


33 
by fast


34 


35 


36 
text "Pushing ALL into an implication."


37 


38 
lemma " (ALL x. P > Q(x)) <> (P > (ALL x. Q(x)))"


39 
by fast


40 


41 
lemma " (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"


42 
by fast


43 


44 
lemma " (EX x. P) <> P"


45 
by fast


46 


47 


48 
text "Distribution of EX over disjunction."


49 


50 
lemma " (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"


51 
by fast


52 


53 
(*Converse is invalid*)


54 
lemma " (EX x. P(x) & Q(x)) > (EX x. P(x)) & (EX x. Q(x))"


55 
by fast


56 


57 


58 
text "Harder examples: classical theorems."


59 


60 
lemma " (EX x. P>Q(x)) <> (P > (EX x. Q(x)))"


61 
by fast


62 


63 
lemma " (EX x. P(x)>Q) <> (ALL x. P(x)) > Q"


64 
by fast


65 


66 
lemma " (ALL x. P(x))  Q <> (ALL x. P(x)  Q)"


67 
by fast


68 


69 


70 
text "Basic test of quantifier reasoning"


71 


72 
lemma " (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"


73 
by fast


74 


75 
lemma " (ALL x. Q(x)) > (EX x. Q(x))"


76 
by fast


77 


78 


79 
text "The following are invalid!"


80 


81 
(*INVALID*)


82 
lemma " (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"


83 
apply fast?


84 
apply (rule _)


85 
oops


86 


87 
(*INVALID*)


88 
lemma " (EX x. Q(x)) > (ALL x. Q(x))"


89 
apply fast?


90 
apply (rule _)


91 
oops


92 


93 
(*INVALID*)


94 
lemma " P(?a) > (ALL x. P(x))"


95 
apply fast?


96 
apply (rule _)


97 
oops


98 


99 
(*INVALID*)


100 
lemma " (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"


101 
apply fast?


102 
apply (rule _)


103 
oops


104 


105 


106 
text "Back to things that are provable..."


107 


108 
lemma " (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))"


109 
by fast


110 


111 
(*An example of why exR should be delayed as long as possible*)


112 
lemma " (P> (EX x. Q(x))) & P> (EX x. Q(x))"


113 
by fast


114 


115 


116 
text "Solving for a Var"


117 


118 
lemma " (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)"


119 
by fast


120 


121 


122 
text "Principia Mathematica *11.53"


123 


124 
lemma " (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"


125 
by fast


126 


127 


128 
text "Principia Mathematica *11.55"


129 


130 
lemma " (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))"


131 
by fast


132 


133 


134 
text "Principia Mathematica *11.61"


135 


136 
lemma " (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"


137 
by fast


138 


139 


140 
(*21 August 88: loaded in 45.7 secs*)


141 
(*18 September 2005: loaded in 0.114 secs*)


142 


143 
end
