Standard context shifts

The shifts of Context that embedding operators push: an attitude verb makes the holder the agent and an accessible world the world (attitudeShift, [schlenker-2003]), and a sequence-of-tense embedding moves the time to the matrix event time (temporalShift, [von-stechow-2009]); a Kaplan-compliant English attitude verb pushes the identity 1. The lemmas record which coordinates each shift changes and which it preserves.

References

• [schlenker-2003]
• [von-stechow-2009]

def Reference.attitudeShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) : Function.End (Context W E P T)

The attitude shift: the holder becomes the agent and the attitude world the world; addressee, time and position are preserved.

Equations

• Reference.attitudeShift holder attWorld c = { agent := holder, addressee := c.addressee, world := attWorld, time := c.time, position := c.position }

def Reference.temporalShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) : Function.End (Context W E P T)

The temporal shift: the time moves to newTime; every other coordinate is preserved.

Equations

• Reference.temporalShift newTime c = { agent := c.agent, addressee := c.addressee, world := c.world, time := newTime, position := c.position }

@[simp]

theorem Reference.attitudeShift_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (holder : E) (attWorld : W) : (attitudeShift holder attWorld c).agent = holder

@[simp]

theorem Reference.attitudeShift_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (holder : E) (attWorld : W) : (attitudeShift holder attWorld c).world = attWorld

@[simp]

theorem Reference.attitudeShift_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (holder : E) (attWorld : W) : (attitudeShift holder attWorld c).addressee = c.addressee

@[simp]

theorem Reference.attitudeShift_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (holder : E) (attWorld : W) : (attitudeShift holder attWorld c).time = c.time

@[simp]

theorem Reference.attitudeShift_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (holder : E) (attWorld : W) : (attitudeShift holder attWorld c).position = c.position

@[simp]

theorem Reference.temporalShift_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (newTime : T) : (temporalShift newTime c).time = newTime

@[simp]

theorem Reference.temporalShift_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (newTime : T) : (temporalShift newTime c).agent = c.agent

@[simp]

theorem Reference.temporalShift_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (newTime : T) : (temporalShift newTime c).world = c.world

@[simp]

theorem Reference.temporalShift_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (newTime : T) : (temporalShift newTime c).addressee = c.addressee

@[simp]

theorem Reference.temporalShift_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E P T) (newTime : T) : (temporalShift newTime c).position = c.position