section \A Hilbert Proof Calculus for Propositional Logic (PL)\ (*<*) theory Hilbert imports Main begin (*>*) subsection \Logical Connectives for PL\ subsubsection \Primitive Connectives\ consts impl :: "bool \ bool \ bool" (infixr "\<^bold>\" 49) consts not :: "bool \ bool" ("\<^bold>\") text \In philosophy, we often assume that the only two logical connectives are the implication @{const impl} and the negation @{const not}. This is handy, since it simplifies proofs to only consider these two cases. \ subsubsection \Further Defined Connectives\ text \We can of course add further connectives that are to be understood as abbreviations that are defined in terms of the primitive connectives above.\ abbreviation disj :: "bool \ bool \ bool" (infixr "\<^bold>\"50) where "A \<^bold>\ B \ \<^bold>\A \<^bold>\ B" abbreviation conj :: "bool \ bool \ bool" (infixr "\<^bold>\"51) where "A \<^bold>\ B \ \<^bold>\(A \<^bold>\ \<^bold>\B)" subsection \Hilbert Axioms for PL\ subsubsection \Axiom Schemes\ axiomatization where (* A1: "(A \<^bold>\ A)" and*) A2: "A \<^bold>\ (B \<^bold>\ A)" and A3: "(A \<^bold>\ (B \<^bold>\ C)) \<^bold>\ ((A \<^bold>\ B) \<^bold>\ (A \<^bold>\ C))" and A4: "(\<^bold>\A \<^bold>\ \<^bold>\B) \<^bold>\ (B \<^bold>\ A)" subsubsection \Inference Rules\ axiomatization where ModusPonens: "(A \<^bold>\ B) \ A \ B" (* Test soundness of axiomatizaion *) lemma True nitpick [satisfy, user_axioms, expect = genuine] oops subsection \A Proof\ (* just playing around *) thm A3[where A = "A" and B = "(B \<^bold>\ A)" and C = "A"] thm A3[of "A" "(B \<^bold>\ A)" "A"] text \We show that A1 is redundant\ theorem A1Redundant: shows "A \<^bold>\ A" proof - have 1: "(A \<^bold>\ ((B \<^bold>\ A) \<^bold>\ A)) \<^bold>\ ((A \<^bold>\ (B \<^bold>\ A)) \<^bold>\ (A \<^bold>\ A))" by (rule A3[where B = "(B \<^bold>\ A)" and C = "A"]) have 2: "A \<^bold>\ ((B \<^bold>\ A) \<^bold>\ A)" by (rule A2[where B = "B \<^bold>\ A"]) from 1 2 have 3: "(A \<^bold>\ (B \<^bold>\ A)) \<^bold>\ (A \<^bold>\ A)" by (rule ModusPonens) have 4: "(A \<^bold>\ (B \<^bold>\ A))" by (rule A2) from 3 4 have 5: "A \<^bold>\ A" by (rule ModusPonens) thus ?thesis . qed theorem shows "A \<^bold>\ A" by (metis (full_types) A2 ModusPonens) -- "Sledgehammer even finds a proof without using A3" (*<*) end (*>*)