(* \$Id: ex.thy,v 1.2 2004/11/23 15:14:35 webertj Exp \$ *) header {* 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 @{text "exI:"}~@{thm exI[no_vars]}\\ @{text "exE:"}~@{thm exE[no_vars]}\\ @{text "allI:"}~@{thm allI[no_vars]}\\ @{text "allE:"}~@{thm allE[no_vars]}\\ 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 (*>*)