theory Propositional_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 "P \ Q \ P"
sorry
lemma
shows "(P \ Q \ R) \ (P \ Q \ R)"
sorry
lemma
assumes "P \ (Q \ R)"
shows "Q"
sorry
lemma
assumes "P \ Q \ R"
and "R \ S"
shows "P \ S"
sorry
lemma
shows "((P \ Q) \ P) \ P"
sorry
lemma
shows "\\\P \ \P"
sorry
lemma
assumes "P \ \ Q \ R"
and "R \ \ Q"
and "S \ P"
shows "\ Q"
sorry
lemma
shows "\ False"
sorry
lemma
shows "\ (P \ Q) \ (\\\P \ \Q)"
sorry
lemma
shows "(True \ P) \ P"
sorry
end