# Theory Implication_Logic

chapter ‹ Implication Logic \label{sec:implicational-intuitionistic-logic} ›

theory Implication_Logic
imports Main
begin

text ‹ This theory presents the pure implicational fragment of
intuitionistic logic. That is to say, this is the fragment of
intuitionistic logic containing ∗‹implication only›, and no other
connectives nor ∗‹falsum› (i.e., ‹⊥›). We shall refer to this logic as
∗‹implication logic› in future discussion. ›

text ‹ For further reference see @{cite urquhartImplicationalFormulasIntuitionistic1974}.›

section ‹ Axiomatization ›

text ‹ Implication logic can be given by the a Hilbert-style  axiom system,
following Troelstra and Schwichtenberg
@{cite ‹\S 1.3.9, pg. 33› troelstraBasicProofTheory2000}. ›

class implication_logic =
fixes deduction :: "'a ⇒ bool" ("⊢ _" [60] 55)
fixes implication :: "'a ⇒ 'a ⇒ 'a" (infixr "→" 70)
assumes axiom_k: "⊢ φ → ψ → φ"
assumes axiom_s: "⊢ (φ → ψ → χ) → (φ → ψ) → φ → χ"
assumes modus_ponens: "⊢ φ → ψ ⟹ ⊢ φ ⟹ ⊢ ψ"

section ‹ Common Rules ›

lemma (in implication_logic) trivial_implication:
"⊢ φ → φ"
by (meson axiom_k axiom_s modus_ponens)

lemma (in implication_logic) flip_implication:
"⊢ (φ → ψ → χ) → ψ → φ → χ"
by (meson axiom_k axiom_s modus_ponens)

lemma (in implication_logic) hypothetical_syllogism:
"⊢ (ψ → χ) → (φ → ψ) → φ → χ"
by (meson axiom_k axiom_s modus_ponens)

lemma (in implication_logic) flip_hypothetical_syllogism:
"⊢ (ψ → φ) → (φ → χ) → (ψ → χ)"
using modus_ponens flip_implication hypothetical_syllogism by blast

lemma (in implication_logic) implication_absorption:
"⊢ (φ → φ → ψ) → φ → ψ"
by (meson axiom_k axiom_s modus_ponens)

section ‹ Lists of Assumptions ›

subsection ‹ List Implication ›

text ‹ Implication given a list of assumptions can be expressed recursively ›

primrec (in implication_logic)
list_implication :: "'a list ⇒ 'a ⇒ 'a" (infix ":→" 80) where
"[] :→ φ = φ"
| "(ψ # Ψ) :→ φ = ψ → Ψ :→ φ"

subsection ‹ Deduction From a List of Assumptions \label{sec:list-deduction}›

text ‹ Deduction from a list of assumptions can be expressed in terms of
@{term "(:→)"}. ›

definition (in implication_logic) list_deduction :: "'a list ⇒ 'a ⇒ bool" (infix ":⊢" 60)
where
"Γ :⊢ φ ≡ ⊢ Γ :→ φ"

subsection ‹ List Deduction as Implication Logic ›

text ‹ The relation @{term "(:⊢)"} may naturally be interpreted as a
@{term "deduction"} predicate for an instance of implication logic
for a fixed list of assumptions @{term "Γ"}. ›

text ‹ Analogues of the two axioms of implication logic can be
naturally stated using list implication. ›

lemma (in implication_logic) list_implication_axiom_k:
"⊢ φ → Γ :→ φ"
by (induct Γ, (simp, meson axiom_k axiom_s modus_ponens)+)

lemma (in implication_logic) list_implication_axiom_s:
"⊢ Γ :→ (φ → ψ) → Γ :→ φ → Γ :→ ψ"
by (induct Γ,
(simp, meson axiom_k axiom_s modus_ponens hypothetical_syllogism)+)

text ‹ The lemmas @{thm list_implication_axiom_k [no_vars]} and
@{thm list_implication_axiom_s [no_vars]} jointly give rise to an
interpretation of implication logic, where a list of assumptions
@{term "Γ"} play the role of a ∗‹background theory› of @{term "(:⊢)"}. ›

