# 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
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)›
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)›
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'›
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
next
case (Cons a G)
have ‹A ⊢ K i a ❙∧ K i (a # G ❙↝ q) ❙⟶ K i (G ❙↝ q)›
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))›
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))›
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›
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
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)›
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
```