Polymorphic Kripke Foundation

@cite{kripke-1963}

The bare foundation for accessibility-restricted modal logic, parameterised by {W : Type*} — no Frame, no Entity, no type system. This file holds the definitions and very simple lemmas that the rest of Core.Logic.Intensional (including Montague's S5 box/diamond in Quantification.lean and the modal-axiom theorems in RestrictedModality.lean) builds on.

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

@[reducible, inline]

abbrev Core.Logic.Intensional.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.Intensional.AccessRel W = (W → W → Prop)

@[reducible, inline]

abbrev Core.Logic.Intensional.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.Intensional.AgentAccessRel W E = (E → Core.Logic.Intensional.AccessRel W)

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

Universal accessibility: every world is accessible from every world.

Equations

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

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

Empty accessibility: no world is accessible from any world.

Equations

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

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

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

Equations

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

def Core.Logic.Intensional.IsReflexive {W : Type u_1} (R : AccessRel W) : Prop

Reflexivity: every world accesses itself.

Equations

• Core.Logic.Intensional.IsReflexive R = ∀ (w : W), R w w

def Core.Logic.Intensional.IsSerial {W : Type u_1} (R : AccessRel W) : Prop

Seriality: every world accesses at least one world.

Equations

• Core.Logic.Intensional.IsSerial R = ∀ (w : W), ∃ (v : W), R w v

def Core.Logic.Intensional.IsTransitive {W : Type u_1} (R : AccessRel W) : Prop

Transitivity.

Equations

• Core.Logic.Intensional.IsTransitive R = ∀ (w v u : W), R w v → R v u → R w u

def Core.Logic.Intensional.IsSymmetric {W : Type u_1} (R : AccessRel W) : Prop

Symmetry.

Equations

• Core.Logic.Intensional.IsSymmetric R = ∀ (w v : W), R w v → R v w

def Core.Logic.Intensional.IsEuclidean {W : Type u_1} (R : AccessRel W) : Prop

Euclideanness.

Equations

• Core.Logic.Intensional.IsEuclidean R = ∀ (w v u : W), R w v → R w u → R v u

theorem Core.Logic.Intensional.universalR_refl {W : Type u_1} : IsReflexive universalR

theorem Core.Logic.Intensional.universalR_serial {W : Type u_1} : IsSerial universalR

theorem Core.Logic.Intensional.universalR_trans {W : Type u_1} : IsTransitive universalR

theorem Core.Logic.Intensional.universalR_symm {W : Type u_1} : IsSymmetric universalR

theorem Core.Logic.Intensional.universalR_eucl {W : Type u_1} : IsEuclidean universalR

theorem Core.Logic.Intensional.refl_serial {W : Type u_1} {R : AccessRel W} (h : IsReflexive R) : IsSerial R

theorem Core.Logic.Intensional.refl_eucl_symm {W : Type u_1} {R : AccessRel W} (hR : IsReflexive R) (hE : IsEuclidean R) : IsSymmetric R

theorem Core.Logic.Intensional.refl_eucl_trans {W : Type u_1} {R : AccessRel W} (hR : IsReflexive R) (hE : IsEuclidean R) : IsTransitive R

theorem Core.Logic.Intensional.symm_trans_eucl {W : Type u_1} {R : AccessRel W} (hS : IsSymmetric R) (hT : IsTransitive R) : IsEuclidean R

theorem Core.Logic.Intensional.S5_equiv {W : Type u_1} {R : AccessRel W} (hR : IsReflexive R) (hE : IsEuclidean R) : IsReflexive R ∧ IsSymmetric R ∧ IsTransitive R

S5 frames are equivalence relations.

theorem Core.Logic.Intensional.S4_preorder {W : Type u_1} {R : AccessRel W} (hR : IsReflexive R) (hT : IsTransitive R) : IsReflexive R ∧ IsTransitive R

S4 frames are preorders.

theorem Core.Logic.Intensional.M_implies_D {W : Type u_1} {R : AccessRel W} (hM : IsReflexive R) : IsSerial R

M implies D (reflexive implies serial).

theorem Core.Logic.Intensional.M5_implies_B {W : Type u_1} {R : AccessRel W} (hM : IsReflexive R) (h5 : IsEuclidean R) : IsSymmetric R

M + 5 implies B.

theorem Core.Logic.Intensional.M5_implies_4 {W : Type u_1} {R : AccessRel W} (hM : IsReflexive R) (h5 : IsEuclidean R) : IsTransitive R

M + 5 implies 4.

def Core.Logic.Intensional.boxR {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.Intensional.box operator in Quantification.lean is the universal-accessibility special case.

Equations

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

def Core.Logic.Intensional.diamondR {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 boxR.

Equations

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

theorem Core.Logic.Intensional.boxR_neg_diamondR {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : boxR R p w = ¬diamondR R (fun (v : W) => ¬p v) w

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

theorem Core.Logic.Intensional.diamondR_neg_boxR {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : diamondR R p w = ¬boxR R (fun (v : W) => ¬p v) w

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