context implication_logic begin
interpretation list_deduction_logic:
implication_logic "λ φ. Γ :⊢ φ" "(→)"
proof qed
(meson
list_deduction_def
axiom_k
axiom_s
modus_ponens
list_implication_axiom_k
list_implication_axiom_s)+
end

text ‹ The following ∗‹weakening› rule can also be derived. ›

lemma (in implication_logic) list_deduction_weaken:
"⊢ φ ⟹ Γ :⊢ φ"
unfolding list_deduction_def
using modus_ponens list_implication_axiom_k
by blast

text ‹ In the case of the empty list, the converse may be established. ›

lemma (in implication_logic) list_deduction_base_theory [simp]:
"[] :⊢ φ ≡ ⊢ φ"
unfolding list_deduction_def
by simp

lemma (in implication_logic) list_deduction_modus_ponens:
"Γ :⊢ φ → ψ ⟹ Γ :⊢ φ ⟹ Γ :⊢ ψ"
unfolding list_deduction_def
using modus_ponens list_implication_axiom_s
by blast

section ‹ The Deduction Theorem ›

text ‹ One result in the meta-theory of implication logic
is the ∗‹deduction theorem›, which is a mechanism for moving
antecedents back and forth from collections of assumptions. ›

text ‹ To develop the deduction theorem, the following two lemmas generalize
@{thm "flip_implication" [no_vars]}. ›

lemma (in implication_logic) list_flip_implication1:
"⊢ (φ # Γ) :→ χ → Γ :→ (φ → χ)"
by (induct Γ,
(simp,
meson
axiom_k
axiom_s
modus_ponens
flip_implication
hypothetical_syllogism)+)

lemma (in implication_logic) list_flip_implication2:
"⊢ Γ :→ (φ → χ) → (φ # Γ) :→ χ"
by (induct Γ,
(simp,
meson
axiom_k
axiom_s
modus_ponens
flip_implication
hypothetical_syllogism)+)

text ‹ Together the two lemmas above suffice to prove a form of
the deduction theorem: ›

theorem (in implication_logic) list_deduction_theorem:
"(φ # Γ) :⊢ ψ = Γ :⊢ φ → ψ"
unfolding list_deduction_def
by (metis modus_ponens list_flip_implication1 list_flip_implication2)

section ‹ Monotonic Growth in Deductive Power ›

text ‹ In logic, for two sets of assumptions @{term "Φ"} and @{term "Ψ"},
if @{term "Ψ ⊆ Φ"} then the latter theory @{term "Φ"} is
said to be ∗‹stronger› than former theory @{term "Ψ"}.
In principle, anything a weaker theory can prove a
stronger theory can prove. One way of saying this is
that deductive power increases monotonically with as the set of
underlying assumptions grow. ›

text ‹ The monotonic growth of deductive power can be expressed as a
meta-theorem in implication logic. ›

text ‹ The lemma @{thm "list_flip_implication2" [no_vars]} presents a means
of ∗‹introducing› assumptions into a list of assumptions when
those assumptions have been arrived at by an implication. The next
lemma presents a means of ∗‹discharging› those assumptions, which can
be used in the monotonic growth theorem to be proved. ›

lemma (in implication_logic) list_implication_removeAll:
"⊢ Γ :→ ψ → (removeAll φ Γ) :→ (φ → ψ)"
proof -
have "∀ ψ. ⊢ Γ :→ ψ → (removeAll φ Γ) :→ (φ → ψ)"
proof(induct Γ)
case Nil
then show ?case by (simp, meson axiom_k)
next
case (Cons χ Γ)
assume
inductive_hypothesis: "∀ ψ. ⊢ Γ :→ ψ → removeAll φ Γ :→ (φ → ψ)"
moreover {
assume "φ ≠ χ"
with inductive_hypothesis
have "∀ ψ. ⊢ (χ # Γ) :→ ψ → removeAll φ (χ # Γ) :→ (φ → ψ)"
by (simp, meson modus_ponens hypothetical_syllogism)
}
moreover {
fix ψ
assume φ_equals_χ: "φ = χ"
moreover with inductive_hypothesis
have "⊢ Γ :→ (χ → ψ) → removeAll φ (χ # Γ) :→ (φ → χ → ψ)" by simp
hence "⊢ Γ :→ (χ → ψ) → removeAll φ (χ # Γ) :→ (φ → ψ)"
by (metis
calculation
modus_ponens
implication_absorption
list_flip_implication1
list_flip_implication2
list_implication.simps(2))
ultimately have "⊢ (χ # Γ) :→ ψ → removeAll φ (χ # Γ) :→ (φ → ψ)"
by (simp,
metis
modus_ponens
hypothetical_syllogism
list_flip_implication1
list_implication.simps(2))
}
ultimately show ?case by simp
qed
thus ?thesis by blast
qed

