Restricted Modality: Modal Axioms, Decidability, Logic Lattice, Gallin Hierarchy

@cite{dowty-wall-peters-1981} @cite{kratzer-1981} @cite{kripke-1963}

Builds on the polymorphic Kripke foundation in Defs.lean. This file adds:

1. Modal axiom correspondence (T, D, 4, B, 5): which frame conditions on R validate which modal axioms when interpreted via boxR/diamondR. The K axiom holds for any R.

2. Monotonicity, distribution, restriction: standard properties of normal modal operators. Restriction (boxR_restrict) is Kratzer's insight that conversational backgrounds strengthen necessity.

3. Decidable instances: boxR R p w, diamondR R p w are decidable over finite worlds with decidable accessibility and propositions.

4. Logic lattice: Axiom, Logic, named logics (K, T, D, S4, S5, KD45), lattice instances, frameConditions predicate.

5. Gallin hierarchy (@cite{gallin-1975}): PropOp (general propositional operators), indicialNec/indicialPoss (Kripke-type), s5Nec/s5Poss (universal-accessibility = classical IL S5). The architectural anchor showing that classical IL S5 = the universal-accessibility special case of the polymorphic theory, and that non-Kripke operators (tense, progressive) live outside IsIndicial.

6. IL Frame specialization: with universal accessibility, boxR/diamondR recover S5 box/diamond from Quantification.lean — the formal bridge that the polymorphic theory contains classical IL as a special case.

Connection to Kratzer semantics

Kratzer's conversational backgrounds derive accessibility from a modal base: R_f(w, w') ≡ w' ∈ ⋂f(w). The ordering source further restricts to "best" worlds. In IL terms:

• Simple Kratzer necessity = boxR R_f (no ordering source)
• Full Kratzer necessity = boxR R_{f,g} where R_{f,g} restricts to best worlds
• S5 necessity = boxR (fun _ _ => True) = box

theorem Core.Logic.Intensional.boxR_K {W : Type u_1} (R : AccessRel W) (p q : W → Prop) (w : W) (hpq : boxR R (fun (v : W) => p v → q v) w) (hp : boxR R p w) : boxR R q w

K axiom: □_R(p → q) → (□_R p → □_R q). Holds for any accessibility relation.

theorem Core.Logic.Intensional.boxR_T {W : Type u_1} (R : AccessRel W) (hR : IsReflexive R) (p : W → Prop) (w : W) (h : boxR R p w) : p w

T axiom: reflexive R gives □_R p w → p w. What is necessary is actual.

theorem Core.Logic.Intensional.boxR_D {W : Type u_1} (R : AccessRel W) (hS : IsSerial R) (p : W → Prop) (w : W) (h : boxR R p w) : diamondR R p w

D axiom: serial R gives □_R p w → ◇_R p w. What is necessary is possible.

theorem Core.Logic.Intensional.boxR_four {W : Type u_1} (R : AccessRel W) (hT : IsTransitive R) (p : W → Prop) (w : W) (h : boxR R p w) : boxR R (boxR R p) w

4 axiom: transitive R gives □_R p → □_R □_R p. Positive introspection.

theorem Core.Logic.Intensional.boxR_B {W : Type u_1} (R : AccessRel W) (hS : IsSymmetric R) (p : W → Prop) (w : W) (h : p w) : boxR R (diamondR R p) w

B axiom: symmetric R gives p w → □_R ◇_R p w. What is actual is necessarily possible.

theorem Core.Logic.Intensional.boxR_five {W : Type u_1} (R : AccessRel W) (hE : IsEuclidean R) (p : W → Prop) (w : W) (h : diamondR R p w) : boxR R (diamondR R p) w

5 axiom: euclidean R gives ◇_R p w → □_R ◇_R p w. Positive possibility introspection.

theorem Core.Logic.Intensional.boxR_mono {W : Type u_1} (R : AccessRel W) {p q : W → Prop} (h : ∀ (v : W), p v → q v) (w : W) (hb : boxR R p w) : boxR R q w

boxR R is monotone: if p ≤ q pointwise, then □_R p ≤ □_R q.

theorem Core.Logic.Intensional.diamondR_mono {W : Type u_1} (R : AccessRel W) {p q : W → Prop} (h : ∀ (v : W), p v → q v) (w : W) (hd : diamondR R p w) : diamondR R q w

diamondR R is monotone.

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

□_R distributes over ∧.

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

◇_R distributes over ∨.

theorem Core.Logic.Intensional.boxR_necessitation {W : Type u_1} (R : AccessRel W) (p : W → Prop) (h : ∀ (v : W), p v) (w : W) : boxR R p w

Necessitation: if p holds at every world, then □_R p holds everywhere.

