LD Structure

structure Semantics.Reference.KaplanLD.LDStructure : Type 1

Full LD model structure (@cite{kaplan-1989} §XVIII).

An LD structure provides the domains (worlds, entities, positions, times), context parameters (agent, world, time, position projections), and the proper-context constraint.

• W : Type

  Possible worlds

• U : Type

  Universe of individuals

• P : Type

  Positions (locations)

• T : Type

  Times

• C : Type

  Set of contexts (a subset of W × U × P × T)

• cAgent : self.C → self.U

  Agent of a context

• cAddressee : self.C → self.U

  Addressee of a context (@cite{speas-tenny-2003} extension)

• cWorld : self.C → self.W

  World of a context

• cTime : self.C → self.T

  Time of a context

• cPosition : self.C → self.P

  Position of a context

• exists_ : self.U → self.W → Prop

  Existence predicate: entity exists at world

• located : self.U → self.P → self.T → self.W → Prop

  Location predicate: entity is at position at time in world

• proper (c : self.C) : self.exists_ (self.cAgent c) (self.cWorld c)

  Proper-context constraint (Kaplan §XVIII): the agent of every context exists at the world of that context. This validates ⊨ Exist I.

def Semantics.Reference.KaplanLD.LDStructure.toKContext (ld : LDStructure) (c : ld.C) : Core.Context.KContext ld.W ld.U ld.P ld.T

Extract a KContext from an LD structure at a context index.

Equations

• ld.toKContext c = { agent := ld.cAgent c, addressee := ld.cAddressee c, world := ld.cWorld c, time := ld.cTime c, position := ld.cPosition c }

Dthat Operator (§XII)

def Semantics.Reference.KaplanLD.dthat {W : Type u_1} {T : Type u_2} {τ : Type u_3} (α : W → T → τ) (cW : W) (cT : T) : Core.Intension W τ

dthat α cW cT — Kaplan's rigidifier: evaluate α at the context parameters (world cW, time cT), then rigidify the result.

dthat[α] is an expression whose content at context c is the rigid intension constantly returning α's extension at ⟨c_w, c_t⟩.

Equations

• Semantics.Reference.KaplanLD.dthat α cW cT = Core.Intension.rigid (α cW cT)

def Semantics.Reference.KaplanLD.dthatW {W : Type u_1} {τ : Type u_2} (α : Core.Intension W τ) (cW : W) : Core.Intension W τ

Simplified world-only dthat (when T is not relevant).

Equations

• Semantics.Reference.KaplanLD.dthatW α cW = Core.Intension.rigid (α cW)

theorem Semantics.Reference.KaplanLD.dthat_isRigid {W : Type u_1} {T : Type u_2} {τ : Type u_3} (α : W → T → τ) (cW : W) (cT : T) : (dthat α cW cT).IsRigid

dthat[α] has Stable Content: it is rigid.

theorem Semantics.Reference.KaplanLD.dthatW_isRigid {W : Type u_1} {τ : Type u_2} (α : Core.Intension W τ) (cW : W) : (dthatW α cW).IsRigid

dthatW[α] is rigid.

theorem Semantics.Reference.KaplanLD.alpha_eq_dthat_alpha {W : Type u_1} {τ : Type u_2} (α : Core.Intension W τ) (w : W) : α w = dthatW α w w

Remark 3: α = dthat[α] is valid — at the context world, α and dthat[α] agree.

For any α and world w, α w = dthatW α w w.

theorem Semantics.Reference.KaplanLD.box_alpha_eq_dthat_not_valid {W : Type u_1} {τ : Type u_2} (α : Core.Intension W τ) (cW w' : W) (h : α w' ≠ α cW) : α w' ≠ dthatW α cW w'

□(α = dthat[α]) is NOT valid in general: dthat[α] is rigid but α may not be. If α varies across worlds, there exists a world w' where α w' ≠ dthatW α cW w'.

We state this as: given α that varies, the universal closure fails.

Indexical Operators (Content Operators, §VI)

def Semantics.Reference.KaplanLD.opNow {W : Type u_1} {T : Type u_2} (cT : T) (φ : W → T → Prop) : W → T → Prop