text ‹ From lemma above presents what is needed to prove that deductive power
for lists is monotonic. ›

theorem (in implication_logic) list_implication_monotonic:
"set Σ ⊆ set Γ ⟹ ⊢ Σ :→ φ → Γ :→ φ"
proof -
assume "set Σ ⊆ set Γ"
moreover have "∀ Σ φ. set Σ ⊆ set Γ ⟶ ⊢ Σ :→ φ → Γ :→ φ"
proof(induct Γ)
case Nil
then show ?case
by (metis
list_implication.simps(1)
list_implication_axiom_k
set_empty
subset_empty)
next
case (Cons ψ Γ)
assume
inductive_hypothesis: "∀Σ φ. set Σ ⊆ set Γ ⟶ ⊢ Σ :→ φ → Γ :→ φ"
{
fix Σ
fix φ
assume Σ_subset_relation: "set Σ ⊆ set (ψ # Γ)"
have "⊢ Σ :→ φ → (ψ # Γ) :→ φ"
proof -
{
assume "set Σ ⊆ set Γ"
hence ?thesis
by (metis
inductive_hypothesis
axiom_k modus_ponens
flip_implication
list_implication.simps(2))
}
moreover {
let ?Δ = "removeAll ψ Σ"
assume "¬ (set Σ ⊆ set Γ)"
hence "set ?Δ ⊆ set Γ"
using Σ_subset_relation by auto
hence "⊢ ?Δ :→ (ψ → φ) → Γ :→ (ψ → φ)"
using inductive_hypothesis by auto
hence "⊢ ?Δ :→ (ψ → φ) → (ψ # Γ) :→ φ"
by (metis
modus_ponens
flip_implication
list_flip_implication2
list_implication.simps(2))
moreover have "⊢ Σ :→ φ → ?Δ :→ (ψ → φ)"
ultimately have ?thesis
using modus_ponens hypothetical_syllogism by blast
}
ultimately show ?thesis by blast
qed
}
thus ?case by simp
qed
ultimately show ?thesis by simp
qed

text ‹ A direct consequence is that deduction from lists of assumptions
is monotonic as well: ›

theorem (in implication_logic) list_deduction_monotonic:
"set Σ ⊆ set Γ ⟹ Σ :⊢ φ ⟹ Γ :⊢ φ"
unfolding list_deduction_def
using modus_ponens list_implication_monotonic
by blast

section ‹ The Deduction Theorem Revisited ›

text ‹ The monotonic nature of deduction allows us to prove another form of
the deduction theorem, where the assumption being discharged is
completely removed from the list of assumptions. ›

theorem (in implication_logic) alternate_list_deduction_theorem:
"(φ # Γ) :⊢ ψ = (removeAll φ Γ) :⊢ φ → ψ"
by (metis
list_deduction_def
modus_ponens
filter_is_subset
list_deduction_monotonic
list_deduction_theorem
list_implication_removeAll
removeAll.simps(2)
removeAll_filter_not_eq)

section ‹ Reflection ›

text ‹ In logic the ∗‹reflection› principle sometimes refers to when
a collection of assumptions can deduce any of its members. It is
automatically derivable from @{thm "list_deduction_monotonic" [no_vars]} among
the other rules provided. ›

lemma (in implication_logic) list_deduction_reflection:
"φ ∈ set Γ ⟹ Γ :⊢ φ"
by (metis
list_deduction_def
insert_subset
list.simps(15)
list_deduction_monotonic
list_implication.simps(2)
list_implication_axiom_k
order_refl)

section ‹ The Cut Rule ›

