# Theory 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 "?Γ :⊢ (φ → ⊥) → ψ"
"?Γ :⊢ ψ → ⊥"
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