The context of utterance

The context of utterance of [kaplan-1989], a tuple of an agent, a world, a time and a position, with the addressee of [ST03] as a fifth coordinate. A context is proper when its agent exists at its world (Context.Proper), which validates I exist, and located when its agent is at its position at its time in its world (Context.Located), which validates I am here now. The world and time of a context form its index of evaluation (Context.toIndex), and replacing them by another index (Context.shiftWorldTime) is the shift to an alternative situation that keeps the agent fixed, used to quantify a concept across a believer's alternatives.

Contexts may also be taken as primitive, with functions returning their coordinates [schlenker-2011]: Kaplan's tenets in Reference/Kaplan.lean take the coordinate projections as arguments, and Context supplies them.

References

• [kaplan-1989]
• [ST03]
• [schlenker-2011]

structure Reference.Context (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)

The context of utterance: an agent, an addressee, a world, a time and a 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

@[instance_reducible]

instance Reference.instDecidableEqContext {W✝ : Type u_1} {E✝ : Type u_2} {P✝ : Type u_3} {T✝ : Type u_4} [DecidableEq W✝] [DecidableEq E✝] [DecidableEq P✝] [DecidableEq T✝] : DecidableEq (Context W✝ E✝ P✝ T✝)

Equations

• Reference.instDecidableEqContext = Reference.instDecidableEqContext.decEq

def Reference.instDecidableEqContext.decEq {W✝ : Type u_1} {E✝ : Type u_2} {P✝ : Type u_3} {T✝ : Type u_4} [DecidableEq W✝] [DecidableEq E✝] [DecidableEq P✝] [DecidableEq T✝] (x✝ x✝¹ : Context W✝ E✝ P✝ T✝) : Decidable (x✝ = x✝¹)

Equations

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

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

A proper context: the agent exists at the context's world.

Equations

• c.Proper exists_ = exists_ c.agent c.world

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

A located context: the agent is at the context's position at its time in its world.

Equations

• c.Located located = located c.agent c.position c.time c.world

def Reference.Context.toIndex {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) : Index W T

The index of evaluation of a context: its world and time.

Equations

• c.toIndex = (c.world, c.time)

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

Replace the world and time of a context by those of an index, keeping the agent, the addressee and the position.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Reference.Context.shiftWorldTime_toIndex {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (s : Index W T) : (c.shiftWorldTime s).toIndex = s