text ‹ ∗‹Cut› is a rule commonly presented in sequent calculi, dating
back to Gerhard Gentzen's ∗‹Investigations in Logical Deduction› (1935)
@{cite gentzenUntersuchungenUeberLogische1935}›

text ‹ The cut rule is not generally necessary in sequent calculi. It can
often be shown that the rule can be eliminated without reducing the
power of the underlying logic. However, as demonstrated by George
Boolos' ∗‹Don't Eliminate Cut› (1984) @{cite boolosDonEliminateCut1984},
removing the rule can often lead to very inefficient proof systems. ›

text ‹ Here the rule is presented just as a meta theorem. ›

theorem (in implication_logic) list_deduction_cut_rule:
"(φ # Γ) :⊢ ψ ⟹ Δ :⊢ φ ⟹ Γ @ Δ :⊢ ψ"
by (metis
(no_types, lifting)
Un_upper1
Un_upper2
list_deduction_modus_ponens
list_deduction_monotonic
list_deduction_theorem
set_append)

text ‹ The cut rule can also be strengthened to entire lists of propositions. ›

theorem (in implication_logic) strong_list_deduction_cut_rule:
"(Φ @ Γ) :⊢ ψ ⟹ ∀ φ ∈ set Φ. Δ :⊢ φ ⟹ Γ @ Δ :⊢ ψ"
proof -
have "∀ ψ. (Φ @ Γ :⊢ ψ ⟶ (∀ φ ∈ set Φ. Δ :⊢ φ) ⟶ Γ @ Δ :⊢ ψ)"
proof(induct Φ)
case Nil
then show ?case
by (metis
Un_iff
append.left_neutral
list_deduction_monotonic
set_append
subsetI)
next
case (Cons χ Φ) assume inductive_hypothesis:
"∀ ψ. Φ @ Γ :⊢ ψ ⟶ (∀φ∈set Φ. Δ :⊢ φ) ⟶ Γ @ Δ :⊢ ψ"
{
fix ψ χ
assume "(χ # Φ) @ Γ :⊢ ψ"
hence A: "Φ @ Γ :⊢ χ → ψ" using list_deduction_theorem by auto
assume "∀φ ∈ set (χ # Φ). Δ :⊢ φ"
hence B: "∀ φ ∈ set Φ. Δ :⊢ φ"
and C: "Δ :⊢ χ" by auto
from A B have "Γ @ Δ :⊢ χ → ψ" using inductive_hypothesis by blast
with C have "Γ @ Δ :⊢ ψ"
by (meson
list.set_intros(1)
list_deduction_cut_rule
list_deduction_modus_ponens
list_deduction_reflection)
}
thus ?case by simp
qed
moreover assume "(Φ @ Γ) :⊢ ψ"
moreover assume "∀ φ ∈ set Φ. Δ :⊢ φ"
ultimately show ?thesis by blast
qed

section ‹ Sets of Assumptions ›

text ‹ While deduction in terms of lists of assumptions is straight-forward
to define, deduction (and the ∗‹deduction theorem›) is commonly given in
terms of ∗‹sets› of propositions.  This formulation is suited to
establishing strong completeness theorems and compactness theorems. ›

text ‹ The presentation of deduction from a set follows the presentation of
list deduction given for \<^term>‹(:⊢)›. ›

section ‹ Definition of Deduction ›

text ‹ Just as deduction from a list \<^term>‹(:⊢)› can be defined in
terms of \<^term>‹(:→)›, deduction from a ∗‹set› of assumptions
can be expressed in terms of \<^term>‹(:⊢)›. ›

definition (in implication_logic) set_deduction :: "'a set ⇒ 'a ⇒ bool" (infix "⊩" 60)
where
"Γ ⊩ φ ≡ ∃ Ψ. set Ψ  ⊆ Γ ∧ Ψ :⊢ φ"

subsection ‹ Interpretation as Implication Logic ›

text ‹ As in the case of @{term "(:⊢)"}, the relation @{term "(⊩)"} may be
interpreted as @{term "deduction"} predicate for a fixed set of
assumptions @{term "Γ"}. ›

text ‹ The following lemma is given in order to establish this, which asserts
that every implication logic tautology @{term "⊢ φ"}
is also a tautology for @{term "Γ ⊩ φ"}. ›

