Modal Logic

@cite{rotter-liu-2025}

Kripke semantics for normal modal logics. Formalizes frames, frame conditions, correspondence theorems, and the lattice of normal modal logics.

Modal typological types (ModalForce, ModalFlavor, ForceFlavor, etc.) live in Core.Modality (Core/Modality/ModalTypes.lean). Linguistic interpretations belong in Theories/Semantics/Modality/.

Frames and Accessibility

@[reducible, inline]

abbrev Core.ModalLogic.AccessRel (W : Type u_1) : Type u_1

Equations

• Core.ModalLogic.AccessRel W = (W → W → Bool)

@[reducible, inline]

abbrev Core.ModalLogic.AgentAccessRel (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Agent-indexed accessibility relation: each agent has their own AccessRel.

Equations

• Core.ModalLogic.AgentAccessRel W E = (E → Core.ModalLogic.AccessRel W)

def Core.ModalLogic.kripkeEval {W : Type u_1} [Proposition.FiniteWorlds W] (R : AccessRel W) (force : Modality.ModalForce) (p : BProp W) (w : W) : Bool

Kripke evaluation of modal formulas.

Equations

• Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.necessity p w = (List.filter (R w) Core.Proposition.FiniteWorlds.worlds).all p
• Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.weakNecessity p w = (List.filter (R w) Core.Proposition.FiniteWorlds.worlds).all p
• Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.possibility p w = (List.filter (R w) Core.Proposition.FiniteWorlds.worlds).any p

theorem Core.ModalLogic.duality {W : Type u_1} [Proposition.FiniteWorlds W] (R : AccessRel W) (p : BProp W) (w : W) : kripkeEval R Modality.ModalForce.necessity p w = !kripkeEval R Modality.ModalForce.possibility (fun (v : W) => !p v) w

Frame Conditions

def Core.ModalLogic.Refl {W : Type u_1} (R : AccessRel W) : Prop

Equations

• Core.ModalLogic.Refl R = ∀ (w : W), R w w = true

def Core.ModalLogic.Serial {W : Type u_1} (R : AccessRel W) : Prop

Equations

• Core.ModalLogic.Serial R = ∀ (w : W), ∃ (v : W), R w v = true

def Core.ModalLogic.Trans {W : Type u_1} (R : AccessRel W) : Prop

Equations

• Core.ModalLogic.Trans R = ∀ (w v u : W), R w v = true → R v u = true → R w u = true

def Core.ModalLogic.Symm {W : Type u_1} (R : AccessRel W) : Prop

Equations

• Core.ModalLogic.Symm R = ∀ (w v : W), R w v = true → R v w = true

def Core.ModalLogic.Eucl {W : Type u_1} (R : AccessRel W) : Prop

Equations

• Core.ModalLogic.Eucl R = ∀ (w v u : W), R w v = true → R w u = true → R v u = true

theorem Core.ModalLogic.refl_serial {W : Type u_1} {R : AccessRel W} (h : Refl R) : Serial R

theorem Core.ModalLogic.refl_eucl_symm {W : Type u_1} {R : AccessRel W} (hR : Refl R) (hE : Eucl R) : Symm R

theorem Core.ModalLogic.refl_eucl_trans {W : Type u_1} {R : AccessRel W} (hR : Refl R) (hE : Eucl R) : Trans R

theorem Core.ModalLogic.symm_trans_eucl {W : Type u_1} {R : AccessRel W} (hS : Symm R) (hT : Trans R) : Eucl R

Frame Correspondence

theorem Core.ModalLogic.T_of_refl {W : Type u_1} [Proposition.FiniteWorlds W] {R : AccessRel W} (hR : Refl R) (p : BProp W) (w : W) (h : kripkeEval R Modality.ModalForce.necessity p w = true) : p w = true

T axiom: □p → p

theorem Core.ModalLogic.D_of_serial {W : Type u_1} [Proposition.FiniteWorlds W] {R : AccessRel W} (hS : Serial R) (p : BProp W) (w : W) (h : kripkeEval R Modality.ModalForce.necessity p w = true) : kripkeEval R Modality.ModalForce.possibility p w = true

D axiom: □p → ◇p

theorem Core.ModalLogic.K_axiom {W : Type u_1} [Proposition.FiniteWorlds W] (R : AccessRel W) (p q : BProp W) (w : W) (hImp : kripkeEval R Modality.ModalForce.necessity (fun (v : W) => !p v || q v) w = true) (hP : kripkeEval R Modality.ModalForce.necessity p w = true) : kripkeEval R Modality.ModalForce.necessity q w = true

K axiom: □(p → q) → □p → □q

theorem Core.ModalLogic.four_of_trans {W : Type u_1} [Proposition.FiniteWorlds W] {R : AccessRel W} (hT : Trans R) (p : BProp W) (w : W) (h : kripkeEval R Modality.ModalForce.necessity p w = true) : kripkeEval R Modality.ModalForce.necessity (kripkeEval R Modality.ModalForce.necessity p) w = true

4 axiom: □p → □□p

theorem Core.ModalLogic.B_of_symm {W : Type u_1} [Proposition.FiniteWorlds W] {R : AccessRel W} (hS : Symm R) (p : BProp W) (w : W) (hP : p w = true) : kripkeEval R Modality.ModalForce.necessity (kripkeEval R Modality.ModalForce.possibility p) w = true

B axiom: p → □◇p

theorem Core.ModalLogic.five_of_eucl {W : Type u_1} [Proposition.FiniteWorlds W] {R : AccessRel W} (hE : Eucl R) (p : BProp W) (w : W) (h : kripkeEval R Modality.ModalForce.possibility p w = true) : kripkeEval R Modality.ModalForce.necessity (kripkeEval R Modality.ModalForce.possibility p) w = true

5 axiom: ◇p → □◇p

Lattice of Normal Modal Logics

inductive Core.ModalLogic.Axiom : Type

Axiom schemas addable to K.

• M : Axiom
• D : Axiom
• B : Axiom
• four : Axiom
• five : Axiom

instance Core.ModalLogic.instDecidableEqAxiom : DecidableEq Axiom

Equations

• Core.ModalLogic.instDecidableEqAxiom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.ModalLogic.instBEqAxiom : BEq Axiom

Equations

• Core.ModalLogic.instBEqAxiom = { beq := Core.ModalLogic.instBEqAxiom.beq }

def Core.ModalLogic.instBEqAxiom.beq : Axiom → Axiom → Bool

Equations

• Core.ModalLogic.instBEqAxiom.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.ModalLogic.instReprAxiom.repr : Axiom → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.ModalLogic.instReprAxiom.repr Core.ModalLogic.Axiom.M prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.ModalLogic.Axiom.M")).group prec✝
• Core.ModalLogic.instReprAxiom.repr Core.ModalLogic.Axiom.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.ModalLogic.Axiom.D")).group prec✝
• Core.ModalLogic.instReprAxiom.repr Core.ModalLogic.Axiom.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.ModalLogic.Axiom.B")).group prec✝

instance Core.ModalLogic.instReprAxiom : Repr Axiom

Equations

• Core.ModalLogic.instReprAxiom = { reprPrec := Core.ModalLogic.instReprAxiom.repr }

instance Core.ModalLogic.instInhabitedAxiom : Inhabited Axiom

Equations

• Core.ModalLogic.instInhabitedAxiom = { default := Core.ModalLogic.instInhabitedAxiom.default }

def Core.ModalLogic.instInhabitedAxiom.default : Axiom

Equations

• Core.ModalLogic.instInhabitedAxiom.default = Core.ModalLogic.Axiom.M

instance Core.ModalLogic.instHashableAxiom : Hashable Axiom

Equations

• Core.ModalLogic.instHashableAxiom = { hash := Core.ModalLogic.instHashableAxiom.hash }

def Core.ModalLogic.instHashableAxiom.hash : Axiom → UInt64

Equations

• Core.ModalLogic.instHashableAxiom.hash Core.ModalLogic.Axiom.M = 0
• Core.ModalLogic.instHashableAxiom.hash Core.ModalLogic.Axiom.D = 1
• Core.ModalLogic.instHashableAxiom.hash Core.ModalLogic.Axiom.B = 2
• Core.ModalLogic.instHashableAxiom.hash Core.ModalLogic.Axiom.four = 3
• Core.ModalLogic.instHashableAxiom.hash Core.ModalLogic.Axiom.five = 4

instance Core.ModalLogic.instToStringAxiom : ToString Axiom

Equations

• One or more equations did not get rendered due to their size.

structure Core.ModalLogic.Logic : Type

A normal modal logic is K plus axiom schemas.

• axioms : Finset Axiom

def Core.ModalLogic.instDecidableEqLogic.decEq (x✝ x✝¹ : Logic) : Decidable (x✝ = x✝¹)

Equations

• Core.ModalLogic.instDecidableEqLogic.decEq { axioms := a } { axioms := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Core.ModalLogic.instDecidableEqLogic : DecidableEq Logic

Equations

• Core.ModalLogic.instDecidableEqLogic = Core.ModalLogic.instDecidableEqLogic.decEq

def Core.ModalLogic.Logic.K : Logic

Equations

• Core.ModalLogic.Logic.K = { axioms := ∅ }

def Core.ModalLogic.Logic.T : Logic

Equations

• Core.ModalLogic.Logic.T = { axioms := {Core.ModalLogic.Axiom.M} }

def Core.ModalLogic.Logic.D : Logic

Equations

• Core.ModalLogic.Logic.D = { axioms := {Core.ModalLogic.Axiom.D} }

def Core.ModalLogic.Logic.KB : Logic

Equations

• Core.ModalLogic.Logic.KB = { axioms := {Core.ModalLogic.Axiom.B} }

def Core.ModalLogic.Logic.K4 : Logic

Equations

• Core.ModalLogic.Logic.K4 = { axioms := {Core.ModalLogic.Axiom.four} }

def Core.ModalLogic.Logic.K5 : Logic

Equations

• Core.ModalLogic.Logic.K5 = { axioms := {Core.ModalLogic.Axiom.five} }

def Core.ModalLogic.Logic.S4 : Logic

Equations

• Core.ModalLogic.Logic.S4 = { axioms := {Core.ModalLogic.Axiom.M, Core.ModalLogic.Axiom.four} }

def Core.ModalLogic.Logic.S5 : Logic

Equations

• Core.ModalLogic.Logic.S5 = { axioms := {Core.ModalLogic.Axiom.M, Core.ModalLogic.Axiom.five} }

def Core.ModalLogic.Logic.KTB : Logic

Equations

• Core.ModalLogic.Logic.KTB = { axioms := {Core.ModalLogic.Axiom.M, Core.ModalLogic.Axiom.B} }

def Core.ModalLogic.Logic.KD45 : Logic

Equations

• Core.ModalLogic.Logic.KD45 = { axioms := {Core.ModalLogic.Axiom.D, Core.ModalLogic.Axiom.four, Core.ModalLogic.Axiom.five} }

def Core.ModalLogic.Logic.K45 : Logic

Equations

• Core.ModalLogic.Logic.K45 = { axioms := {Core.ModalLogic.Axiom.four, Core.ModalLogic.Axiom.five} }

instance Core.ModalLogic.Logic.instLE : LE Logic

L₁ ≤ L₂ means L₁ is weaker (fewer axioms).

Equations

• Core.ModalLogic.Logic.instLE = { le := fun (L₁ L₂ : Core.ModalLogic.Logic) => L₁.axioms ⊆ L₂.axioms }

instance Core.ModalLogic.Logic.instPartialOrder : PartialOrder Logic

Equations

• One or more equations did not get rendered due to their size.

instance Core.ModalLogic.Logic.instLattice : Lattice Logic

Equations

• One or more equations did not get rendered due to their size.

def Core.ModalLogic.Logic.top : Logic

Equations

• Core.ModalLogic.Logic.top = { axioms := {Core.ModalLogic.Axiom.M, Core.ModalLogic.Axiom.D, Core.ModalLogic.Axiom.B, Core.ModalLogic.Axiom.four, Core.ModalLogic.Axiom.five} }

instance Core.ModalLogic.Logic.instOrderBot : OrderBot Logic

Equations

• Core.ModalLogic.Logic.instOrderBot = { bot := Core.ModalLogic.Logic.K, bot_le := Core.ModalLogic.Logic.instOrderBot._proof_1 }

instance Core.ModalLogic.Logic.instOrderTop : OrderTop Logic

Equations

• Core.ModalLogic.Logic.instOrderTop = { top := Core.ModalLogic.Logic.top, le_top := Core.ModalLogic.Logic.instOrderTop._proof_1 }

instance Core.ModalLogic.Logic.instBoundedOrder : BoundedOrder Logic

Equations

• Core.ModalLogic.Logic.instBoundedOrder = { toOrderTop := Core.ModalLogic.Logic.instOrderTop, toOrderBot := Core.ModalLogic.Logic.instOrderBot }

theorem Core.ModalLogic.Logic.K_bot : K = ⊥

theorem Core.ModalLogic.Logic.top_all_axioms : top = ⊤

def Core.ModalLogic.Logic.hasAxiom (L : Logic) (a : Axiom) : Bool

Equations

• L.hasAxiom a = decide (a ∈ L.axioms)

def Core.ModalLogic.Logic.frameConditions {W : Type u_1} (L : Logic) (R : AccessRel W) : Prop

Frame conditions required by a logic.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.ModalLogic.S5_equiv {W : Type u_1} {R : AccessRel W} (hR : Refl R) (hE : Eucl R) : Refl R ∧ Symm R ∧ Trans R

S5 frames are equivalence relations.

theorem Core.ModalLogic.S4_preorder {W : Type u_1} {R : AccessRel W} (hR : Refl R) (hT : Trans R) : Refl R ∧ Trans R

S4 frames are preorders.

theorem Core.ModalLogic.M_implies_D {W : Type u_1} {R : AccessRel W} (hM : Refl R) : Serial R

M + 5 implies D (M implies serial).

theorem Core.ModalLogic.M5_implies_B {W : Type u_1} {R : AccessRel W} (hM : Refl R) (h5 : Eucl R) : Symm R

M + 5 implies B.

theorem Core.ModalLogic.M5_implies_4 {W : Type u_1} {R : AccessRel W} (hM : Refl R) (h5 : Eucl R) : Trans R

M + 5 implies 4.

theorem Core.ModalLogic.S5_collapse {W : Type u_1} {R : AccessRel W} (hM : Refl R) (h5 : Eucl R) : Refl R ∧ Serial R ∧ Symm R ∧ Trans R ∧ Eucl R

S5 = M5 = MB5 = M4B5 = M45 = M4B (all collapse to same frame class). Any frame satisfying M and 5 automatically satisfies B and 4.

Standard Frames

def Core.ModalLogic.universalR {W : Type u_1} : AccessRel W

Equations

• Core.ModalLogic.universalR x✝¹ x✝ = true

def Core.ModalLogic.emptyR {W : Type u_1} : AccessRel W

Equations

• Core.ModalLogic.emptyR x✝¹ x✝ = false

def Core.ModalLogic.identityR {W : Type u_1} [DecidableEq W] : AccessRel W

Equations

• Core.ModalLogic.identityR w v = (w == v)

@[simp]

theorem Core.ModalLogic.universalR_refl {W : Type u_1} : Refl universalR

@[simp]

theorem Core.ModalLogic.universalR_symm {W : Type u_1} : Symm universalR

@[simp]

theorem Core.ModalLogic.universalR_trans {W : Type u_1} : Trans universalR

@[simp]

theorem Core.ModalLogic.universalR_eucl {W : Type u_1} : Eucl universalR

@[simp]

theorem Core.ModalLogic.universalR_serial {W : Type u_1} : Serial universalR

theorem Core.ModalLogic.universalR_S5 {W : Type u_1} : Refl universalR ∧ Symm universalR ∧ Trans universalR

theorem Core.ModalLogic.identityR_refl {W : Type u_1} [DecidableEq W] : Refl identityR