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