lemma (in implication_logic) set_deduction_weaken:
"⊢ φ ⟹ Γ ⊩ φ"
using list_deduction_base_theory set_deduction_def by fastforce

text ‹ In the case of the empty set, the converse may be established. ›

lemma (in implication_logic) set_deduction_base_theory:
"{} ⊩ φ ≡ ⊢ φ"
using list_deduction_base_theory set_deduction_def by auto

text ‹ Next, a form of ∗‹modus ponens› is provided for @{term "(⊩)"}. ›

lemma (in implication_logic) set_deduction_modus_ponens:
"Γ ⊩ φ → ψ ⟹ Γ ⊩ φ ⟹ Γ ⊩ ψ"
proof -
assume "Γ ⊩ φ → ψ"
then obtain Φ where A: "set Φ ⊆ Γ" and B: "Φ :⊢ φ → ψ"
using set_deduction_def by blast
assume "Γ ⊩ φ"
then obtain Ψ where C: "set Ψ ⊆ Γ" and D: "Ψ :⊢ φ"
using set_deduction_def by blast
from B D have "Φ @ Ψ :⊢ ψ"
using list_deduction_cut_rule list_deduction_theorem by blast
moreover from A C have "set (Φ @ Ψ) ⊆ Γ" by simp
ultimately show ?thesis
using set_deduction_def by blast
qed

context implication_logic begin
interpretation set_deduction_logic:
implication_logic "λ φ. Γ ⊩ φ" "(→)"
proof
fix φ ψ
show "Γ ⊩ φ → ψ → φ"  by (metis axiom_k set_deduction_weaken)
next
fix φ ψ χ
show "Γ ⊩ (φ → ψ → χ) → (φ → ψ) → φ → χ"
by (metis axiom_s set_deduction_weaken)
next
fix φ ψ
show "Γ ⊩ φ → ψ ⟹ Γ ⊩ φ ⟹ Γ ⊩ ψ"
using set_deduction_modus_ponens by metis
qed
end

section ‹ The Deduction Theorem ›

text ‹ The next result gives the deduction theorem for @{term "(⊩)"}. ›

theorem (in implication_logic) set_deduction_theorem:
"insert φ Γ ⊩ ψ = Γ ⊩ φ → ψ"
proof -
have "Γ ⊩ φ → ψ ⟹ insert φ Γ ⊩ ψ"
by (metis
set_deduction_def
insert_mono
list.simps(15)
list_deduction_theorem)
moreover {
assume "insert φ Γ ⊩ ψ"
then obtain Φ where "set Φ ⊆ insert φ Γ" and "Φ :⊢ ψ"
using set_deduction_def by auto
hence "set (removeAll φ Φ) ⊆ Γ" by auto
moreover from ‹Φ :⊢ ψ› have "removeAll φ Φ :⊢ φ → ψ"
using modus_ponens list_implication_removeAll list_deduction_def
by blast
ultimately have "Γ ⊩ φ → ψ"
using set_deduction_def by blast
}
ultimately show "insert φ Γ ⊩ ψ = Γ ⊩ φ → ψ" by metis
qed

section ‹ Monotonic Growth in Deductive Power ›

text ‹ In contrast to the @{term "(:⊢)"} relation, the proof that the
deductive power of @{term "(⊩)"} grows monotonically with its
assumptions may be fully automated. ›

theorem set_deduction_monotonic:
"Σ ⊆ Γ ⟹ Σ ⊩ φ ⟹ Γ ⊩ φ"
by (meson dual_order.trans set_deduction_def)

section ‹ The Deduction Theorem Revisited ›

text ‹ As a consequence of the fact that @{thm "set_deduction_monotonic" [no_vars]}
is automatically provable, an alternate ∗‹deduction theorem› where the
discharged assumption is completely removed from the set of assumptions
is just a consequence of the more conventional
@{thm "set_deduction_theorem" [no_vars]} rule and some basic set identities. ›

theorem (in implication_logic) alternate_set_deduction_theorem:
"insert φ Γ ⊩ ψ = Γ - {φ} ⊩ φ → ψ"
by (metis insert_Diff_single set_deduction_theorem)

section ‹ Reflection ›

