Theory Epistemic_Logic

(*
  File:      Epistemic_Logic.thy
  Author:    Asta Halkjær From

  This work is a formalization of epistemic logic.
  It includes proofs of soundness and completeness for the axiom system K.
  The completeness proof is based on the textbook "Reasoning About Knowledge"
  by Fagin, Halpern, Moses and Vardi (MIT Press 1995).
  The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs
  are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema
  (Cambridge University Press 2001).
*)

theory Epistemic_Logic imports Maximal_Consistent_Sets begin

section ‹Syntax›

type_synonym id = string

datatype 'i fm
  = FF (‹❙⊥›)
  | Pro id
  | Dis ‹'i fm› ‹'i fm› (infixr ‹❙∨› 60)
  | Con ‹'i fm› ‹'i fm› (infixr ‹❙∧› 65)
  | Imp ‹'i fm› ‹'i fm› (infixr ‹❙⟶› 55)
  | K 'i ‹'i fm›

abbreviation TT (‹❙⊤›) where
  ‹TT ≡ ❙⊥ ❙⟶ ❙⊥›

abbreviation Neg (‹❙¬ _› [70] 70) where
  ‹Neg p ≡ p ❙⟶ ❙⊥›

abbreviation ‹L i p ≡ ❙¬ K i (❙¬ p)›

section ‹Semantics›

record ('i, 'w) frame =
  𝒲 :: ‹'w set›
  𝒦 :: ‹'i ⇒ 'w ⇒ 'w set›

record ('i, 'w) kripke =
  ‹('i, 'w) frame› +
  π :: ‹'w ⇒ id ⇒ bool›

primrec semantics :: ‹('i, 'w) kripke ⇒ 'w ⇒ 'i fm ⇒ bool› (‹_, _ ⊨ _› [50, 50, 50] 50) where
  ‹M, w ⊨ ❙⊥ ⟷ False›
| ‹M, w ⊨ Pro x ⟷ π M w x›
| ‹M, w ⊨ p ❙∨ q ⟷ M, w ⊨ p ∨ M, w ⊨ q›
| ‹M, w ⊨ p ❙∧ q ⟷ M, w ⊨ p ∧ M, w ⊨ q›
| ‹M, w ⊨ p ❙⟶ q ⟷ M, w ⊨ p ⟶ M, w ⊨ q›
| ‹M, w ⊨ K i p ⟷ (∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ p)›

abbreviation validStar :: ‹(('i, 'w) kripke ⇒ bool) ⇒ 'i fm set ⇒ 'i fm ⇒ bool›
  (‹_; _ ⊫⋆ _› [50, 50, 50] 50) where
  ‹P; G ⊫⋆ p ≡ ∀M. P M ⟶
    (∀w ∈ 𝒲 M. (∀q ∈ G. M, w ⊨ q) ⟶ M, w ⊨ p)›

section ‹S5 Axioms›

definition reflexive :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹reflexive M ≡ ∀i. ∀w ∈ 𝒲 M. w ∈ 𝒦 M i w›
 
definition symmetric :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹symmetric M ≡ ∀i. ∀v ∈ 𝒲 M. ∀w ∈ 𝒲 M. v ∈ 𝒦 M i w ⟷ w ∈ 𝒦 M i v›

definition transitive :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹transitive M ≡ ∀i. ∀u ∈ 𝒲 M. ∀v ∈ 𝒲 M. ∀w ∈ 𝒲 M.
    w ∈ 𝒦 M i v ∧ u ∈ 𝒦 M i w ⟶ u ∈ 𝒦 M i v›

abbreviation refltrans :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹refltrans M ≡ reflexive M ∧ transitive M›

abbreviation equivalence :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹equivalence M ≡ reflexive M ∧ symmetric M ∧ transitive M›

