Theory Propositional_Logic_Class.Classical_Logic

chapter ‹ Classical Propositional Logic \label{sec:classical-propositional-logic}›

theory Classical_Logic
  imports Implication_Logic
begin

text ‹ This theory presents ∗‹classical propositional logic›, which is
       classical logic without quantifiers. ›

section ‹ Axiomatization ›

text ‹ Classical propositional logic can be given by the following
       Hilbert-style axiom system.  It is @{class implication_logic}
       extended with ∗‹falsum› and double negation. ›

class classical_logic = implication_logic +
  fixes falsum :: "'a" (‹⊥›)
  assumes double_negation: "⊢ (((φ → ⊥) → ⊥) → φ)"

text ‹ In some cases it is useful to assume consistency as an axiom: ›

class consistent_classical_logic = classical_logic +
  assumes consistency: "¬ ⊢ ⊥"

section ‹ Common Rules ›

text ‹ There are many common tautologies in classical logic.  Once we have
       established ∗‹completeness› in \S\ref{sec:classical-propositional-calculus},
       we will be able to leverage Isabelle/HOL's automation for proving
       these elementary results. ›

text ‹ In order to bootstrap completeness, we develop some common lemmas
       using classical deduction alone. ›

lemma (in classical_logic)
  ex_falso_quodlibet: "⊢ ⊥ → φ"
  using axiom_k double_negation modus_ponens hypothetical_syllogism
  by blast

lemma (in classical_logic)
  Contraposition: "⊢ ((φ → ⊥) → (ψ → ⊥)) → ψ → φ"
proof -
  have "[φ → ⊥, ψ, (φ → ⊥) → (ψ → ⊥)] :⊢ ⊥"
    using flip_implication list_deduction_theorem list_implication.simps(1)
    unfolding list_deduction_def
    by presburger
  hence "[ψ, (φ → ⊥) → (ψ → ⊥)] :⊢ (φ → ⊥) → ⊥"
    using list_deduction_theorem by blast
  hence "[ψ, (φ → ⊥) → (ψ → ⊥)] :⊢ φ"
    using double_negation list_deduction_weaken list_deduction_modus_ponens
    by blast
  thus ?thesis
    using list_deduction_base_theory list_deduction_theorem by blast
qed

lemma (in classical_logic)
  double_negation_converse: "⊢ φ → (φ → ⊥) → ⊥"
  by (meson axiom_k modus_ponens flip_implication)

text ‹The following lemma is sometimes referred to as
      ∗‹The Principle of Pseudo-Scotus›@{cite bobenriethOriginsUseArgument2010}.›

lemma (in classical_logic)
  pseudo_scotus: "⊢ (φ → ⊥) → φ → ψ"
  using ex_falso_quodlibet modus_ponens hypothetical_syllogism by blast

text ‹Another popular lemma is attributed to Charles Sanders Peirce,
      and has come to be known as ∗‹Peirces Law›@{cite peirceAlgebraLogicContribution1885}.›

lemma (in classical_logic) Peirces_law:
  "⊢ ((φ → ψ) → φ) → φ"
proof -
  have "[φ → ⊥, (φ → ψ) → φ] :⊢ φ → ψ"
    using
      pseudo_scotus
      list_deduction_theorem
      list_deduction_weaken
    by blast
  hence "[φ → ⊥, (φ → ψ) → φ] :⊢ φ"
    by (meson
          list.set_intros(1)
          list_deduction_reflection
          list_deduction_modus_ponens
          set_subset_Cons
          subsetCE)
  hence "[φ → ⊥, (φ → ψ) → φ] :⊢ ⊥"
    by (meson
          list.set_intros(1)
          list_deduction_modus_ponens
          list_deduction_reflection)
  hence "[(φ → ψ) → φ] :⊢ (φ → ⊥) → ⊥"
    using list_deduction_theorem by blast
  hence "[(φ → ψ) → φ] :⊢ φ"
    using double_negation
          list_deduction_modus_ponens
          list_deduction_weaken
    by blast
  thus ?thesis
    using list_deduction_def
    by auto
qed

