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