definition Euclidean :: ‹('i, 'w, 'c) frame_scheme ⇒ bool› where
  ‹Euclidean M ≡ ∀i. ∀u ∈ 𝒲 M. ∀v ∈ 𝒲 M. ∀w ∈ 𝒲 M.
    v ∈ 𝒦 M i u ⟶ w ∈ 𝒦 M i u ⟶ w ∈ 𝒦 M i v›

lemma Imp_intro [intro]: ‹(M, w ⊨ p ⟹ M, w ⊨ q) ⟹ M, w ⊨ p ❙⟶ q›
  by simp

theorem distribution: ‹M, w ⊨ K i p ❙∧ K i (p ❙⟶ q) ❙⟶ K i q›
proof
  assume ‹M, w ⊨ K i p ❙∧ K i (p ❙⟶ q)›
  then have ‹M, w ⊨ K i p› ‹M, w ⊨ K i (p ❙⟶ q)›
    by simp_all
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ p› ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ p ❙⟶ q›
    by simp_all
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ q›
    by simp
  then show ‹M, w ⊨ K i q›
    by simp
qed

theorem generalization:
  fixes M :: ‹('i, 'w) kripke›
  assumes ‹∀(M :: ('i, 'w) kripke). ∀w ∈ 𝒲 M. M, w ⊨ p› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨ K i p›
proof -
  have ‹∀w' ∈ 𝒲 M ∩ 𝒦 M i w. M, w' ⊨ p›
    using assms by blast
  then show ‹M, w ⊨ K i p›
    by simp
qed

theorem truth:
  assumes ‹reflexive M› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨ K i p ❙⟶ p›
proof
  assume ‹M, w ⊨ K i p›
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ p›
    by simp
  moreover have ‹w ∈ 𝒦 M i w›
    using ‹reflexive M› ‹w ∈ 𝒲 M› unfolding reflexive_def by blast
  ultimately show ‹M, w ⊨ p›
    using ‹w ∈ 𝒲 M› by simp
qed

theorem pos_introspection:
  assumes ‹transitive M› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨ K i p ❙⟶ K i (K i p)›
proof
  assume ‹M, w ⊨ K i p›
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ p›
    by simp
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. ∀u ∈ 𝒲 M ∩ 𝒦 M i v. M, u ⊨ p›
    using ‹transitive M› ‹w ∈ 𝒲 M› unfolding transitive_def by blast
  then have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ K i p›
    by simp
  then show ‹M, w ⊨ K i (K i p)›
    by simp
qed

theorem neg_introspection:
  assumes ‹symmetric M› ‹transitive M› ‹w ∈ 𝒲 M›
  shows ‹M, w ⊨ ❙¬ K i p ❙⟶ K i (❙¬ K i p)›
proof
  assume ‹M, w ⊨ ❙¬ (K i p)›
  then obtain u where ‹u ∈ 𝒦 M i w› ‹¬ (M, u ⊨ p)› ‹u ∈ 𝒲 M›
    by auto
  moreover have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. u ∈ 𝒲 M ∩ 𝒦 M i v›
    using ‹u ∈ 𝒦 M i w› ‹symmetric M› ‹transitive M› ‹u ∈ 𝒲 M› ‹w ∈ 𝒲 M›
    unfolding symmetric_def transitive_def by blast
  ultimately have ‹∀v ∈ 𝒲 M ∩ 𝒦 M i w. M, v ⊨ ❙¬ K i p›
    by auto
  then show ‹M, w ⊨ K i (❙¬ K i p)›
    by simp
qed

section ‹Normal Modal Logic›

primrec eval :: ‹(id ⇒ bool) ⇒ ('i fm ⇒ bool) ⇒ 'i fm ⇒ bool› where
  ‹eval _ _ ❙⊥ = False›
| ‹eval g _ (Pro x) = g x›
| ‹eval g h (p ❙∨ q) = (eval g h p ∨ eval g h q)›
| ‹eval g h (p ❙∧ q) = (eval g h p ∧ eval g h q)›
| ‹eval g h (p ❙⟶ q) = (eval g h p ⟶ eval g h q)›
| ‹eval _ h (K i p) = h (K i p)›

abbreviation ‹tautology p ≡ ∀g h. eval g h p›

inductive AK :: ‹('i fm ⇒ bool) ⇒ 'i fm ⇒ bool› (‹_ ⊢ _› [50, 50] 50)
  for A :: ‹'i fm ⇒ bool› where
    A1: ‹tautology p ⟹ A ⊢ p›
  | A2: ‹A ⊢ K i p ❙∧ K i (p ❙⟶ q) ❙⟶ K i q›
  | Ax: ‹A p ⟹ A ⊢ p›
  | R1: ‹A ⊢ p ⟹ A ⊢ p ❙⟶ q ⟹ A ⊢ q›
  | R2: ‹A ⊢ p ⟹ A ⊢ K i p›

primrec imply :: ‹'i fm list ⇒ 'i fm ⇒ 'i fm› (infixr ‹❙↝› 56) where
  ‹([] ❙↝ q) = q›
| ‹(p # ps ❙↝ q) = (p ❙⟶ ps ❙↝ q)›

abbreviation AK_assms (‹_; _ ⊢ _› [50, 50, 50] 50) where
  ‹A; G ⊢ p ≡ ∃qs. set qs ⊆ G ∧ (A ⊢ qs ❙↝ p)›

section ‹Soundness›

lemma eval_semantics:
  ‹eval (pi w) (λq. ⦇𝒲 = W, 𝒦 = r, π = pi⦈, w ⊨ q) p = (⦇𝒲 = W, 𝒦 = r, π = pi⦈, w ⊨ p)›
  by (induct p) simp_all

lemma tautology:
  assumes ‹tautology p›
  shows ‹M, w ⊨ p›
proof -
  from assms have ‹eval (g w) (λq. ⦇𝒲 = W, 𝒦 = r, π = g⦈, w ⊨ q) p› for W g r
    by simp
  then have ‹⦇𝒲 = W, 𝒦 = r, π = g⦈, w ⊨ p› for W g r
    using eval_semantics by fast
  then show ‹M, w ⊨ p›
    by (metis kripke.cases)
qed

theorem soundness:
  assumes ‹⋀M w p. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  shows ‹A ⊢ p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  by (induct p arbitrary: w rule: AK.induct) (auto simp: assms tautology)

section ‹Derived rules›

lemma K_A2': ‹A ⊢ K i (p ❙⟶ q) ❙⟶ K i p ❙⟶ K i q›
proof -
  have ‹A ⊢ K i p ❙∧ K i (p ❙⟶ q) ❙⟶ K i q›
    using A2 by fast
  moreover have ‹A ⊢ (P ❙∧ Q ❙⟶ R) ❙⟶ (Q ❙⟶ P ❙⟶ R)› for P Q R
    by (simp add: A1)
  ultimately show ?thesis
    using R1 by fast
qed

lemma K_map:
  assumes ‹A ⊢ p ❙⟶ q›
  shows ‹A ⊢ K i p ❙⟶ K i q›
proof -
  note ‹A ⊢ p ❙⟶ q›
  then have ‹A ⊢ K i (p ❙⟶ q)›
    using R2 by fast
  moreover have ‹A ⊢ K i (p ❙⟶ q) ❙⟶ K i p ❙⟶ K i q›
    using K_A2' by fast
  ultimately show ?thesis
    using R1 by fast
qed

lemma K_LK: ‹A ⊢ (L i (❙¬ p) ❙⟶ ❙¬ K i p)›
proof -
  have ‹A ⊢ (p ❙⟶ ❙¬ ❙¬ p)›
    by (simp add: A1)
  moreover have ‹A ⊢ ((P ❙⟶ Q) ❙⟶ (❙¬ Q ❙⟶ ❙¬ P))› for P Q
    using A1 by force
  ultimately show ?thesis
    using K_map R1 by fast
qed

lemma K_imply_head: ‹A ⊢ (p # ps ❙↝ p)›
proof -
  have ‹tautology (p # ps ❙↝ p)›
    by (induct ps) simp_all
  then show ?thesis
    using A1 by blast
qed

lemma K_imply_Cons:
  assumes ‹A ⊢ ps ❙↝ q›
  shows ‹A ⊢ p # ps ❙↝ q›
proof -
  have ‹A ⊢ (ps ❙↝ q ❙⟶ p # ps ❙↝ q)›
    by (simp add: A1)
  with R1 assms show ?thesis .
qed

lemma K_right_mp:
  assumes ‹A ⊢ ps ❙↝ p› ‹A ⊢ ps ❙↝ (p ❙⟶ q)›
  shows ‹A ⊢ ps ❙↝ q›
proof -
  have ‹tautology (ps ❙↝ p ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q)›
    by (induct ps) simp_all
  with A1 have ‹A ⊢ ps ❙↝ p ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q› .
  then show ?thesis
    using assms R1 by blast
qed

lemma tautology_imply_superset:
  assumes ‹set ps ⊆ set qs›
  shows ‹tautology (ps ❙↝ r ❙⟶ qs ❙↝ r)›
proof (rule ccontr)
  assume ‹¬ tautology (ps ❙↝ r ❙⟶ qs ❙↝ r)›
  then obtain g h where ‹¬ eval g h (ps ❙↝ r ❙⟶ qs ❙↝ r)›
    by blast
  then have ‹eval g h (ps ❙↝ r)› ‹¬ eval g h (qs ❙↝ r)›
    by simp_all
  then consider (np) ‹∃p ∈ set ps. ¬ eval g h p› | (r) ‹∀p ∈ set ps. eval g h p› ‹eval g h r›
    by (induct ps) auto
  then show False
  proof cases
    case np
    then have ‹∃p ∈ set qs. ¬ eval g h p›
      using ‹set ps ⊆ set qs› by blast
    then have ‹eval g h (qs ❙↝ r)›
      by (induct qs) simp_all
    then show ?thesis
      using ‹¬ eval g h (qs ❙↝ r)› by blast
  next
    case r
    then have ‹eval g h (qs ❙↝ r)›
      by (induct qs) simp_all
    then show ?thesis
      using ‹¬ eval g h (qs ❙↝ r)› by blast
  qed
qed

lemma K_imply_weaken:
  assumes ‹A ⊢ ps ❙↝ q› ‹set ps ⊆ set ps'›
  shows ‹A ⊢ ps' ❙↝ q›
proof -
  have ‹tautology (ps ❙↝ q ❙⟶ ps' ❙↝ q)›
    using ‹set ps ⊆ set ps'› tautology_imply_superset by blast
  then have ‹A ⊢ ps ❙↝ q ❙⟶ ps' ❙↝ q›
    using A1 by blast
  then show ?thesis
    using ‹A ⊢ ps ❙↝ q› R1 by blast
qed

lemma imply_append: ‹(ps @ ps' ❙↝ q) = (ps ❙↝ ps' ❙↝ q)›
  by (induct ps) simp_all

lemma K_ImpI:
  assumes ‹A ⊢ p # G ❙↝ q›
  shows ‹A ⊢ G ❙↝ (p ❙⟶ q)›
proof -
  have ‹set (p # G) ⊆ set (G @ [p])›
    by simp
  then have ‹A ⊢ G @ [p] ❙↝ q›
    using assms K_imply_weaken by blast
  then have ‹A ⊢ G ❙↝ [p] ❙↝ q›
    using imply_append by metis
  then show ?thesis
    by simp
qed

lemma K_Boole:
  assumes ‹A ⊢ (❙¬ p) # G ❙↝ ❙⊥›
  shows ‹A ⊢ G ❙↝ p›
proof -
  have ‹A ⊢ G ❙↝ ❙¬ ❙¬ p›
    using assms K_ImpI by blast
  moreover have ‹tautology (G ❙↝ ❙¬ ❙¬ p ❙⟶ G ❙↝ p)›
    by (induct G) simp_all
  then have ‹A ⊢ (G ❙↝ ❙¬ ❙¬ p ❙⟶ G ❙↝ p)›
    using A1 by blast
  ultimately show ?thesis
    using R1 by blast
qed

lemma K_DisE:
  assumes ‹A ⊢ p # G ❙↝ r› ‹A ⊢ q # G ❙↝ r› ‹A ⊢ G ❙↝ p ❙∨ q›
  shows ‹A ⊢ G ❙↝ r›
proof -
  have ‹tautology (p # G ❙↝ r ❙⟶ q # G ❙↝ r ❙⟶ G ❙↝ p ❙∨ q ❙⟶ G ❙↝ r)›
    by (induct G) auto
  then have ‹A ⊢ p # G ❙↝ r ❙⟶ q # G ❙↝ r ❙⟶ G ❙↝ p ❙∨ q ❙⟶ G ❙↝ r›
    using A1 by blast
  then show ?thesis
    using assms R1 by blast
qed

lemma K_mp: ‹A ⊢ p # (p ❙⟶ q) # G ❙↝ q›
  by (meson K_imply_head K_imply_weaken K_right_mp set_subset_Cons)

lemma K_swap:
  assumes ‹A ⊢ p # q # G ❙↝ r›
  shows ‹A ⊢ q # p # G ❙↝ r›
  using assms K_ImpI by (metis imply.simps(1-2))

lemma K_DisL:
  assumes ‹A ⊢ p # ps ❙↝ q› ‹A ⊢ p' # ps ❙↝ q›
  shows ‹A ⊢ (p ❙∨ p') # ps ❙↝ q›
proof -
  have ‹A ⊢ p # (p ❙∨ p') # ps ❙↝ q› ‹A ⊢ p' # (p ❙∨ p') # ps ❙↝ q›
    using assms K_swap K_imply_Cons by blast+
  moreover have ‹A ⊢ (p ❙∨ p') # ps ❙↝ p ❙∨ p'›
    using K_imply_head by blast
  ultimately show ?thesis
    using K_DisE by blast
qed

lemma K_distrib_K_imp:
  assumes ‹A ⊢ K i (G ❙↝ q)›
  shows ‹A ⊢ map (K i) G ❙↝ K i q›
proof -
  have ‹A ⊢ (K i (G ❙↝ q) ❙⟶ map (K i) G ❙↝ K i q)›
  proof (induct G)
    case Nil
    then show ?case
      by (simp add: A1)
  next
    case (Cons a G)
    have ‹A ⊢ K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ K i (G ❙↝ q)›
      by (simp add: A2)
    moreover have
      ‹A ⊢ ((K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ K i (G ❙↝ q)) ❙⟶
        (K i (G ❙↝ q) ❙⟶ map (K i) G ❙↝ K i q) ❙⟶
        (K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ map (K i) G ❙↝ K i q))›
      by (simp add: A1)
    ultimately have ‹A ⊢ K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ map (K i) G ❙↝ K i q›
      using Cons R1 by blast
    moreover have
      ‹A ⊢ ((K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ map (K i) G ❙↝ K i q) ❙⟶
        (K i (a # G ❙↝ q) ❙⟶ K i a ❙⟶ map (K i) G ❙↝ K i q))›
      by (simp add: A1)
    ultimately have ‹A ⊢ (K i (a # G ❙↝ q) ❙⟶ K i a ❙⟶ map (K i) G ❙↝ K i q)›
      using R1 by blast
    then show ?case
      by simp
  qed
  then show ?thesis
    using assms R1 by blast
qed

lemma K_trans: ‹A ⊢ (p ❙⟶ q) ❙⟶ (q ❙⟶ r) ❙⟶ p ❙⟶ r›
  by (auto intro: A1)

lemma K_L_dual: ‹A ⊢ ❙¬ L i (❙¬ p) ❙⟶ K i p›
proof -
  have ‹A ⊢ K i p ❙⟶ K i p› ‹A ⊢ ❙¬ ❙¬ p ❙⟶ p›
    by (auto intro: A1)
  then have ‹A ⊢ K i (❙¬ ❙¬ p) ❙⟶ K i p›
    by (auto intro: K_map)
  moreover have ‹A ⊢ (P ❙⟶ Q) ❙⟶ (❙¬ ❙¬ P ❙⟶ Q)› for P Q
    by (auto intro: A1)
  ultimately show ‹A ⊢ ❙¬ ❙¬ K i (❙¬ ❙¬ p) ❙⟶ K i p›
    by (auto intro: R1)
qed

section ‹Strong Soundness›

corollary soundness_imply:
  assumes ‹⋀M w p. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  shows ‹A ⊢ ps ❙↝ p ⟹ P; set ps ⊫⋆ p›
proof (induct ps arbitrary: p)
  case Nil
  then show ?case
    using soundness[of A P p] assms by simp
next
  case (Cons a ps)
  then show ?case
    using K_ImpI by fastforce
qed

theorem strong_soundness:
  assumes ‹⋀M w p. A p ⟹ P M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  shows ‹A; G ⊢ p ⟹ P; G ⊫⋆ p›
proof safe
  fix qs w and M :: ‹('a, 'b) kripke›
  assume ‹A ⊢ qs ❙↝ p›
  moreover assume ‹set qs ⊆ G› ‹∀q ∈ G. M, w ⊨ q›
  then have ‹∀q ∈ set qs. M, w ⊨ q›
    using ‹set qs ⊆ G› by blast
  moreover assume ‹P M› ‹w ∈ 𝒲 M›
  ultimately show ‹M, w ⊨ p›
    using soundness_imply[of A P qs p] assms by blast
qed

section ‹Completeness›

subsection ‹Consistent sets›

definition consistent :: ‹('i fm ⇒ bool) ⇒ 'i fm set ⇒ bool› where
  ‹consistent A S ≡ ¬ (A; S ⊢ ❙⊥)›

lemma inconsistent_subset:
  assumes ‹consistent A V› ‹¬ consistent A ({p} ∪ V)›
  obtains V' where ‹set V' ⊆ V› ‹A ⊢ p # V' ❙↝ ❙⊥›
proof -
  obtain V' where V': ‹set V' ⊆ ({p} ∪ V)› ‹p ∈ set V'› ‹A ⊢ V' ❙↝ ❙⊥›
    using assms unfolding consistent_def by blast
  then have *: ‹A ⊢ p # V' ❙↝ ❙⊥›
    using K_imply_Cons by blast

  let ?S = ‹removeAll p V'›
  have ‹set (p # V') ⊆ set (p # ?S)›
    by auto
  then have ‹A ⊢ p # ?S ❙↝ ❙⊥›
    using * K_imply_weaken by blast
  moreover have ‹set ?S ⊆ V›
    using V'(1) by (metis Diff_subset_conv set_removeAll)
  ultimately show ?thesis
    using that by blast
qed

lemma consistent_consequent:
  assumes ‹consistent A V› ‹p ∈ V› ‹A ⊢ p ❙⟶ q›
  shows ‹consistent A ({q} ∪ V)›
proof -
  have ‹∀V'. set V' ⊆ V ⟶ ¬ (A ⊢ p # V' ❙↝ ❙⊥)›
    using ‹consistent A V› ‹p ∈ V› unfolding consistent_def
    by (metis insert_subset list.simps(15))
  then have ‹∀V'. set V' ⊆ V ⟶ ¬ (A ⊢ q # V' ❙↝ ❙⊥)›
    using ‹A ⊢ (p ❙⟶ q)› K_imply_head K_right_mp by (metis imply.simps(1-2))
  then show ?thesis
    using ‹consistent A V› inconsistent_subset by metis
qed

lemma consistent_consequent':
  assumes ‹consistent A V› ‹p ∈ V› ‹tautology (p ❙⟶ q)›
  shows ‹consistent A ({q} ∪ V)›
  using assms consistent_consequent A1 by blast

lemma consistent_disjuncts:
  assumes ‹consistent A V› ‹(p ❙∨ q) ∈ V›
  shows ‹consistent A ({p} ∪ V) ∨ consistent A ({q} ∪ V)›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then have ‹¬ consistent A ({p} ∪ V)› ‹¬ consistent A ({q} ∪ V)›
    by blast+

  then obtain S' T' where
    S': ‹set S' ⊆ V› ‹A ⊢ p # S' ❙↝ ❙⊥› and
    T': ‹set T' ⊆ V› ‹A ⊢ q # T' ❙↝ ❙⊥›
    using ‹consistent A V› inconsistent_subset by metis

  from S' have p: ‹A ⊢ p # S' @ T' ❙↝ ❙⊥›
    by (metis K_imply_weaken Un_upper1 append_Cons set_append)
  moreover from T' have q: ‹A ⊢ q # S' @ T' ❙↝ ❙⊥›
    by (metis K_imply_head K_right_mp R1 imply.simps(2) imply_append)
  ultimately have ‹A ⊢ (p ❙∨ q) # S' @ T' ❙↝ ❙⊥›
    using K_DisL by blast
  then have ‹A ⊢ S' @ T' ❙↝ ❙⊥›
    using S'(1) T'(1) p q ‹consistent A V› ‹(p ❙∨ q) ∈ V› unfolding consistent_def
    by (metis Un_subset_iff insert_subset list.simps(15) set_append)
  moreover have ‹set (S' @ T') ⊆ V›
    by (simp add: S'(1) T'(1))
  ultimately show False
    using ‹consistent A V› unfolding consistent_def by blast
qed

lemma exists_finite_inconsistent:
  assumes ‹¬ consistent A ({❙¬ p} ∪ V)›
  obtains W where ‹{❙¬ p} ∪ W ⊆ {❙¬ p} ∪ V› ‹(❙¬ p) ∉ W› ‹finite W› ‹¬ consistent A ({❙¬ p} ∪ W)›
proof -
  obtain W' where W': ‹set W' ⊆ {❙¬ p} ∪ V› ‹A ⊢ W' ❙↝ ❙⊥›
    using assms unfolding consistent_def by blast
  let ?S = ‹removeAll (❙¬ p) W'›
  have ‹¬ consistent A ({❙¬ p} ∪ set ?S)›
    unfolding consistent_def using W'(2) by auto
  moreover have ‹finite (set ?S)›
    by blast
  moreover have ‹{❙¬ p} ∪ set ?S ⊆ {❙¬ p} ∪ V›
    using W'(1) by auto
  moreover have ‹(❙¬ p) ∉ set ?S›
    by simp
  ultimately show ?thesis
    by (meson that)
qed

lemma inconsistent_imply:
  assumes ‹¬ consistent A ({❙¬ p} ∪ set G)›
  shows ‹A ⊢ G ❙↝ p›
  using assms K_Boole K_imply_weaken unfolding consistent_def
  by (metis insert_is_Un list.simps(15))

subsection ‹Maximal consistent sets›

lemma fm_any_size: ‹∃p :: 'i fm. size p = n›
proof (induct n)
  case 0
  then show ?case
    using fm.size(7) by blast
next
  case (Suc n)
  then show ?case
    by (metis add.commute add_0 add_Suc_right fm.size(12))
qed

lemma infinite_UNIV_fm: ‹infinite (UNIV :: 'i fm set)›
  using fm_any_size by (metis (full_types) finite_imageI infinite_UNIV_nat surj_def)

interpretation MCS ‹consistent A› for A :: ‹'i fm ⇒ bool›
proof
  show ‹infinite (UNIV :: 'i fm set)›
    using infinite_UNIV_fm .
next
  fix S S'
  assume ‹consistent A S› ‹S' ⊆ S›
  then show ‹consistent A S'›
    unfolding consistent_def by simp
next
  fix S
  assume ‹¬ consistent A S›
  then show ‹∃S' ⊆ S. finite S' ∧ ¬ consistent A S'›
    unfolding consistent_def by blast
qed

theorem deriv_in_maximal:
  assumes ‹consistent A V› ‹maximal A V› ‹A ⊢ p›
  shows ‹p ∈ V›
  using assms R1 inconsistent_subset unfolding consistent_def maximal_def
  by (metis imply.simps(2))

theorem exactly_one_in_maximal:
  assumes ‹consistent A V› ‹maximal A V›
  shows ‹p ∈ V ⟷ (❙¬ p) ∉ V›
proof
  assume ‹p ∈ V›
  then show ‹(❙¬ p) ∉ V›
    using assms K_mp unfolding consistent_def maximal_def
    by (metis empty_subsetI insert_subset list.set(1) list.simps(15))
next
  assume ‹(❙¬ p) ∉ V›
  have ‹A ⊢ (p ❙∨ ❙¬ p)›
    by (simp add: A1)
  then have ‹(p ❙∨ ❙¬ p) ∈ V›
    using assms deriv_in_maximal by blast
  then have ‹consistent A ({p} ∪ V) ∨ consistent A ({❙¬ p} ∪ V)›
    using assms consistent_disjuncts by blast
  then show ‹p ∈ V›
    using ‹maximal A V› ‹(❙¬ p) ∉ V› unfolding maximal_def by blast
qed

theorem consequent_in_maximal:
  assumes ‹consistent A V› ‹maximal A V› ‹p ∈ V› ‹(p ❙⟶ q) ∈ V›
  shows ‹q ∈ V›
proof -
  have ‹∀V'. set V' ⊆ V ⟶ ¬ (A ⊢ p # (p ❙⟶ q) # V' ❙↝ ❙⊥)›
    using ‹consistent A V› ‹p ∈ V› ‹(p ❙⟶ q) ∈ V› unfolding consistent_def
    by (metis insert_subset list.simps(15))
  then have ‹∀V'. set V' ⊆ V ⟶ ¬ (A ⊢ q # V' ❙↝ ❙⊥)›
    by (meson K_mp K_ImpI K_imply_weaken K_right_mp set_subset_Cons)
  then have ‹consistent A ({q} ∪ V)›
    using ‹consistent A V› inconsistent_subset by metis
  then show ?thesis
    using ‹maximal A V› unfolding maximal_def by fast
qed

theorem ax_in_maximal:
  assumes ‹consistent A V› ‹maximal A V› ‹A p›
  shows ‹p ∈ V›
  using assms deriv_in_maximal Ax by blast

theorem mcs_properties:
  assumes ‹consistent A V› and ‹maximal A V›
  shows ‹A ⊢ p ⟹ p ∈ V›
    and ‹p ∈ V ⟷ (❙¬ p) ∉ V›
    and ‹p ∈ V ⟹ (p ❙⟶ q) ∈ V ⟹ q ∈ V›
  using assms deriv_in_maximal exactly_one_in_maximal consequent_in_maximal by blast+

lemma maximal_extension:
  fixes V :: ‹'i fm set›
  assumes ‹consistent A V›
  obtains W where ‹V ⊆ W› ‹consistent A W› ‹maximal A W›
proof -
  let ?W = ‹Extend A V›
  have ‹V ⊆ ?W›
    using Extend_subset by blast
  moreover have ‹consistent A ?W›
    using assms consistent_Extend by blast
  moreover have ‹maximal A ?W›
    using assms maximal_Extend by blast
  ultimately show ?thesis
    using that by blast
qed

subsection ‹Canonical model›

abbreviation pi :: ‹'i fm set ⇒ id ⇒ bool› where
  ‹pi V x ≡ Pro x ∈ V›

abbreviation known :: ‹'i fm set ⇒ 'i ⇒ 'i fm set› where
  ‹known V i ≡ {p. K i p ∈ V}›

abbreviation reach :: ‹('i fm ⇒ bool) ⇒ 'i ⇒ 'i fm set ⇒ 'i fm set set› where
  ‹reach A i V ≡ {W. known V i ⊆ W}›

abbreviation mcss :: ‹('i fm ⇒ bool) ⇒ 'i fm set set› where
  ‹mcss A ≡ {W. consistent A W ∧ maximal A W}›

abbreviation canonical :: ‹('i fm ⇒ bool) ⇒ ('i, 'i fm set) kripke› where
  ‹canonical A ≡ ⦇𝒲 = mcss A, 𝒦 = reach A, π = pi⦈›

lemma truth_lemma:
  fixes p :: ‹'i fm›
  assumes ‹consistent A V› and ‹maximal A V›
  shows ‹p ∈ V ⟷ canonical A, V ⊨ p›
  using assms
proof (induct p arbitrary: V)
  case FF
  then show ?case
  proof safe
    assume ‹❙⊥ ∈ V›
    then have False
      using ‹consistent A V› K_imply_head unfolding consistent_def
      by (metis bot.extremum insert_subset list.set(1) list.simps(15))
    then show ‹canonical A, V ⊨ ❙⊥› ..
  next
    assume ‹canonical A, V ⊨ ❙⊥›
    then show ‹❙⊥ ∈ V›
      by simp
  qed
next
  case (Pro x)
  then show ?case
    by simp
next
  case (Dis p q)
  then show ?case
  proof safe
    assume ‹(p ❙∨ q) ∈ V›
    then have ‹consistent A ({p} ∪ V) ∨ consistent A ({q} ∪ V)›
      using ‹consistent A V› consistent_disjuncts by blast
    then have ‹p ∈ V ∨ q ∈ V›
      using ‹maximal A V› unfolding maximal_def by fast
    then show ‹canonical A, V ⊨ (p ❙∨ q)›
      using Dis by simp
  next
    assume ‹canonical A, V ⊨ (p ❙∨ q)›
    then consider ‹canonical A, V ⊨ p› | ‹canonical A, V ⊨ q›
      by auto
    then have ‹p ∈ V ∨ q ∈ V›
      using Dis by auto
    moreover have ‹A ⊢ p ❙⟶ p ❙∨ q› ‹A ⊢ q ❙⟶ p ❙∨ q›
      by (auto simp: A1)
    ultimately show ‹(p ❙∨ q) ∈ V›
      using Dis.prems deriv_in_maximal consequent_in_maximal by blast
  qed
next
  case (Con p q)
  then show ?case
  proof safe
    assume ‹(p ❙∧ q) ∈ V›
    then have ‹consistent A ({p} ∪ V)› ‹consistent A ({q} ∪ V)›
      using ‹consistent A V› consistent_consequent' by fastforce+
    then have ‹p ∈ V› ‹q ∈ V›
      using ‹maximal A V› unfolding maximal_def by fast+
    then show ‹canonical A, V ⊨ (p ❙∧ q)›
      using Con by simp
  next
    assume ‹canonical A, V ⊨ (p ❙∧ q)›
    then have ‹canonical A, V ⊨ p› ‹canonical A, V ⊨ q›
      by auto
    then have ‹p ∈ V› ‹q ∈ V›
      using Con by auto
    moreover have ‹A ⊢ p ❙⟶ q ❙⟶ p ❙∧ q›
      by (auto simp: A1)
    ultimately show ‹(p ❙∧ q) ∈ V›
      using Con.prems deriv_in_maximal consequent_in_maximal by blast
  qed
next
  case (Imp p q)
  then show ?case
  proof safe
    assume ‹(p ❙⟶ q) ∈ V›
    then have ‹consistent A ({❙¬ p ❙∨ q} ∪ V)›
      using ‹consistent A V› consistent_consequent' by fastforce
    then have ‹consistent A ({❙¬ p} ∪ V) ∨ consistent A ({q} ∪ V)›
      using ‹consistent A V› ‹maximal A V› consistent_disjuncts unfolding maximal_def by blast
    then have ‹(❙¬ p) ∈ V ∨ q ∈ V›
      using ‹maximal A V› unfolding maximal_def by fast
    then have ‹p ∉ V ∨ q ∈ V›
      using Imp.prems exactly_one_in_maximal by blast
    then show ‹canonical A, V ⊨ (p ❙⟶ q)›
      using Imp by simp
  next
    assume ‹canonical A, V ⊨ (p ❙⟶ q)›
    then consider ‹¬ canonical A, V ⊨ p› | ‹canonical A, V ⊨ q›
      by auto
    then have ‹p ∉ V ∨ q ∈ V›
      using Imp by auto
    then have ‹(❙¬ p) ∈ V ∨ q ∈ V›
      using Imp.prems exactly_one_in_maximal by blast
    moreover have ‹A ⊢ ❙¬ p ❙⟶ p ❙⟶ q› ‹A ⊢ q ❙⟶ p ❙⟶ q›
      by (auto simp: A1)
    ultimately show ‹(p ❙⟶ q) ∈ V›
      using Imp.prems deriv_in_maximal consequent_in_maximal by blast
  qed
next
  case (K i p)
  then show ?case
  proof safe
    assume ‹K i p ∈ V›
    then show ‹canonical A, V ⊨ K i p›
      using K.hyps by auto
  next
    assume ‹canonical A, V ⊨ K i p›

    have ‹¬ consistent A ({❙¬ p} ∪ known V i)›
    proof
      assume ‹consistent A ({❙¬ p} ∪ known V i)›
      then obtain W where W: ‹{❙¬ p} ∪ known V i ⊆ W› ‹consistent A W› ‹maximal A W›
        using ‹consistent A V› maximal_extension by blast
      then have ‹canonical A, W ⊨ ❙¬ p›
        using K ‹consistent A V› exactly_one_in_maximal by auto
      moreover have ‹W ∈ reach A i V› ‹W ∈ mcss A›
        using W by simp_all
      ultimately have ‹canonical A, V ⊨ ❙¬ K i p›
        by auto
      then show False
        using ‹canonical A, V ⊨ K i p› by auto
    qed

    then obtain W where W:
      ‹{❙¬ p} ∪ W ⊆ {❙¬ p} ∪ known V i› ‹(❙¬ p) ∉ W› ‹finite W› ‹¬ consistent A ({❙¬ p} ∪ W)›
      using exists_finite_inconsistent by metis

    obtain L where L: ‹set L = W›
      using ‹finite W› finite_list by blast

    then have ‹A ⊢ L ❙↝ p›
      using W(4) inconsistent_imply by blast
    then have ‹A ⊢ K i (L ❙↝ p)›
      using R2 by fast
    then have ‹A ⊢ map (K i) L ❙↝ K i p›
      using K_distrib_K_imp by fast
    then have ‹(map (K i) L ❙↝ K i p) ∈ V›
      using deriv_in_maximal K.prems(1, 2) by blast
    then show ‹K i p ∈ V›
      using L W(1-2)
    proof (induct L arbitrary: W)
      case (Cons a L)
      then have ‹K i a ∈ V›
        by auto
      then have ‹(map (K i) L ❙↝ K i p) ∈ V›
        using Cons(2) ‹consistent A V› ‹maximal A V› consequent_in_maximal by auto
      then show ?case
        using Cons by auto
    qed simp
  qed
qed

lemma canonical_model:
  assumes ‹consistent A S› and ‹p ∈ S›
  defines ‹V ≡ Extend A S› and ‹M ≡ canonical A›
  shows ‹M, V ⊨ p› and ‹consistent A V› and ‹maximal A V›
proof -
  have ‹consistent A V›
    using ‹consistent A S› unfolding V_def using consistent_Extend by blast
  have ‹maximal A V›
    unfolding V_def using maximal_Extend by blast
  { fix x
    assume ‹x ∈ S›
    then have ‹x ∈ V›
      unfolding V_def using Extend_subset by blast
    then have ‹M, V ⊨ x›
      unfolding M_def using truth_lemma ‹consistent A V› ‹maximal A V› by blast }
  then show ‹M, V ⊨ p›
    using ‹p ∈ S› by blast+
  show ‹consistent A V› ‹maximal A V›
    by fact+
qed

subsection ‹Completeness›

abbreviation valid :: ‹(('i, 'i fm set) kripke ⇒ bool) ⇒ 'i fm set ⇒ 'i fm ⇒ bool›
  (‹_; _ ⊫ _› [50, 50, 50] 50)
  where ‹P; G ⊫ p ≡ P; G ⊫⋆ p›

theorem strong_completeness:
  assumes ‹P; G ⊫ p› and ‹P (canonical A)›
  shows ‹A; G ⊢ p›
proof (rule ccontr)
  assume ‹∄qs. set qs ⊆ G ∧ (A ⊢ qs ❙↝ p)›
  then have *: ‹∀qs. set qs ⊆ G ⟶ ¬ (A ⊢ (❙¬ p) # qs ❙↝ ❙⊥)›
    using K_Boole by blast

  let ?S = ‹{❙¬ p} ∪ G›
  let ?V = ‹Extend A ?S›
  let ?M = ‹canonical A›

  have ‹consistent A ?S›
    using * by (metis K_imply_Cons consistent_def inconsistent_subset)
  then have ‹?M, ?V ⊨ (❙¬ p)› ‹∀q ∈ G. ?M, ?V ⊨ q›
    using canonical_model by fastforce+
  moreover have ‹?V ∈ mcss A›
    using ‹consistent A ?S› consistent_Extend maximal_Extend by blast
  ultimately have ‹?M, ?V ⊨ p›
    using assms by simp
  then show False
    using ‹?M, ?V ⊨ (❙¬ p)› by simp
qed

corollary completeness:
  assumes ‹P; {} ⊫ p› and ‹P (canonical A)›
  shows ‹A ⊢ p›
  using assms strong_completeness[where G=‹{}›] by simp

corollary completeness⇩A:
  assumes ‹(λ_. True); {} ⊫ p›
  shows ‹A ⊢ p›
  using assms completeness by blast

section ‹System K›

abbreviation SystemK (‹_ ⊢⇩K _› [50] 50) where
  ‹G ⊢⇩K p ≡ (λ_. False); G ⊢ p›

lemma strong_soundness⇩K: ‹G ⊢⇩K p ⟹ P; G ⊫⋆ p›
  using strong_soundness[of ‹λ_. False› ‹λ_. True›] by fast

abbreviation validK (‹_ ⊫⇩K _› [50, 50] 50) where
  ‹G ⊫⇩K p ≡ (λ_. True); G ⊫ p›

lemma strong_completeness⇩K: ‹G ⊫⇩K p ⟹ G ⊢⇩K p›
  using strong_completeness[of ‹λ_. True›] by blast

theorem main⇩K: ‹G ⊫⇩K p ⟷ G ⊢⇩K p›
  using strong_soundness⇩K[of G p] strong_completeness⇩K[of G p] by fast

corollary ‹G ⊫⇩K p ⟹ (λ_. True); G ⊫⋆ p›
  using strong_soundness⇩K[of G p] strong_completeness⇩K[of G p] by fast

section ‹System T›

text ‹Also known as System M›

inductive AxT :: ‹'i fm ⇒ bool› where
  ‹AxT (K i p ❙⟶ p)›

abbreviation SystemT (‹_ ⊢⇩T _› [50, 50] 50) where
  ‹G ⊢⇩T p ≡ AxT; G ⊢ p›

lemma soundness_AxT: ‹AxT p ⟹ reflexive M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  by (induct p rule: AxT.induct) (meson truth)

lemma strong_soundness⇩T: ‹G ⊢⇩T p ⟹ reflexive; G ⊫⋆ p›
  using strong_soundness soundness_AxT .

lemma AxT_reflexive:
  assumes ‹AxT ≤ A› and ‹consistent A V› and ‹maximal A V›
  shows ‹V ∈ reach A i V›
proof -
  have ‹(K i p ❙⟶ p) ∈ V› for p
    using assms ax_in_maximal AxT.intros by fast
  then have ‹p ∈ V› if ‹K i p ∈ V› for p
    using that assms consequent_in_maximal by blast
  then show ?thesis
    using assms by blast
qed

lemma reflexive⇩T:
  assumes ‹AxT ≤ A›
  shows ‹reflexive (canonical A)›
  unfolding reflexive_def
proof safe
  fix i V
  assume ‹V ∈ 𝒲 (canonical A)›
  then have ‹consistent A V› ‹maximal A V›
    by simp_all
  with AxT_reflexive assms have ‹V ∈ reach A i V› .
  then show ‹V ∈ 𝒦 (canonical A) i V›
    by simp
qed

abbreviation validT (‹_ ⊫⇩T _› [50, 50] 50) where
  ‹G ⊫⇩T p ≡ reflexive; G ⊫ p›

lemma strong_completeness⇩T: ‹G ⊫⇩T p ⟹ G ⊢⇩T p›
  using strong_completeness reflexive⇩T by blast

theorem main⇩T: ‹G ⊫⇩T p ⟷ G ⊢⇩T p›
  using strong_soundness⇩T[of G p] strong_completeness⇩T[of G p] by fast

corollary ‹G ⊫⇩T p ⟶ reflexive; G ⊫⋆ p›
  using strong_soundness⇩T[of G p] strong_completeness⇩T[of G p] by fast

section ‹System KB›

inductive AxB :: ‹'i fm ⇒ bool› where
  ‹AxB (p ❙⟶ K i (L i p))›

abbreviation SystemKB (‹_ ⊢⇩K⇩B _› [50, 50] 50) where
  ‹G ⊢⇩K⇩B p ≡ AxB; G ⊢ p›

lemma soundness_AxB: ‹AxB p ⟹ symmetric M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  unfolding symmetric_def by (induct p rule: AxB.induct) auto

lemma strong_soundness⇩K⇩B: ‹G ⊢⇩K⇩B p ⟹ symmetric; G ⊫⋆ p›
  using strong_soundness soundness_AxB .

lemma AxB_symmetric':
  assumes ‹AxB ≤ A› ‹consistent A V› ‹maximal A V› ‹consistent A W› ‹maximal A W›
    and ‹W ∈ reach A i V›
  shows ‹V ∈ reach A i W›
proof -
  have ‹∀p. K i p ∈ W ⟶ p ∈ V›
  proof (safe, rule ccontr)
    fix p
    assume ‹K i p ∈ W› ‹p ∉ V›
    then have ‹(❙¬ p) ∈ V›
      using assms(2-3) exactly_one_in_maximal by fast
    then have ‹K i (L i (❙¬ p)) ∈ V›
      using assms(1-3) ax_in_maximal AxB.intros consequent_in_maximal by fast
    then have ‹L i (❙¬ p) ∈ W›
      using ‹W ∈ reach A i V› by fast
    then have ‹(❙¬ K i p) ∈ W›
      using assms(4-5) by (meson K_LK consistent_consequent maximal_def)
    then show False
      using ‹K i p ∈ W› assms(4-5) exactly_one_in_maximal by fast
  qed
  then have ‹known W i ⊆ V›
    by blast
  then show ?thesis
    using assms(2-3) by simp
qed

lemma symmetric⇩K⇩B:
  assumes ‹AxB ≤ A›
  shows ‹symmetric (canonical A)›
  unfolding symmetric_def
proof (intro allI ballI)
  fix i V W
  assume ‹V ∈ 𝒲 (canonical A)› ‹W ∈ 𝒲 (canonical A)›
  then have ‹consistent A V› ‹maximal A V› ‹consistent A W› ‹maximal A W›
    by simp_all
  with AxB_symmetric' assms have ‹W ∈ reach A i V ⟷ V ∈ reach A i W›
    by metis
  then show ‹(W ∈ 𝒦 (canonical A) i V) = (V ∈ 𝒦 (canonical A) i W)›
    by simp
qed

abbreviation validKB (‹_ ⊫⇩K⇩B _› [50, 50] 50) where
  ‹G ⊫⇩K⇩B p ≡ symmetric; G ⊫ p›

lemma strong_completeness⇩K⇩B: ‹G ⊫⇩K⇩B p ⟹ G ⊢⇩K⇩B p›
  using strong_completeness symmetric⇩K⇩B by blast

theorem main⇩K⇩B: ‹G ⊫⇩K⇩B p ⟷ G ⊢⇩K⇩B p›
  using strong_soundness⇩K⇩B[of G p] strong_completeness⇩K⇩B[of G p] by fast

corollary ‹G ⊫⇩K⇩B p ⟶ symmetric; G ⊫⋆ p›
  using strong_soundness⇩K⇩B[of G p] strong_completeness⇩K⇩B[of G p] by fast

section ‹System K4›

inductive Ax4 :: ‹'i fm ⇒ bool› where
  ‹Ax4 (K i p ❙⟶ K i (K i p))›

abbreviation SystemK4 (‹_ ⊢⇩K⇩4 _› [50, 50] 50) where
  ‹G ⊢⇩K⇩4 p ≡ Ax4; G ⊢ p›

lemma soundness_Ax4: ‹Ax4 p ⟹ transitive M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  by (induct p rule: Ax4.induct) (meson pos_introspection)

lemma strong_soundness⇩K⇩4: ‹G ⊢⇩K⇩4 p ⟹ transitive; G ⊫⋆ p›
  using strong_soundness soundness_Ax4 .

lemma Ax4_transitive:
  assumes ‹Ax4 ≤ A› ‹consistent A V› ‹maximal A V›
    and ‹W ∈ reach A i V› ‹U ∈ reach A i W›
  shows ‹U ∈ reach A i V›
proof -
  have ‹(K i p ❙⟶ K i (K i p)) ∈ V› for p
    using assms(1-3) ax_in_maximal Ax4.intros by fast
  then have ‹K i (K i p) ∈ V› if ‹K i p ∈ V› for p
    using that assms(2-3) consequent_in_maximal by blast
  then show ?thesis
    using assms(4-5) by blast
qed

lemma transitive⇩K⇩4:
  assumes ‹Ax4 ≤ A›
  shows ‹transitive (canonical A)›
  unfolding transitive_def
proof safe
  fix i U V W
  assume ‹V ∈ 𝒲 (canonical A)›
  then have ‹consistent A V› ‹maximal A V›
    by simp_all
  moreover assume
    ‹W ∈ 𝒦 (canonical A) i V›
    ‹U ∈ 𝒦 (canonical A) i W›
  ultimately have ‹U ∈ reach A i V›
    using Ax4_transitive assms by simp
  then show ‹U ∈ 𝒦 (canonical A) i V›
    by simp
qed

abbreviation validK4 (‹_ ⊫⇩K⇩4 _› [50, 50] 50) where
  ‹G ⊫⇩K⇩4 p ≡ transitive; G ⊫ p›

lemma strong_completeness⇩K⇩4: ‹G ⊫⇩K⇩4 p ⟹ G ⊢⇩K⇩4 p›
  using strong_completeness transitive⇩K⇩4 by blast

theorem main⇩K⇩4: ‹G ⊫⇩K⇩4 p ⟷ G ⊢⇩K⇩4 p›
  using strong_soundness⇩K⇩4[of G p] strong_completeness⇩K⇩4[of G p] by fast

corollary ‹G ⊫⇩K⇩4 p ⟶ transitive; G ⊫⋆ p›
  using strong_soundness⇩K⇩4[of G p] strong_completeness⇩K⇩4[of G p] by fast

section ‹System K5›

inductive Ax5 :: ‹'i fm ⇒ bool› where
  ‹Ax5 (L i p ❙⟶ K i (L i p))›

abbreviation SystemK5 (‹_ ⊢⇩K⇩5 _› [50, 50] 50) where
  ‹G ⊢⇩K⇩5 p ≡ Ax5; G ⊢ p›

lemma soundness_Ax5: ‹Ax5 p ⟹ Euclidean M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  by (induct p rule: Ax5.induct) (unfold Euclidean_def semantics.simps, blast)

lemma strong_soundness⇩K⇩5: ‹G ⊢⇩K⇩5 p ⟹ Euclidean; G ⊫⋆ p›
  using strong_soundness soundness_Ax5 .

lemma Ax5_Euclidean:
  assumes ‹Ax5 ≤ A›
    ‹consistent A U› ‹maximal A U›
    ‹consistent A V› ‹maximal A V›
    ‹consistent A W› ‹maximal A W›
    and ‹V ∈ reach A i U› ‹W ∈ reach A i U›
  shows ‹W ∈ reach A i V›
  using assms
proof -
  { fix p
    assume ‹K i p ∈ V› ‹p ∉ W›
    then have ‹(❙¬ p) ∈ W›
      using assms(6-7) exactly_one_in_maximal by fast
    then have ‹L i (❙¬ p) ∈ U›
      using assms(2-3, 6-7, 9) exactly_one_in_maximal by blast
    then have ‹K i (L i (❙¬ p)) ∈ U›
      using assms(1-3) ax_in_maximal Ax5.intros consequent_in_maximal by fast
    then have ‹L i (❙¬ p) ∈ V›
      using assms(8) by blast
    then have ‹❙¬ K i p ∈ V›
      using assms(4-5) K_LK consequent_in_maximal deriv_in_maximal by fast
    then have False
      using assms(4-5) ‹K i p ∈ V› exactly_one_in_maximal by fast
  }
  then show ?thesis
    by blast
qed

lemma Euclidean⇩K⇩5:
  assumes ‹Ax5 ≤ A›
  shows ‹Euclidean (canonical A)›
  unfolding Euclidean_def
proof safe
  fix i U V W
  assume ‹U ∈ 𝒲 (canonical A)› ‹V ∈ 𝒲 (canonical A)› ‹W ∈ 𝒲 (canonical A)›
  then have
    ‹consistent A U› ‹maximal A U›
    ‹consistent A V› ‹maximal A V›
    ‹consistent A W› ‹maximal A W›
    by simp_all
  moreover assume
    ‹V ∈ 𝒦 (canonical A) i U›
    ‹W ∈ 𝒦 (canonical A) i U›
  ultimately have ‹W ∈ reach A i V›
    using Ax5_Euclidean assms by simp
  then show ‹W ∈ 𝒦 (canonical A) i V›
    by simp
qed

abbreviation validK5 (‹_ ⊫⇩K⇩5 _› [50, 50] 50) where
  ‹G ⊫⇩K⇩5 p ≡ Euclidean; G ⊫ p›

lemma strong_completeness⇩K⇩5: ‹G ⊫⇩K⇩5 p ⟹ G ⊢⇩K⇩5 p›
  using strong_completeness Euclidean⇩K⇩5 by blast

theorem main⇩K⇩5: ‹G ⊫⇩K⇩5 p ⟷ G ⊢⇩K⇩5 p›
  using strong_soundness⇩K⇩5[of G p] strong_completeness⇩K⇩5[of G p] by fast

corollary ‹G ⊫⇩K⇩5 p ⟶ Euclidean; G ⊫⋆ p›
  using strong_soundness⇩K⇩5[of G p] strong_completeness⇩K⇩5[of G p] by fast

section ‹System S4›

abbreviation Or :: ‹('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool› (infixl ‹⊕› 65) where
  ‹(A ⊕ A') p ≡ A p ∨ A' p›

abbreviation SystemS4 (‹_ ⊢⇩S⇩4 _› [50, 50] 50) where
  ‹G ⊢⇩S⇩4 p ≡ AxT ⊕ Ax4; G ⊢ p›

lemma soundness_AxT4: ‹(AxT ⊕ Ax4) p ⟹ reflexive M ∧ transitive M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  using soundness_AxT soundness_Ax4 by fast

lemma strong_soundness⇩S⇩4: ‹G ⊢⇩S⇩4 p ⟹ refltrans; G ⊫⋆ p›
  using strong_soundness soundness_AxT4 .

abbreviation validS4 (‹_ ⊫⇩S⇩4 _› [50, 50] 50) where
  ‹G ⊫⇩S⇩4 p ≡ refltrans; G ⊫ p›

lemma strong_completeness⇩S⇩4: ‹G ⊫⇩S⇩4 p ⟹ G ⊢⇩S⇩4 p›
  using strong_completeness[of refltrans] reflexive⇩T[of ‹AxT ⊕ Ax4›] transitive⇩K⇩4[of ‹AxT ⊕ Ax4›]
  by blast

theorem main⇩S⇩4: ‹G ⊫⇩S⇩4 p ⟷ G ⊢⇩S⇩4 p›
  using strong_soundness⇩S⇩4[of G p] strong_completeness⇩S⇩4[of G p] by fast

corollary ‹G ⊫⇩S⇩4 p ⟶ refltrans; G ⊫⋆ p›
  using strong_soundness⇩S⇩4[of G p] strong_completeness⇩S⇩4[of G p] by fast

section ‹System S5›

subsection ‹T + B + 4›

abbreviation SystemS5 (‹_ ⊢⇩S⇩5 _› [50, 50] 50) where
  ‹G ⊢⇩S⇩5 p ≡ AxT ⊕ AxB ⊕ Ax4; G ⊢ p›

abbreviation AxTB4 :: ‹'i fm ⇒ bool› where
  ‹AxTB4 ≡ AxT ⊕ AxB ⊕ Ax4›

lemma soundness_AxTB4: ‹AxTB4 p ⟹ equivalence M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  using soundness_AxT soundness_AxB soundness_Ax4 by fast

lemma strong_soundness⇩S⇩5: ‹G ⊢⇩S⇩5 p ⟹ equivalence; G ⊫⋆ p›
  using strong_soundness soundness_AxTB4 .

abbreviation validS5 (‹_ ⊫⇩S⇩5 _› [50, 50] 50) where
  ‹G ⊫⇩S⇩5 p ≡ equivalence; G ⊫ p›

lemma strong_completeness⇩S⇩5: ‹G ⊫⇩S⇩5 p ⟹ G ⊢⇩S⇩5 p›
  using strong_completeness[of equivalence]
    reflexive⇩T[of AxTB4] symmetric⇩K⇩B[of AxTB4] transitive⇩K⇩4[of AxTB4]
  by blast

theorem main⇩S⇩5: ‹G ⊫⇩S⇩5 p ⟷ G ⊢⇩S⇩5 p›
  using strong_soundness⇩S⇩5[of G p] strong_completeness⇩S⇩5[of G p] by fast

corollary ‹G ⊫⇩S⇩5 p ⟶ equivalence; G ⊫⋆ p›
  using strong_soundness⇩S⇩5[of G p] strong_completeness⇩S⇩5[of G p] by fast

subsection ‹T + 5›

abbreviation SystemS5' (‹_ ⊢⇩S⇩5'' _› [50, 50] 50) where
  ‹G ⊢⇩S⇩5' p ≡ AxT ⊕ Ax5; G ⊢ p›

abbreviation AxT5 :: ‹'i fm ⇒ bool› where
  ‹AxT5 ≡ AxT ⊕ Ax5›

lemma symm_trans_Euclid: ‹symmetric M ⟹ transitive M ⟹ Euclidean M›
  unfolding symmetric_def transitive_def Euclidean_def by blast

lemma soundness_AxT5: ‹AxT5 p ⟹ equivalence M ⟹ w ∈ 𝒲 M ⟹ M, w ⊨ p›
  using soundness_AxT[of p M w] soundness_Ax5[of p M w] symm_trans_Euclid by blast

lemma strong_soundness⇩S⇩5': ‹G ⊢⇩S⇩5' p ⟹ equivalence; G ⊫⋆ p›
  using strong_soundness soundness_AxT5 .

lemma refl_Euclid_equiv: ‹reflexive M ⟹ Euclidean M ⟹ equivalence M›
  unfolding reflexive_def symmetric_def transitive_def Euclidean_def by metis

lemma strong_completeness⇩S⇩5': ‹G ⊫⇩S⇩5 p ⟹ G ⊢⇩S⇩5' p›
  using strong_completeness[of equivalence]
    reflexive⇩T[of AxT5] Euclidean⇩K⇩5[of AxT5] refl_Euclid_equiv by blast

theorem main⇩S⇩5': ‹G ⊫⇩S⇩5 p ⟷ G ⊢⇩S⇩5' p›
  using strong_soundness⇩S⇩5'[of G p] strong_completeness⇩S⇩5'[of G p] by fast

subsection ‹Equivalence between systems›

subsubsection ‹Axiom 5 from B and 4›

lemma K4_L:
  assumes ‹Ax4 ≤ A›
  shows ‹A ⊢ L i (L i p) ❙⟶ L i p›
proof -
  have ‹A ⊢ K i (❙¬ p) ❙⟶ K i (K i (❙¬ p))›
    using assms by (auto intro: Ax Ax4.intros)
  then show ?thesis
    by (meson K_LK K_trans R1)
qed

lemma KB4_5:
  assumes ‹AxB ≤ A› ‹Ax4 ≤ A›
  shows ‹A ⊢ L i p ❙⟶ K i (L i p)›
proof -
  have ‹A ⊢ L i p ❙⟶ K i (L i (L i p))›
    using assms by (auto intro: Ax AxB.intros)
  moreover have ‹A ⊢ L i (L i p) ❙⟶ L i p›
    using assms by (auto intro: K4_L)
  then have ‹A ⊢ K i (L i (L i p)) ❙⟶ K i (L i p)›
    using K_map by fast
  ultimately show ?thesis
    using K_trans R1 by metis
qed

subsubsection ‹Axioms B and 4 from T and 5›

lemma T_L:
  assumes ‹AxT ≤ A›
  shows ‹A ⊢ p ❙⟶ L i p›
proof -
  have ‹A ⊢ K i (❙¬ p) ❙⟶ ❙¬ p›
    using assms by (auto intro: Ax AxT.intros)
  moreover have ‹A ⊢ (P ❙⟶ ❙¬ Q) ❙⟶ Q ❙⟶ ❙¬ P› for P Q
    by (auto intro: A1)
  ultimately show ?thesis
    by (auto intro: R1)
qed

lemma S5'_B:
  assumes ‹AxT ≤ A› ‹Ax5 ≤ A›
  shows ‹A ⊢ p ❙⟶ K i (L i p)›
proof -
  have ‹A ⊢ L i p ❙⟶ K i (L i p)›
    using assms(2) by (auto intro: Ax Ax5.intros)
  moreover have ‹A ⊢ p ❙⟶ L i p›
    using assms(1) by (auto intro: T_L)
  ultimately show ?thesis
    using K_trans R1 by metis
qed

lemma K5_L:
  assumes ‹Ax5 ≤ A›
  shows ‹A ⊢ L i (K i p) ❙⟶ K i p›
proof -
  have ‹A ⊢ L i (❙¬ p) ❙⟶ K i (L i (❙¬ p))›
    using assms by (auto intro: Ax Ax5.intros)
  then have ‹A ⊢ L i (❙¬ p) ❙⟶ K i (❙¬ K i p)›
    using K_LK by (metis K_map K_trans R1)
  moreover have ‹A ⊢ (P ❙⟶ Q) ❙⟶ ❙¬ Q ❙⟶ ❙¬ P› for P Q
    by (auto intro: A1)
  ultimately have ‹A ⊢ ❙¬ K i (❙¬ K i p) ❙⟶ ❙¬ L i (❙¬ p)›
    using R1 by blast
  then have ‹A ⊢ ❙¬ K i (❙¬ K i p) ❙⟶ K i p›
    using K_L_dual R1 K_trans by metis
  then show ?thesis
    by blast
qed

lemma S5'_4:
  assumes ‹AxT ≤ A› ‹Ax5 ≤ A›
  shows ‹A ⊢ K i p ❙⟶ K i (K i p)›
proof -
  have ‹A ⊢ L i (K i p) ❙⟶ K i (L i (K i p))›
    using assms(2) by (auto intro: Ax Ax5.intros)
  moreover have ‹A ⊢ K i p ❙⟶ L i (K i p)›
    using assms(1) by (auto intro: T_L)
  ultimately have ‹A ⊢ K i p ❙⟶ K i (L i (K i p))›
    using K_trans R1 by metis
  moreover have ‹A ⊢ L i (K i p) ❙⟶ K i p›
    using assms(2) K5_L by metis
  then have ‹A ⊢ K i (L i (K i p)) ❙⟶ K i (K i p)›
    using K_map by fast
  ultimately show ?thesis
    using R1 K_trans by metis
qed

lemma S5_S5': ‹AxTB4 ⊢ p ⟹ AxT5 ⊢ p›
proof (induct p rule: AK.induct)
  case (Ax p)
  moreover have ‹AxT5 ⊢ p› if ‹AxT p›
    using that AK.Ax by metis
  moreover have ‹AxT5 ⊢ p› if ‹AxB p›
    using that S5'_B by (metis (no_types, lifting) AxB.cases predicate1I)
  moreover have ‹AxT5 ⊢ p› if ‹Ax4 p›
    using that S5'_4 by (metis (no_types, lifting) Ax4.cases predicate1I)
  ultimately show ?case
    by blast
qed (auto intro: AK.intros)

lemma S5'_S5: ‹AxT5 ⊢ p ⟹ AxTB4 ⊢ p›
proof (induct p rule: AK.induct)
  case (Ax p)
  moreover have ‹AxTB4 ⊢ p› if ‹AxT p›
    using that AK.Ax by metis
  moreover have ‹AxTB4 ⊢ p› if ‹Ax5 p›
    using that KB4_5 by (metis (no_types, lifting) Ax5.cases predicate1I)
  ultimately show ?case
    by blast
qed (auto intro: AK.intros)

corollary S5_S5'_assms: ‹G ⊢⇩S⇩5 p ⟷ G ⊢⇩S⇩5' p›
  using S5_S5' S5'_S5 by blast

section ‹Acknowledgements›

text ‹
The formalization is inspired by Berghofer's formalization of Henkin-style completeness.

  ▪ Stefan Berghofer:
  First-Order Logic According to Fitting.
  🌐‹https://www.isa-afp.org/entries/FOL-Fitting.shtml›
›

end