Polymorphic Kripke Foundation

[Kri63]

The bare foundation for accessibility-restricted modal logic, parameterised by {W : Type*} — no Frame, no Entity, no type system: accessibility relations, frame conditions, and the relational box/diamond. The modal-axiom theorems (RestrictedModality.lean) build on it.

Montague's S5 box/diamond in Intensional.Quantification is the universal-accessibility special case (box universalR), but it lives in the typed IL layer and is developed independently there.

Defs.lean is the foundation file in mathlib's sense: just the data and the relationships among frame conditions. Modal axiom correspondence (K/T/D/4/B/5), monotonicity, distribution, restriction, the Logic lattice, and the PropOp ("Gallin") hierarchy live in RestrictedModality.lean.

@[reducible, inline]

abbrev Core.Logic.Modal.AccessRel (W : Type u_1) : Type u_1

An accessibility relation on worlds. R w v means world v is accessible from world w.

Equations

• Core.Logic.Modal.AccessRel W = (W → W → Prop)

@[reducible, inline]

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

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

Equations

• Core.Logic.Modal.AgentAccessRel W E = (E → Core.Logic.Modal.AccessRel W)

def Core.Logic.Modal.universalR {W : Type u_1} : AccessRel W

Universal accessibility: every world is accessible from every world.

Equations

• Core.Logic.Modal.universalR x✝¹ x✝ = True

def Core.Logic.Modal.emptyR {W : Type u_1} : AccessRel W

Empty accessibility: no world is accessible from any world.

Equations

• Core.Logic.Modal.emptyR x✝¹ x✝ = False

def Core.Logic.Modal.identityR {W : Type u_1} : AccessRel W

Reflexive (identity) accessibility: each world accesses only itself.

Equations

• Core.Logic.Modal.identityR w v = (w = v)

Reflexivity, symmetry, and transitivity are Std.Refl R, Std.Symm R, IsTrans W R from Lean core + mathlib. Seriality and Euclideanness are modal-logic-specific and defined here.

class Core.Logic.Modal.IsSerial {W : Type u_1} (R : AccessRel W) : Prop

Seriality: every world accesses at least one world.

Identical as a Prop to Mathlib.Logic.Relator.LeftTotal R, but packaged as a class with the modal-logic-canonical name.

• serial (w : W) : ∃ (v : W), R w v

class Core.Logic.Modal.IsEuclidean {W : Type u_1} (R : AccessRel W) : Prop

Euclideanness: from any pair of R-successors of w, each is an R-successor of the other. No mathlib analogue (modal-specific).

• eucl (w v u : W) : R w v → R w u → R v u

class Core.Logic.Modal.IsS4Frame {W : Type u_1} (R : AccessRel W) extends Std.Refl R, IsTrans W R : Prop

S4 frame: reflexive + transitive.

• refl (a : W) : R a a
• trans (a b c : W) : R a b → R b c → R a c

class Core.Logic.Modal.IsS5Frame {W : Type u_1} (R : AccessRel W) extends Std.Refl R, Core.Logic.Modal.IsEuclidean R : Prop

S5 frame: reflexive + euclidean (implies symmetric + transitive).

• refl (a : W) : R a a
• eucl (w v u : W) : R w v → R w u → R v u

class Core.Logic.Modal.IsKD45Frame {W : Type u_1} (R : AccessRel W) extends Core.Logic.Modal.IsSerial R, IsTrans W R, Core.Logic.Modal.IsEuclidean R : Prop

KD45 frame for textbook belief: serial + transitive + euclidean.

• serial (w : W) : ∃ (v : W), R w v
• trans (a b c : W) : R a b → R b c → R a c
• eucl (w v u : W) : R w v → R w u → R v u

class Core.Logic.Modal.IsK4EuclFrame {W : Type u_1} (R : AccessRel W) extends IsTrans W R, Core.Logic.Modal.IsEuclidean R : Prop