text ‹ Just as in the case of @{term "(:⊢)"}, deduction from sets of
assumptions makes true the ∗‹reflection principle› and is
automatically provable. ›

theorem (in implication_logic) set_deduction_reflection:
"φ ∈ Γ ⟹ Γ ⊩ φ"
by (metis
Set.set_insert
list_implication.simps(1)
list_implication_axiom_k
set_deduction_theorem
set_deduction_weaken)

section ‹ The Cut Rule ›

text ‹ The final principle of @{term "(⊩)"} presented is the ∗‹cut rule›. ›

text ‹ First, the weak form of the rule is established. ›

theorem (in implication_logic) set_deduction_cut_rule:
"insert φ Γ ⊩ ψ ⟹ Δ ⊩ φ ⟹ Γ ∪ Δ ⊩ ψ"
proof -
assume "insert φ Γ ⊩ ψ"
hence "Γ ⊩ φ → ψ" using set_deduction_theorem by auto
hence "Γ ∪ Δ ⊩ φ → ψ" using set_deduction_def by auto
moreover assume "Δ ⊩ φ"
hence "Γ ∪ Δ ⊩ φ" using set_deduction_def by auto
ultimately show ?thesis using set_deduction_modus_ponens by metis
qed

text ‹ Another lemma is shown next in order to establish the strong form
of the cut rule. The lemma shows the existence of a ∗‹covering list› of
assumptions \<^term>‹Ψ› in the event some set of assumptions
\<^term>‹Δ› proves everything in a finite set of assumptions
\<^term>‹Φ›. ›

lemma (in implication_logic) finite_set_deduction_list_deduction:
assumes "finite Φ"
and "∀ φ ∈ Φ. Δ ⊩ φ"
shows "∃Ψ. set Ψ ⊆ Δ ∧ (∀φ ∈ Φ. Ψ :⊢ φ)"
using assms
proof(induct Φ rule: finite_induct)
case empty thus ?case by (metis all_not_in_conv empty_subsetI set_empty)
next
case (insert χ Φ)
assume "∀φ ∈ Φ. Δ ⊩ φ ⟹ ∃Ψ. set Ψ ⊆ Δ ∧ (∀φ ∈ Φ. Ψ :⊢ φ)"
and "∀φ ∈ insert χ Φ. Δ ⊩ φ"
hence "∃Ψ. set Ψ ⊆ Δ ∧ (∀φ∈Φ. Ψ :⊢ φ)" and "Δ ⊩ χ" by simp+
then obtain Ψ⇩1 Ψ⇩2 where
"set (Ψ⇩1 @ Ψ⇩2) ⊆ Δ"
"∀φ ∈ Φ. Ψ⇩1 :⊢ φ"
"Ψ⇩2 :⊢ χ"
using set_deduction_def by auto
moreover from this have "∀φ ∈ (insert χ Φ). Ψ⇩1 @ Ψ⇩2 :⊢ φ"
by (metis
insert_iff
le_sup_iff
list_deduction_monotonic
order_refl set_append)
ultimately show ?case by blast
qed

text ‹ With @{thm finite_set_deduction_list_deduction [no_vars]} the strengthened
form of the cut rule can be given. ›

theorem (in implication_logic) strong_set_deduction_cut_rule:
assumes "Φ ∪ Γ ⊩ ψ"
and "∀ φ ∈ Φ. Δ ⊩ φ"
shows "Γ ∪ Δ ⊩ ψ"
proof -
obtain Σ where
A: "set Σ  ⊆ Φ ∪ Γ" and
B: "Σ :⊢ ψ"
using assms(1) set_deduction_def
by auto+
obtain Φ' Γ' where
C: "set Φ' = set Σ ∩ Φ" and
D: "set Γ' = set Σ ∩ Γ"
by (metis inf_sup_aci(1) inter_set_filter)+
then have "set (Φ' @ Γ') = set Σ" using A by auto
hence E: "Φ' @ Γ' :⊢ ψ" using B list_deduction_monotonic by blast
hence "∀ φ ∈ set Φ'. Δ ⊩ φ" using assms(2) C by auto
from this obtain Δ' where "set Δ' ⊆ Δ" and "∀ φ ∈ set Φ'. Δ' :⊢ φ"
using finite_set_deduction_list_deduction by blast
with strong_list_deduction_cut_rule D E
have "set (Γ' @ Δ') ⊆ Γ ∪ Δ" and "Γ' @ Δ' :⊢ ψ" by auto
thus ?thesis using set_deduction_def by blast
qed