lemma (in classical_logic) excluded_middle_elimination:
  "⊢ (φ → ψ) → ((φ → ⊥) → ψ) → ψ"
proof -
  let ?Γ = "[ψ → ⊥, φ → ψ, (φ → ⊥) → ψ]"
  have "?Γ :⊢ (φ → ⊥) → ψ"
       "?Γ :⊢ ψ → ⊥"
    by (simp add: list_deduction_reflection)+
  hence "?Γ :⊢ (φ → ⊥) → ⊥"
    by (meson
          flip_hypothetical_syllogism
          list_deduction_base_theory
          list_deduction_monotonic
          list_deduction_theorem
          set_subset_Cons)
  hence "?Γ :⊢ φ"
    using
      double_negation
      list_deduction_modus_ponens
      list_deduction_weaken
    by blast
  hence "?Γ :⊢ ψ"
    by (meson
          list.set_intros(1)
          list_deduction_modus_ponens
          list_deduction_reflection
          set_subset_Cons subsetCE)
  hence "[φ → ψ, (φ → ⊥) → ψ] :⊢ ψ"
    using
      Peirces_law
      list_deduction_modus_ponens
      list_deduction_theorem
      list_deduction_weaken
    by blast
  thus ?thesis
    unfolding list_deduction_def
    by simp
qed

section ‹ Maximally Consistent Sets For Classical Logic \label{sec:mcs}›

text ‹ ∗‹Relativized› maximally consistent sets were introduced in
       \S\ref{sec:implicational-maximally-consistent-sets}.
       Often this is exactly what we want in a proof.
       A completeness theorem typically starts by assuming \<^term>‹φ› is
       not provable, then finding a \<^term>‹φ-MCS Γ› which gives rise to a model
       which does not make \<^term>‹φ› true. ›

text ‹ A more conventional presentation says that \<^term>‹Γ› is maximally
       consistent if and only if  \<^term>‹¬ (Γ ⊩ ⊥)› and
       \<^term>‹∀ ψ. ψ ∈ Γ ∨ (ψ → φ) ∈ Γ›. This conventional presentation
       will come up when formulating \textsc{MaxSAT} in
       \S\ref{sec:abstract-maxsat}. This in turn allows us to formulate
       \textsc{MaxSAT} completeness for probability inequalities in
       \S\ref{subsec:maxsat-completeness}, and reduce checking if a strategy
       will always lose money or if it will always make money if matched to
       bounded \textsc{MaxSAT} as part of our proof of the ∗‹Dutch Book Theorem›
       in \S\ref{subsec:guardian-dutch-book-maxsat-reduction} and \S\ref{subsec:market-depth-dutch-book-maxsat-reduction}
       respectively. ›

definition (in classical_logic)
  consistent :: "'a set ⇒ bool" where
    [simp]: "consistent Γ ≡ ⊥-consistent Γ"

definition (in classical_logic)
  maximally_consistent_set :: "'a set ⇒ bool" (‹MCS›) where
    [simp]: "MCS Γ ≡ ⊥-MCS Γ"

lemma (in classical_logic)
  formula_maximally_consistent_set_def_negation: "φ-MCS Γ ⟹ φ → ⊥ ∈ Γ"
proof -
  assume "φ-MCS Γ"
  {
    assume "φ → ⊥ ∉ Γ"
    hence "(φ → ⊥) → φ ∈ Γ"
      using ‹φ-MCS Γ›
      unfolding formula_maximally_consistent_set_def_def
      by blast
    hence "Γ ⊩ (φ → ⊥) → φ"
      using set_deduction_reflection
      by simp
    hence "Γ ⊩ φ"
      using
        Peirces_law
        set_deduction_modus_ponens
        set_deduction_weaken
      by metis
    hence "False"
      using ‹φ-MCS Γ›
      unfolding
        formula_maximally_consistent_set_def_def
        formula_consistent_def
      by simp
  }
  thus ?thesis by blast
qed

text ‹ Relative maximal consistency and conventional maximal consistency in
       fact coincide in classical logic. ›

