Theory Propositional_Logic_Class.Classical_Logic_Completeness

chapter ‹ Classical Soundness and Completeness \label{sec:classical-propositional-calculus} ›

theory Classical_Logic_Completeness
  imports Classical_Logic
begin

text ‹ The following presents soundness completeness of the classical propositional
       calculus for propositional semantics. The classical propositional calculus
       is sometimes referred to as the ‹sentential calculus›.
       We give a concrete algebraic data type for propositional
       formulae in \S\ref{sec:classical-calculus-syntax}. We inductively
       define a logical judgement prop for these formulae.
       We also define the Tarski truth relation prop inductively,
       which we present in \S\ref{sec:propositional-semantics}.›

text ‹ The most significant results here are the ‹embedding theorems›.
       These theorems show that the propositional calculus
       can be embedded in any logic extending @{class classical_logic}.
       These theorems are proved in \S\ref{sec:propositional-embedding}. ›

section ‹ Syntax \label{sec:classical-calculus-syntax} ›

text ‹ Here we provide the usual language for formulae in the propositional
       calculus. It contains  ‹falsum› , implication ()›, and a way of
       constructing ‹atomic› propositions λ φ .  φ . Defining the
       language is straight-forward using an algebraic data type. ›

datatype 'a classical_propositional_formula =
      Falsum ("")
    | Proposition 'a (" _ " [45])
    | Implication
        "'a classical_propositional_formula"
        "'a classical_propositional_formula" (infixr "" 70)

section ‹ Propositional Calculus ›

text ‹ In this section we recursively define what a proof is in the classical
       propositional calculus. We provide the familiar ‹K› and ‹S› axioms,
       as well as ‹double negation› and ‹modus ponens›. ›

named_theorems classical_propositional_calculus
  "Rules for the Propositional Calculus"

inductive classical_propositional_calculus ::
  "'a classical_propositional_formula  bool" ("prop _" [60] 55)
  where
     axiom_k [classical_propositional_calculus]:
       "prop φ  ψ  φ"
   | axiom_s [classical_propositional_calculus]:
       "prop (φ  ψ  χ)  (φ  ψ)  φ  χ"
   | double_negation [classical_propositional_calculus]:
       "prop ((φ  )  )  φ"
   | modus_ponens [classical_propositional_calculus]:
        "prop φ  ψ  prop φ  prop ψ"

text ‹ Our proof system for our propositional calculus is trivially
       an instance of @{class classical_logic}. The introduction rules
       for prop naturally reflect the axioms of the classical logic
       axiom class. ›

instantiation classical_propositional_formula
  :: (type) classical_logic
begin
definition [simp]: " = "
definition [simp]: " φ = prop φ"
definition [simp]: "φ  ψ = φ  ψ"
instance by standard (simp add: classical_propositional_calculus)+
end

section ‹ Propositional Semantics \label{sec:propositional-semantics} ›

text ‹ Below we give the typical definition of the Tarski truth relation
       prop. ›

primrec classical_propositional_semantics ::
  "'a set  'a classical_propositional_formula  bool"
  (infix "prop" 65)
  where
       "𝔐 prop  p  = (p  𝔐)"
    |  "𝔐 prop φ  ψ = (𝔐 prop φ  𝔐 prop ψ)"
    |  "𝔐 prop  = False"

text ‹ Soundness of our calculus for these semantics is trivial. ›

theorem classical_propositional_calculus_soundness:
  "prop φ  𝔐 prop φ"
  by (induct rule: classical_propositional_calculus.induct, simp+)

section ‹ Soundness and Completeness Proofs \label{sec:classical-logic-completeness}›

definition strong_classical_propositional_deduction ::
  "'a classical_propositional_formula set
     'a classical_propositional_formula  bool"
  (infix "prop" 65)
  where
    [simp]: "Γ prop φ  Γ  φ"

definition strong_classical_propositional_tarski_truth ::
  "'a classical_propositional_formula set
     'a classical_propositional_formula  bool"
  (infix "prop" 65)
  where
    [simp]: "Γ prop φ   𝔐.( γ  Γ. 𝔐 prop γ)  𝔐 prop φ"

definition theory_propositions ::
  "'a classical_propositional_formula set  'a set" (" _ " [50])
  where
    [simp]: " Γ  = {p . Γ prop  p }"

text ‹ Below we give the main lemma for completeness: the ‹truth lemma›.
       This proof connects the maximally consistent sets developed in \S\ref{sec:implicational-maximally-consistent-sets}
       and \S\ref{sec:mcs} with the semantics given in
       \S\ref{sec:propositional-semantics}. ›

text ‹ All together, the technique we are using essentially follows the
       approach by Blackburn et al. @{cite ‹\S 4.2, pgs. 196-201› blackburnSectionCanonicalModels2001}. ›

lemma truth_lemma:
  assumes "MCS Γ"
  shows "Γ prop φ   Γ  prop φ"
proof (induct φ)
  case Falsum
  then show ?case using assms by auto
next
  case (Proposition x)
  then show ?case by simp
