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) : Situation W T

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

Equations

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

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) : 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 }