lemma (in classical_logic)
  formula_maximal_consistency: "(∃φ. φ-MCS Γ) = MCS Γ"
proof -
  {
    fix φ
    have "φ-MCS Γ ⟹ MCS Γ"
    proof -
      assume "φ-MCS Γ"
      have "consistent Γ"
        using
          ‹φ-MCS Γ›
          ex_falso_quodlibet [where φ="φ"]
          set_deduction_weaken [where Γ="Γ"]
          set_deduction_modus_ponens
        unfolding
          formula_maximally_consistent_set_def_def
          consistent_def
          formula_consistent_def
        by metis
      moreover {
        fix ψ
        have "ψ → ⊥ ∉ Γ ⟹ ψ ∈ Γ"
        proof -
          assume "ψ → ⊥ ∉ Γ"
          hence "(ψ → ⊥) → φ ∈ Γ"
            using ‹φ-MCS Γ›
            unfolding formula_maximally_consistent_set_def_def
            by blast
          hence "Γ ⊩ (ψ → ⊥) → φ"
            using set_deduction_reflection
            by simp
          also have "Γ ⊩ φ → ⊥"
            using ‹φ-MCS Γ›
                  formula_maximally_consistent_set_def_negation
                  set_deduction_reflection
            by simp
          hence "Γ ⊩ (ψ → ⊥) → ⊥"
            using calculation
                  hypothetical_syllogism
                    [where φ="ψ → ⊥" and ψ="φ" and χ="⊥"]
                  set_deduction_weaken
                    [where Γ="Γ"]
                  set_deduction_modus_ponens
            by metis
          hence "Γ ⊩ ψ"
            using double_negation
                    [where φ="ψ"]
                  set_deduction_weaken
                    [where Γ="Γ"]
                  set_deduction_modus_ponens
            by metis
          thus ?thesis
            using ‹φ-MCS Γ›
                  formula_maximally_consistent_set_def_reflection
            by blast
       qed
      }
      ultimately show ?thesis
        unfolding maximally_consistent_set_def
                  formula_maximally_consistent_set_def_def
                  formula_consistent_def
                  consistent_def
        by blast
    qed
  }
  thus ?thesis
    unfolding maximally_consistent_set_def
    by metis
qed

text ‹ Finally, classical logic allows us to strengthen
       @{thm formula_maximally_consistent_set_def_implication_elimination [no_vars]} to a
       biconditional. ›

lemma (in classical_logic)
  formula_maximally_consistent_set_def_implication:
  assumes "φ-MCS Γ"
  shows "ψ → χ ∈ Γ = (ψ ∈ Γ ⟶ χ ∈ Γ)"
proof -
  {
    assume hypothesis: "ψ ∈ Γ ⟶ χ ∈ Γ"
    {
      assume "ψ ∉ Γ"
      have "∀ψ. φ → ψ ∈ Γ"
        by (meson assms
                  formula_maximally_consistent_set_def_negation
                  formula_maximally_consistent_set_def_implication_elimination
                  formula_maximally_consistent_set_def_reflection
                  pseudo_scotus set_deduction_weaken)
      then have "∀χ ψ. insert χ Γ ⊩ ψ ∨ χ → φ ∉ Γ"
        by (meson assms
                  axiom_k
                  formula_maximally_consistent_set_def_reflection
                  set_deduction_modus_ponens
                  set_deduction_theorem
                  set_deduction_weaken)
      hence "ψ → χ ∈ Γ"
        by (meson ‹ψ ∉ Γ›
                  assms
                  formula_maximally_consistent_set_def_def
                  formula_maximally_consistent_set_def_reflection
                  set_deduction_theorem)
    }
    moreover {
      assume "χ ∈ Γ"
      hence "ψ → χ ∈ Γ"
        by (metis assms
                  calculation
                  insert_absorb
                  formula_maximally_consistent_set_def_reflection
                  set_deduction_theorem)
    }
    ultimately have  "ψ → χ ∈ Γ" using hypothesis by blast
  }
  thus ?thesis
    using assms
          formula_maximally_consistent_set_def_implication_elimination
    by metis
qed

end