K4-Eucl frame: transitive + euclidean, NOT serial. The frame condition for commitment in [Sta84]-style discourse models, where commitment violations (no accessible compliance world) must be expressible.

• trans (a b c : W) : R a b → R b c → R a c
• eucl (w v u : W) : R w v → R w u → R v u

class Core.Logic.Modal.IsKTFrame {W : Type u_1} (R : AccessRel W) extends Std.Refl R : Prop

KT frame: reflexive. (T axiom alone.)

• refl (a : W) : R a a

class Core.Logic.Modal.IsKTBFrame {W : Type u_1} (R : AccessRel W) extends Std.Refl R, Std.Symm R : Prop

KTB frame: reflexive + symmetric. The natural setting for tolerance semantics ([CERvR12]) where each predicate's similarity relation is reflexive and symmetric but possibly non-transitive.

• refl (a : W) : R a a
• symm (a b : W) : R a b → R b a

class Core.Logic.Modal.IsBeliefRefinementOf {W : Type u_1} (Rk Rb : AccessRel W) : Prop

Rb is a belief refinement of Rk: every belief-accessible world is knowledge-accessible. The pure subset condition; whether Rk is S5 and Rb is KD45 is asserted by separate instance declarations.

• sub (w v : W) : Rb w v → Rk w v

instance Core.Logic.Modal.universalR_isRefl {W : Type u_1} : Std.Refl universalR

instance Core.Logic.Modal.universalR_isSerial {W : Type u_1} : IsSerial universalR

instance Core.Logic.Modal.universalR_isTrans {W : Type u_1} : IsTrans W universalR

instance Core.Logic.Modal.universalR_isSymm {W : Type u_1} : Std.Symm universalR

instance Core.Logic.Modal.universalR_isEuclidean {W : Type u_1} : IsEuclidean universalR

@[instance 100]

instance Core.Logic.Modal.Std.Refl.toIsSerial {W : Type u_1} {R : AccessRel W} [h : Std.Refl R] : IsSerial R

Reflexive relations are serial.

@[instance 100]

instance Core.Logic.Modal.instSymmOfReflOfIsEuclidean {W : Type u_1} {R : AccessRel W} [hR : Std.Refl R] [hE : IsEuclidean R] : Std.Symm R

Reflexive + Euclidean implies symmetric.

@[instance 100]

instance Core.Logic.Modal.instIsTransOfReflOfIsEuclidean {W : Type u_1} {R : AccessRel W} [hR : Std.Refl R] [hE : IsEuclidean R] : IsTrans W R

Reflexive + Euclidean implies transitive.

@[instance 100]

instance Core.Logic.Modal.instIsEuclideanOfSymmOfIsTrans {W : Type u_1} {R : AccessRel W} [hS : Std.Symm R] [hT : IsTrans W R] : IsEuclidean R

Symmetric + transitive implies euclidean.

def Core.Logic.Modal.box {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : Prop

Restricted necessity: □_R p at world w holds iff p v for all v accessible from w.

⟦□_R φ⟧^w = 1 iff ⟦φ⟧^v = 1 for all v with R(w,v).

This is the Kripke generalization of DWP's Rule B.13 (box); the Core.Logic.Modal.box operator in Quantification.lean is the universal-accessibility special case.

Equations

• Core.Logic.Modal.box R p w = ∀ (v : W), R w v → p v

def Core.Logic.Modal.diamond {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : Prop

Restricted possibility: ◇_R p at world w holds iff p v for some v accessible from w. Dual of box.

Equations

• Core.Logic.Modal.diamond R p w = ∃ (v : W), R w v ∧ p v

theorem Core.Logic.Modal.box_neg_diamond {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : box R p w = ¬diamond R (fun (v : W) => ¬p v) w

□_R p ↔ ¬◇_R ¬p — restricted modal duality.

theorem Core.Logic.Modal.diamond_neg_box {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : diamond R p w = ¬box R (fun (v : W) => ¬p v) w

◇_R p ↔ ¬□_R ¬p — dual form.