next
  case (Implication ψ χ)
  thus ?case
    unfolding strong_classical_propositional_deduction_def
    by (metis
          assms
          maximally_consistent_set_def
          formula_maximally_consistent_set_def_implication
          classical_propositional_semantics.simps(2)
          implication_classical_propositional_formula_def
          set_deduction_modus_ponens
          set_deduction_reflection)
qed

text ‹ Here the truth lemma above is combined with @{thm formula_maximally_consistent_extension [no_vars]}
 proven in \S\ref{sec:propositional-semantics}.  These theorems together
  give rise to strong completeness for the propositional calculus. ›

theorem classical_propositional_calculus_strong_soundness_and_completeness:
  "Γ prop φ = Γ prop φ"
proof -
  have soundness: "Γ prop φ  Γ prop φ"
  proof -
    assume "Γ prop φ"
    from this obtain Γ' where Γ': "set Γ'  Γ" "Γ' :⊢ φ"
    by (simp add: set_deduction_def, blast)
    {
      fix 𝔐
      assume " γ  Γ. 𝔐 prop γ"
      hence " γ  set Γ'. 𝔐 prop γ" using Γ'(1) by auto
      hence " φ. Γ' :⊢ φ  𝔐 prop φ"
      proof (induct Γ')
        case Nil
        then show ?case
          by (simp add:
                classical_propositional_calculus_soundness
                list_deduction_def)
      next
        case (Cons ψ Γ')
        thus ?case using list_deduction_theorem by fastforce
      qed
      with Γ'(2) have "𝔐 prop φ" by blast
    }
    thus "Γ prop φ"
      using strong_classical_propositional_tarski_truth_def by blast
  qed
  have completeness: "Γ prop φ  Γ prop φ"
  proof (erule contrapos_pp)
    assume "¬ Γ prop φ"
    hence " 𝔐. ( γ  Γ. 𝔐 prop γ)  ¬ 𝔐 prop φ"
    proof -
      from ¬ Γ prop φ obtain Ω where Ω: "Γ  Ω" "φ-MCS Ω"
        by (meson
              formula_consistent_def
              formula_maximally_consistent_extension
              strong_classical_propositional_deduction_def)
      hence "(φ  )  Ω"
        using formula_maximally_consistent_set_def_negation by blast
      hence "¬  Ω  prop φ"
        using Ω
              formula_consistent_def
              formula_maximal_consistency
              formula_maximally_consistent_set_def_def
              truth_lemma
        unfolding strong_classical_propositional_deduction_def
        by blast
      moreover have " γ  Γ.  Ω  prop γ"
        using
          formula_maximal_consistency
          truth_lemma
          Ω
          set_deduction_reflection
        unfolding strong_classical_propositional_deduction_def
        by blast
      ultimately show ?thesis by auto
    qed
    thus "¬ Γ prop φ"
      unfolding strong_classical_propositional_tarski_truth_def
      by simp
  qed
  from soundness completeness show "Γ prop φ = Γ prop φ"
    by linarith
qed

text ‹ For our applications in \S{sec:propositional-embedding},
       we will only need a weaker form of soundness and completeness
       rather than the stronger form proved above.›

theorem classical_propositional_calculus_soundness_and_completeness:
  "prop φ = (𝔐. 𝔐 prop φ)"
  using classical_propositional_calculus_soundness [where φ="φ"]
        classical_propositional_calculus_strong_soundness_and_completeness
            [where φ="φ" and Γ="{}"]
        strong_classical_propositional_deduction_def
            [where φ="φ" and Γ="{}"]
        strong_classical_propositional_tarski_truth_def
            [where φ="φ" and Γ="{}"]
        deduction_classical_propositional_formula_def [where φ="φ"]
        set_deduction_base_theory [where φ="φ"]
  by metis

instantiation classical_propositional_formula
  :: (type) consistent_classical_logic
begin
instance by standard
  (simp add: classical_propositional_calculus_soundness_and_completeness)
end

section ‹ Embedding Theorem For the Propositional Calculus \label{sec:propositional-embedding} ›

text ‹ A recurring technique to prove theorems in logic moving forward is
       ‹embed› our theorem into the classical propositional calculus. ›

text ‹ Using our embedding, we can leverage completeness to turn our
       problem into semantics and dispatch to Isabelle/HOL's classical
       theorem provers.›

text ‹ In future work we may make a tactic for this, but for now we just
       manually leverage the technique throughout our subsequent proofs. ›

primrec (in classical_logic)
   classical_propositional_formula_embedding
   :: "'a classical_propositional_formula  'a" (" _ " [50]) where
     "  p   = p"
   | " φ  ψ  =  φ    ψ "
   | "   = "

theorem (in classical_logic) propositional_calculus:
  "prop φ    φ "
  by (induct rule: classical_propositional_calculus.induct,
      (simp add: axiom_k axiom_s double_negation modus_ponens)+)

text ‹ The following theorem in particular shows that it suffices to
       prove theorems using classical semantics to prove theorems about
       the logic under investigation. ›

theorem (in classical_logic) propositional_semantics:
  "𝔐. 𝔐 prop φ    φ "
  by (simp add:
        classical_propositional_calculus_soundness_and_completeness
        propositional_calculus)

end