Kaplanian Context of Utterance

@cite{kaplan-1989} @cite{speas-tenny-2003}

The full context tuple ⟨agent, world, time, position⟩ from @cite{kaplan-1989} "Demonstratives" §XVIII. Framework-agnostic infrastructure used by reference theory, tense semantics, mood, and RSA.

The simple Context W E (agent + world) in Reference/Basic.lean is a projection; KContext is the full Kaplanian structure.

structure Core.Context.KContext (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

Full Kaplanian context of utterance: ⟨agent, world, time, position⟩.

@cite{kaplan-1989} §XVIII: "A context is a tuple ⟨cₐ, cw, ct, cp⟩ where cₐ is the agent, cw the world, ct the time, and cp the position."

• agent : E

  The agent (speaker) of the context

• addressee : E

  The addressee (hearer) of the context

• world : W

  The world of the context

• time : T

  The time of the context

• position : P

  The position (location) of the context

def Core.Context.ProperContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (exists_ : E → W → Prop) : Prop

Proper context: the agent exists at the context's world.

@cite{kaplan-1989} §XVIII Remark 3: contexts are proper only if the agent exists at the world of the context. This validates ⊨ Exist I.

Equations

• Core.Context.ProperContext c exists_ = exists_ c.agent c.world

def Core.Context.LocatedContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (located : E → P → T → W → Prop) : Prop

Located context: the agent is at the context's position at the context's time in the context's world.

Validates ⊨ N(Located(I, Here)).

Equations

• Core.Context.LocatedContext c located = located c.agent c.position c.time c.world

def Core.Context.KContext.toSituation {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) : WorldTimeIndex W T

Project a KContext to a WorldTimeIndex (world + time pair).

Equations

• c.toSituation = { world := c.world, time := c.time }

def Core.Context.KContext.shiftWorldTime {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (s : WorldTimeIndex W T) : KContext W E P T

Replace the world and time of a KContext with those of a WorldTimeIndex, preserving agent / addressee / position. The natural "shift to alternative situation" operation: an agent at an evaluation context can hold the same centered identity (agent) while considering an alternative ⟨world, time⟩. Used by centered-world de re semantics to quantify the time-concept across a believer's doxastic or metaphysical alternative situations.

Equations

• c.shiftWorldTime s = { agent := c.agent, addressee := c.addressee, world := s.world, time := s.time, position := c.position }

@[simp]

theorem Core.Context.KContext.shiftWorldTime_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (s : WorldTimeIndex W T) : (c.shiftWorldTime s).world = s.world

@[simp]

theorem Core.Context.KContext.shiftWorldTime_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (s : WorldTimeIndex W T) : (c.shiftWorldTime s).time = s.time

@[simp]

theorem Core.Context.KContext.shiftWorldTime_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (s : WorldTimeIndex W T) : (c.shiftWorldTime s).agent = c.agent

@[simp]

theorem Core.Context.KContext.shiftWorldTime_toSituation {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (s : WorldTimeIndex W T) : (c.shiftWorldTime s).toSituation = s

def Core.Context.KContext.toReichenbachFrame {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) (R Ev : T) : Time.Reichenbach.ReichenbachFrame T

Project a KContext into a root-clause ReichenbachFrame. Speech time S = context time; perspective time P = S (root clause default, @cite{kiparsky-2002}); R and E are supplied per clause.

Equations

• c.toReichenbachFrame R Ev = { speechTime := c.time, perspectiveTime := c.time, referenceTime := R, eventTime := Ev }