theorem Core.Logic.Intensional.boxR_restrict {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) (hb : boxR R₁ p w) : boxR R₂ p w

Restricting accessibility strengthens necessity: if R₂ ⊆ R₁, then □_{R₁} p → □_{R₂} p.

theorem Core.Logic.Intensional.diamondR_restrict {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) (hd : diamondR R₂ p w) : diamondR R₁ p w

Restricting accessibility weakens possibility: if R₂ ⊆ R₁, then ◇_{R₂} p → ◇_{R₁} p.

theorem Core.Logic.Intensional.S5_frame_all_axioms {W : Type u_1} (R : AccessRel W) (hR : IsReflexive R) (hE : IsEuclidean R) : (∀ (p : W → Prop) (w : W), boxR R p w → p w) ∧ (∀ (p : W → Prop) (w : W), boxR R p w → diamondR R p w) ∧ (∀ (p : W → Prop) (w : W), boxR R p w → boxR R (boxR R p) w) ∧ (∀ (p : W → Prop) (w : W), p w → boxR R (diamondR R p) w) ∧ ∀ (p : W → Prop) (w : W), diamondR R p w → boxR R (diamondR R p) w

With reflexive + euclidean accessibility (= S5 frame conditions), boxR validates all of T, D, 4, B, 5.