section ‹Maximally Consistent Sets For Implication Logic \label{sec:implicational-maximally-consistent-sets}›

text ‹ ∗‹Maximally Consistent Sets› are a common construction for proving
completeness of logical calculi.  For a classic presentation, see
Dirk van Dalen's ∗‹Logic and Structure› (2013, \S1.5, pgs. 42--45)
@{cite vandalenLogicStructure2013}. ›

text ‹ Maximally consistent sets will form the foundation of all of the
model theory we will employ in this text. In fact, apart from
classical logic semantics, conventional model theory will not be
used at all. ›

text ‹ The models we are centrally concerned are derived from maximally
consistent sets. These include probability measures used in completeness
theorems of probability logic found in \S\ref{sec:probability-logic-completeness},
as well as arbitrage protection and trading strategies stipulated by
our formulation of the ∗‹Dutch Book Theorem› we present in
\S\ref{chap:dutch-book-theorem}. ›

text ‹ Since implication logic does not have ∗‹falsum›, consistency is
defined relative to a formula \<^term>‹φ›. ›

definition (in implication_logic)
formula_consistent :: "'a ⇒ 'a set ⇒ bool" ("_-consistent _" [100] 100)
where
[simp]: "φ-consistent Γ ≡ ¬ (Γ ⊩ φ)"

text ‹ Since consistency is defined relative to some \<^term>‹φ›,
∗‹maximal consistency› is presented as asserting that either
\<^term>‹ψ› or \<^term>‹ψ → φ› is in the consistent set \<^term>‹Γ›,
for all \<^term>‹ψ›.  This coincides with the traditional definition in
classical logic when \<^term>‹φ› is ∗‹falsum›. ›

definition (in implication_logic)
formula_maximally_consistent_set_def :: "'a ⇒ 'a set ⇒ bool" ("_-MCS _" [100] 100)
where
[simp]: "φ-MCS Γ ≡ (φ-consistent Γ) ∧ (∀ ψ. ψ ∈ Γ ∨ (ψ → φ) ∈ Γ)"

text ‹ Every consistent set \<^term>‹Γ› may be extended to a maximally
consistent set. ›

text ‹ However, no assumption is made regarding the cardinality of the types
of an instance of @{class implication_logic}. ›

text ‹ As a result, typical proofs that assume a countable domain are not
suitable.  Our proof leverages ∗‹Zorn's lemma›. ›

lemma (in implication_logic) formula_consistent_extension:
assumes "φ-consistent Γ"
shows "(φ-consistent (insert ψ Γ)) ∨ (φ-consistent (insert (ψ → φ) Γ))"
proof -
{
assume "¬ φ-consistent insert ψ Γ"
hence "Γ ⊩ ψ → φ"
using set_deduction_theorem
unfolding formula_consistent_def
by simp
hence "φ-consistent insert (ψ → φ) Γ"
by (metis Un_absorb assms formula_consistent_def set_deduction_cut_rule)
}
thus ?thesis by blast
qed

