theory Predicate_Logic_Exercises
imports Main
begin
(*use rule, erule, and so on combined with basic elimination and introduction rules. do not use
any automation...*)
lemma
shows "(\x. (P \ Q x)) \ (P \ (\x. Q x))"
sorry
(*prove contrapos_np first, then use it to prove the next lemma below:*)
lemma contrapos_np:
assumes "\ Q" and "\ P \ Q"
shows "P"
sorry
lemma
shows "\ (\x. P x \ Q x) \ (\x. \ P x \ \ Q x)"
sorry
lemma
shows "\P. \Q. \x. ((P x \ Q x) \ P x) \ P x"
sorry
lemma
assumes "Q \ (\x. S x)"
and "S False \ Q"
and "S True \ Q"
shows "Q \ (\x. S x)"
sorry
lemma
shows "(\P Q. \!x. P x \ Q x) \ False"
sorry
lemma
shows "\P. \x. \ P x"
sorry
lemma
shows "(\x. P x \ Q x) \ (\x. \ P x \ Q x)"
sorry
end