theorem Core.Logic.Intensional.boxR_eq_forall {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : boxR R p w = ∀ (v : W), R w v → p v

boxR R p i is the infimum of p v over worlds v accessible from w.

theorem Core.Logic.Intensional.diamondR_eq_exists {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) : diamondR R p w = ∃ (v : W), R w v ∧ p v

diamondR R p w is the supremum of p v over worlds v accessible from w.

The Gallin hierarchy (@cite{gallin-1975})

In IL/ML_p, propositional operators form a three-level hierarchy:

1. General (PropOp): Any (W → Prop) → W → Prop — arbitrary properties of propositions, varying by world.

2. Indicial (= Kripke-type): Operators definable via an accessibility relation R. The necessity variant is ∀ v, R w v → p v (= boxR); the possibility variant is ∃ v, R w v ∧ p v (= diamondR).

3. S5: The indicial case with R = universalR — IL's box/diamond.

All PropOps  ⊋  Indicial (Kripke)  ⊋  S5 (IL's □)

Why this is here even with no current downstream consumer. These theorems are the architectural anchor for the design choice that restricted modality lives in Core/Logic/Intensional/: they prove that classical IL S5 is exactly the universal-accessibility special case of the polymorphic theory, and that every boxR R is a normal modal operator (monotone, distribConj). Non-indicial PropOps (e.g., tense, present progressive) are the formal extension point for tense / non-Kripke modal operators that cannot be expressed as boxR R for any R. Removing this section would erase the formal record of why the directory layout is what it is.

@[reducible, inline]

abbrev Core.Logic.Intensional.PropOp (W : Type u_2) : Type u_2

A propositional operator: any function from propositions to propositions, parametrized by world. This is Gallin's most general level — an arbitrary property of propositions varying by index.

Examples: necessity (boxR R), possibility (diamondR R), past tense (∃ v, v < w ∧ p v), present progressive, habituals.

Equations

• Core.Logic.Intensional.PropOp W = ((W → Prop) → W → Prop)

def Core.Logic.Intensional.PropOp.Monotone {W : Type u_2} (N : PropOp W) : Prop

A propositional operator N is monotone if p ≤ q pointwise implies N p ≤ N q pointwise. Every K-operator (= normal modal operator) is monotone.

Equations

• N.Monotone = ∀ {p q : W → Prop}, (∀ (v : W), p v → q v) → ∀ (w : W), N p w → N q w

def Core.Logic.Intensional.PropOp.DistribConj {W : Type u_2} (N : PropOp W) : Prop

A propositional operator distributes over conjunction (one direction of the K axiom: □(p ∧ q) → □p ∧ □q).

Equations

• N.DistribConj = ∀ (p q : W → Prop) (w : W), N (fun (v : W) => p v ∧ q v) w → N p w ∧ N q w

def Core.Logic.Intensional.indicialNec {W : Type u_2} (R : AccessRel W) : PropOp W

An indicial necessity operator: the restriction of PropOp to operators definable via an accessibility relation. indicialNec R p w ↔ ∀ v, R w v → p v.

This is boxR viewed as a member of the Gallin hierarchy.

Equations

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

def Core.Logic.Intensional.indicialPoss {W : Type u_2} (R : AccessRel W) : PropOp W

An indicial possibility operator (dual). indicialPoss R p w ↔ ∃ v, R w v ∧ p v.

Equations

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

theorem Core.Logic.Intensional.boxR_eq_indicialNec {W : Type u_1} (R : AccessRel W) : boxR R = indicialNec R

boxR IS indicialNec — definitional equality.

theorem Core.Logic.Intensional.diamondR_eq_indicialPoss {W : Type u_1} (R : AccessRel W) : diamondR R = indicialPoss R

diamondR IS indicialPoss — definitional equality.

def Core.Logic.Intensional.IsIndicial {W : Type u_2} (N : PropOp W) : Prop

A propositional operator is indicial if there exists an accessibility relation R such that N = indicialNec R. The non-indicial case is where tense and other non-Kripke operators live.

Equations

• Core.Logic.Intensional.IsIndicial N = ∃ (R : Core.Logic.Intensional.AccessRel W), N = Core.Logic.Intensional.indicialNec R

theorem Core.Logic.Intensional.boxR_isIndicial {W : Type u_1} (R : AccessRel W) : IsIndicial (boxR R)

Every boxR R is indicial.

theorem Core.Logic.Intensional.indicial_monotone {W : Type u_1} (R : AccessRel W) : (indicialNec R).Monotone

Every indicial operator is monotone (every Kripke operator is a K-operator).

theorem Core.Logic.Intensional.indicial_distribConj {W : Type u_1} (R : AccessRel W) : (indicialNec R).DistribConj

Every indicial operator distributes over conjunction.

def Core.Logic.Intensional.s5Nec {W : Type u_2} : PropOp W

S5 necessity as a PropOp: p holds at all worlds.

Equations

• Core.Logic.Intensional.s5Nec p x✝ = ∀ (w : W), p w

def Core.Logic.Intensional.s5Poss {W : Type u_2} : PropOp W

S5 possibility as a PropOp: p holds at some world.

Equations

• Core.Logic.Intensional.s5Poss p x✝ = ∃ (w : W), p w

theorem Core.Logic.Intensional.s5Nec_eq_indicialNec_universalR {W : Type u_1} : s5Nec = indicialNec universalR

S5 = indicialNec universalR: the S5 necessity operator is the indicial operator with universal accessibility. The formal statement that S5 sits at the top of the indicial hierarchy.

theorem Core.Logic.Intensional.s5Nec_isIndicial {W : Type u_1} : IsIndicial s5Nec

S5 necessity is indicial.

theorem Core.Logic.Intensional.indicialNec_weaker_of_sub {W : Type u_1} {R₁ R₂ : AccessRel W} (h : ∀ (w v : W), R₂ w v → R₁ w v) (p : W → Prop) (w : W) : indicialNec R₁ p w → indicialNec R₂ p w

Restriction order on indicial operators: if R₂ ⊆ R₁ then indicialNec R₁ is weaker than indicialNec R₂ — fewer accessible worlds means a stronger necessity.

S5 (R = universal) is the weakest; empty R is the strongest (vacuously true). This is Kratzer's insight that conversational backgrounds restrict the modal base, formalized at the PropOp level.

theorem Core.Logic.Intensional.s5Nec_weakest {W : Type u_1} (R : AccessRel W) (p : W → Prop) (w : W) (h : s5Nec p w) : indicialNec R p w

S5 necessity is the weakest indicial operator: for any R, s5Nec p w → indicialNec R p w.

theorem Core.Logic.Intensional.indicialNec_emptyR {W : Type u_1} (p : W → Prop) (w : W) : indicialNec emptyR p w

Empty accessibility gives the strongest (vacuously true) indicial operator.

Following mathlib conventions: definitions are Prop-valued (in Defs.lean), with Decidable instances providing computation. With [Fintype W], [DecidableRel R], and [DecidablePred p], formulas like boxR R p w and IsReflexive R reduce by decide.

@[implicit_reducible]

instance Core.Logic.Intensional.boxR_decidable {W : Type u_2} [Fintype W] (R : AccessRel W) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (boxR R p w)

boxR R p w is decidable when worlds enumerate, accessibility is decidable, and the proposition is decidable.

Equations

• Core.Logic.Intensional.boxR_decidable R p w = decidable_of_iff (∀ v ∈ Finset.univ, R w v → p v) ⋯

@[implicit_reducible]

instance Core.Logic.Intensional.diamondR_decidable {W : Type u_2} [Fintype W] (R : AccessRel W) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (diamondR R p w)

diamondR R p w is decidable under the same conditions as boxR.

Equations

• Core.Logic.Intensional.diamondR_decidable R p w = decidable_of_iff (∃ v ∈ Finset.univ, R w v ∧ p v) ⋯

inductive Core.Logic.Intensional.Axiom : Type

Axiom schemas addable to K.

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

@[implicit_reducible]

instance Core.Logic.Intensional.instDecidableEqAxiom : DecidableEq Axiom

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.instReprAxiom : Repr Axiom

Equations

• Core.Logic.Intensional.instReprAxiom = { reprPrec := Core.Logic.Intensional.instReprAxiom.repr }

def Core.Logic.Intensional.instReprAxiom.repr : Axiom → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.instInhabitedAxiom : Inhabited Axiom

Equations

• Core.Logic.Intensional.instInhabitedAxiom = { default := Core.Logic.Intensional.instInhabitedAxiom.default }

def Core.Logic.Intensional.instInhabitedAxiom.default : Axiom

Equations

• Core.Logic.Intensional.instInhabitedAxiom.default = Core.Logic.Intensional.Axiom.M

def Core.Logic.Intensional.instHashableAxiom.hash : Axiom → UInt64

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.instHashableAxiom : Hashable Axiom

Equations

• Core.Logic.Intensional.instHashableAxiom = { hash := Core.Logic.Intensional.instHashableAxiom.hash }

@[implicit_reducible]

instance Core.Logic.Intensional.instToStringAxiom : ToString Axiom

Equations

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

structure Core.Logic.Intensional.Logic : Type

A normal modal logic is K plus axiom schemas.

• axioms : Finset Axiom

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

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.instDecidableEqLogic : DecidableEq Logic

Equations

• Core.Logic.Intensional.instDecidableEqLogic = Core.Logic.Intensional.instDecidableEqLogic.decEq

def Core.Logic.Intensional.Logic.K : Logic

Equations

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

def Core.Logic.Intensional.Logic.T : Logic

Equations

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

def Core.Logic.Intensional.Logic.D : Logic

Equations

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

def Core.Logic.Intensional.Logic.KB : Logic

Equations

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

def Core.Logic.Intensional.Logic.K4 : Logic

Equations

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

def Core.Logic.Intensional.Logic.K5 : Logic

Equations

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

def Core.Logic.Intensional.Logic.S4 : Logic

Equations

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

def Core.Logic.Intensional.Logic.S5 : Logic

Equations

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

def Core.Logic.Intensional.Logic.KTB : Logic

Equations

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

def Core.Logic.Intensional.Logic.KD45 : Logic

Equations

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

def Core.Logic.Intensional.Logic.K45 : Logic

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instLE : LE Logic

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

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instPartialOrder : PartialOrder Logic

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instLattice : Lattice Logic

Equations

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

def Core.Logic.Intensional.Logic.top : Logic

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instOrderBot : OrderBot Logic

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instOrderTop : OrderTop Logic

Equations

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

@[implicit_reducible]

instance Core.Logic.Intensional.Logic.instBoundedOrder : BoundedOrder Logic

Equations

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

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

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

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

Equations

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

def Core.Logic.Intensional.Logic.frameConditions {W : Type u_2} (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.

Bridge theorems connecting the polymorphic infrastructure to Montague's IL. With universal accessibility, boxR/diamondR recover S5 box/diamond from Quantification.lean. These would all be rfl if box/diamond were definitionally boxR universalR ∘ pick-an-index — see the Quantification module for the layering question. As stated they're one-step simp proofs.

theorem Core.Logic.Intensional.boxR_universal {F : Frame} (p : F.Denot Ty.prop) : (fun (i : F.Index) => boxR universalR p i) = fun (x : F.Index) => box p

S5 necessity (box) is restricted necessity with universal accessibility.

theorem Core.Logic.Intensional.diamondR_universal {F : Frame} (p : F.Denot Ty.prop) : (fun (i : F.Index) => diamondR universalR p i) = fun (x : F.Index) => diamond p

S5 possibility (diamond) is restricted possibility with universal accessibility.

theorem Core.Logic.Intensional.box_implies_boxR {F : Frame} (R : AccessRel F.Index) (p : F.Denot Ty.prop) (h : box p) (i : F.Index) : boxR R p i

S5 box implies any restricted box.

theorem Core.Logic.Intensional.diamondR_implies_diamond {F : Frame} (R : AccessRel F.Index) (p : F.Denot Ty.prop) (i : F.Index) (h : diamondR R p i) : diamond p

Any restricted diamond implies S5 diamond.

theorem Core.Logic.Intensional.valid_boxR {F : Frame} (R : AccessRel F.Index) (p : F.Denot Ty.prop) (hv : Algebra.valid p) (i : F.Index) : boxR R p i

A valid proposition is R-necessary at every world (for any R).

theorem Core.Logic.Intensional.boxR_entailment_lift {F : Frame} (R : AccessRel F.Index) (p q : F.Denot Ty.prop) (h : ∀ (v : F.Index), p v → q v) (i : F.Index) (hb : boxR R p i) : boxR R q i

Semantic entailment lifts to restricted modality: if p ⊨ q then □_R p ⊨ □_R q.