theorem (in implication_logic) formula_maximally_consistent_extension:
assumes "φ-consistent Γ"
shows "∃ Ω. (φ-MCS Ω) ∧ Γ ⊆ Ω"
proof -
let ?Γ_extensions = "{Σ. (φ-consistent Σ) ∧ Γ ⊆ Σ}"
have "∃ Ω ∈ ?Γ_extensions. ∀Σ ∈ ?Γ_extensions. Ω ⊆ Σ ⟶ Σ = Ω"
proof (rule subset_Zorn)
fix 𝒞 :: "'a set set"
assume subset_chain_𝒞: "subset.chain ?Γ_extensions 𝒞"
hence 𝒞:  "∀ Σ ∈ 𝒞. Γ ⊆ Σ" "∀ Σ ∈ 𝒞. φ-consistent Σ"
unfolding subset.chain_def
by blast+
show "∃ Ω ∈ ?Γ_extensions. ∀ Σ ∈ 𝒞. Σ ⊆ Ω"
proof cases
assume "𝒞 = {}" thus ?thesis using assms by blast
next
let ?Ω = "⋃ 𝒞"
assume "𝒞 ≠ {}"
hence "Γ ⊆ ?Ω" by (simp add: 𝒞(1) less_eq_Sup)
moreover have "φ-consistent ?Ω"
proof -
{
assume "¬ φ-consistent ?Ω"
then obtain ω where ω:
"finite ω"
"ω ⊆ ?Ω"
"¬ φ-consistent ω"
unfolding
formula_consistent_def
set_deduction_def
by auto
from ω(1) ω(2) have "∃ Σ ∈ 𝒞. ω ⊆ Σ"
proof (induct ω rule: finite_induct)
case empty thus ?case using ‹𝒞 ≠ {}› by blast
next
case (insert ψ ω)
from this obtain Σ⇩1 Σ⇩2 where
Σ⇩1:
"ω ⊆ Σ⇩1"
"Σ⇩1 ∈ 𝒞"
and Σ⇩2:
"ψ ∈ Σ⇩2"
"Σ⇩2 ∈ 𝒞"
by auto
hence "Σ⇩1 ⊆ Σ⇩2 ∨ Σ⇩2 ⊆ Σ⇩1"
using subset_chain_𝒞
unfolding subset.chain_def
by blast
hence "(insert ψ ω) ⊆ Σ⇩1 ∨ (insert ψ ω) ⊆ Σ⇩2"
using Σ⇩1 Σ⇩2 by blast
thus ?case using Σ⇩1 Σ⇩2 by blast
qed
hence "∃ Σ ∈ 𝒞. (φ-consistent Σ) ∧ ¬ (φ-consistent Σ)"
using 𝒞(2) ω(3)
unfolding
formula_consistent_def
set_deduction_def
by auto
hence "False" by auto
}
thus ?thesis by blast
qed
ultimately show ?thesis by blast
qed
qed
then obtain Ω where Ω:
"Ω ∈ ?Γ_extensions"
"∀Σ ∈ ?Γ_extensions. Ω ⊆ Σ ⟶ Σ = Ω"
by auto+
{
fix ψ
have "(φ-consistent insert ψ Ω) ∨ (φ-consistent insert (ψ → φ) Ω)"
"Γ ⊆ insert ψ Ω"
"Γ ⊆ insert (ψ → φ) Ω"
using Ω(1) formula_consistent_extension formula_consistent_def
by auto
hence "insert ψ Ω ∈ ?Γ_extensions
∨ insert (ψ → φ) Ω ∈ ?Γ_extensions"
by blast
hence "ψ ∈ Ω ∨ (ψ → φ) ∈ Ω" using Ω(2) by blast
}
thus ?thesis
using Ω(1)
unfolding formula_maximally_consistent_set_def_def
by blast
qed

text ‹ Finally, maximally consistent sets contain anything that can be deduced
from them, and model a form of ∗‹modus ponens›. ›

lemma (in implication_logic) formula_maximally_consistent_set_def_reflection:
"φ-MCS Γ ⟹ ψ ∈ Γ = Γ ⊩ ψ"
proof -
assume "φ-MCS Γ"
{
assume "Γ ⊩ ψ"
moreover from ‹φ-MCS Γ› have "ψ ∈ Γ ∨ (ψ → φ) ∈ Γ" "¬ Γ ⊩ φ"
unfolding
formula_maximally_consistent_set_def_def
formula_consistent_def
by auto
ultimately have "ψ ∈ Γ"
using set_deduction_reflection set_deduction_modus_ponens
by metis
}
thus "ψ ∈ Γ = Γ ⊩ ψ"
using set_deduction_reflection
by metis
qed

theorem (in implication_logic) formula_maximally_consistent_set_def_implication_elimination:
assumes "φ-MCS Ω"
shows "(ψ → χ) ∈ Ω ⟹ ψ ∈ Ω ⟹ χ ∈ Ω"
using
assms
formula_maximally_consistent_set_def_reflection
set_deduction_modus_ponens
by blast

text ‹ This concludes our introduction to implication logic. ›

end