Theory Propositional_Logic_Class.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 "⊢ Σ :→ φ → ?Δ :→ (ψ → φ)"
            by (simp add: local.list_implication_removeAll)
          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