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