(*
ex.thy,v 1.1 2016/09/29 17:37:37 jdf Exp
Original Author: Tjark Weber
Updated to Isabelle 2016 by Jacques Fleuriot
*)
section {* Predicate Logic *}
theory ex imports Main begin
text {*
We are again talking about proofs in the calculus of Natural Deduction. In
addition to the rules given in the exercise "Propositional Logic", you may
now also use
exI: ?P ?x \ \x. ?P x
exE:\\x. ?P x; \x. ?P x \ ?Q\ \ ?Q
allI: (\x. ?P x) \ \x. ?P x
allE: \\x. ?P x; ?P ?x \ ?R\ \ ?R
Give a proof of the following propositions or an argument why the formula is
not valid:
*}
lemma "(\x. \y. P x y) \ (\y. \x. P x y)"
oops
lemma "(\x. P x \ Q) = ((\x. P x) \ Q)"
oops
lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))"
oops
lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))"
oops
lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))"
oops
lemma "(\x. \y. P x y) \ (\y. \x. P x y)"
oops
lemma "(\ (\ x. P x)) = (\ x. \ P x)"
oops
end