N ("now"): shift evaluation time to context time.

opNow cT φ evaluates φ at the context time cT instead of the circumstance time. This is a content operator — it operates on the circumstance of evaluation.

Equations

• Semantics.Reference.KaplanLD.opNow cT φ w x✝ = φ w cT

def Semantics.Reference.KaplanLD.opActually {W : Type u_1} {T : Type u_2} (cW : W) (φ : W → T → Prop) : W → T → Prop

A ("actually"): shift evaluation world to context world.

opActually cW φ evaluates φ at the context world cW instead of the circumstance world.

Equations

• Semantics.Reference.KaplanLD.opActually cW φ x✝ t = φ cW t

def Semantics.Reference.KaplanLD.opYesterday {W : Type u_1} {T : Type u_2} [HSub T ℕ T] (cT : T) (φ : W → T → Prop) : W → T → Prop

Y ("yesterday"): shift evaluation time to cT - 1 (requires HSub).

Equations

• Semantics.Reference.KaplanLD.opYesterday cT φ w x✝ = φ w (cT - 1)

Tense Operators (Circumstance Operators)

def Semantics.Reference.KaplanLD.opFuture {W : Type u_1} {T : Type u_2} [LT T] (times : List T) (φ : W → T → Prop) : W → T → Prop

F (future): ∃t' in times with t' > t such that φ at ⟨w, t'⟩.

Equations

• Semantics.Reference.KaplanLD.opFuture times φ w t = ∃ t' ∈ times, t < t' ∧ φ w t'

def Semantics.Reference.KaplanLD.opPast {W : Type u_1} {T : Type u_2} [LT T] (times : List T) (φ : W → T → Prop) : W → T → Prop

P (past): ∃t' in times with t' < t such that φ at ⟨w, t'⟩.

Equations

• Semantics.Reference.KaplanLD.opPast times φ w t = ∃ t' ∈ times, t' < t ∧ φ w t'

Modal Operators

def Semantics.Reference.KaplanLD.opBox {W : Type u_1} {T : Type u_2} (worlds : List W) (φ : W → T → Prop) : W → T → Prop

□ (box): ∀w' in worlds, φ at ⟨w', t⟩.

Equations

• Semantics.Reference.KaplanLD.opBox worlds φ x✝ t = ∀ w' ∈ worlds, φ w' t

def Semantics.Reference.KaplanLD.opDiamond {W : Type u_1} {T : Type u_2} (worlds : List W) (φ : W → T → Prop) : W → T → Prop

◇ (diamond): ∃w' in worlds, φ at ⟨w', t⟩.

Equations

• Semantics.Reference.KaplanLD.opDiamond worlds φ x✝ t = ∃ w' ∈ worlds, φ w' t

Key Metatheorems

theorem Semantics.Reference.KaplanLD.exist_i_valid (ld : LDStructure) (c : ld.C) : ld.exists_ (ld.cAgent c) (ld.cWorld c)

⊨ Exist I: at every (proper) context, the agent exists.

Follows directly from LDStructure.proper. @cite{kaplan-1989} §XVIII Remark 3.

theorem Semantics.Reference.KaplanLD.i_am_located_valid (ld : LDStructure) (locatedProper : ∀ (c : ld.C), ld.located (ld.cAgent c) (ld.cPosition c) (ld.cTime c) (ld.cWorld c)) (c : ld.C) : ld.located (ld.cAgent c) (ld.cPosition c) (ld.cTime c) (ld.cWorld c)

⊨ N(Located(I, Here)): the agent is located at the context's position at the context's time in the context's world.

Requires a locatedProper hypothesis: an LD structure where contexts satisfy the location constraint.

theorem Semantics.Reference.KaplanLD.actually_stable {W : Type u_1} {T : Type u_2} (cW : W) (φ : W → T → Prop) (t : T) (w₁ w₂ : W) : opActually cW φ w₁ t = opActually cW φ w₂ t

A(φ) produces Stable Content: the result is world-independent.

opActually cW φ evaluates φ at cW regardless of the evaluation world, so changing the evaluation world has no effect.