(* ex.thy,v 1.1 2016/09/29 17:37:37 jdf Exp Original Author: Tjark Weber Updated to Isabelle 2016 and additions by Jacques Fleuriot *) section {* Propositional Logic *} theory ex imports Main begin text {* In this exercise, we will prove some lemmas of propositional logic with the aid of a calculus of natural deduction. For the proofs, you may only use notI: (?P \ False) \ \ ?P notE: \\ ?P; ?P\ \ ?R 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 mp: \?P \ ?Q; ?P\ \ ?Q iffI:\?P \ ?Q; ?Q \ ?P\ \ ?P = ?Q iffE:\?P = ?Q; \?P \ ?Q; ?Q \ ?P\ \ ?R\ \ ?R classical: (\ ?P \ ?P) \ ?P and the proof methods rule, erule and assumption. \end{itemize} Prove: *} lemma I: "A \ A" oops lemma "A \ B \ B \ A" oops lemma "(A \ B) \ (A \ B)" oops lemma "((A \ B) \ C) \ A \ (B \ C)" oops lemma K: "A \ B \ A" oops lemma "(A \ A) = (A \ A)" oops lemma S: "(A \ B \ C) \ (A \ B) \ A \ C" oops lemma "(A \ B) \ (B \ C) \ A \ C" oops lemma "\ \ A \ A" oops lemma "A \ \ \ A" oops lemma "(\ A \ B) \ (\ B \ A)" oops lemma "((A \ B) \ A) \ A" oops lemma "A \ \ A" oops lemma "(\ (A \ B)) = (\ A \ \ B)" oops end