theory mp1 imports Main begin (* In this exercise, you will prove some lemmas of propositional logic with the aid of a calculus of natural deduction. For the proofs, you may only use "assumption", and the following rules with rule, erule, rule_tac or erule_tac. You may also use lemmas that you have proved so long as they meet the same restriction. *) thm notI thm notE thm conjI thm conjE thm disjI1 thm disjI2 thm disjE thm impI thm impE thm iffI thm iffE (* notI: (P \ False) \ \ P notE: \ \ P; P \ \ Q conjI: \ P; Q \ \ P \ Q conjE: \ P \ Q; \ P; Q \ \ R \ \ R disjI1: P \ P \ Q disjI2: Q \ P \ Q disjE: \ P \ Q; P \ R; Q \ R \ \ R impI: (P \ Q) \ P \ Q impE: \ P \ Q; P; Q \ R \ \ R iffI: \ P \ Q; Q \ P \ \ P = Q iffE: \ P = Q; \ P \ Q; Q \ P \ \ R \ \ R Prove: *) lemma problem1: "(A \ B) \ (B \ A)" sorry lemma problem2: "(A \ B) \ (B \ A)" sorry lemma problem3: "(A \ B) \ ((\B) \ (\A))" sorry lemma problem4: " (A \ B) \ ((\ B) \ (\ A))" sorry lemma problem5: "((A \ B) \ C) \ (A \ (B \ C))" sorry lemma problem6: "((\ B) \ (\ A)) \ (\(A \ B))" sorry lemma problem7: "(\A \ \B) \ (\(A \ B))" sorry (* Extra Credit *) thm classical lemma problem8: "\ \ A \ A" sorry lemma problem9: "A \ \ A" sorry lemma problem10: "(\ A \ B) \ (\ B \ A)" sorry lemma problem11: "((A \ B) \ A) \ A" sorry lemma problem12: "(\ (A \ B)) = (\ A \ \ B)" sorry lemma problem13: "(\ A \ False) \ A" sorry end