Documentation

Linglib.Theories.Semantics.Tense.ModalTense

@cite{klecha-2016}: Modality and Embedded Temporal Operators #

@cite{klecha-2016}

Klecha's theory: modals shift the evaluation time, not just attitude verbs. This means tense under a modal is checked against the modal's evaluation time, explaining modal-tense interactions that other theories leave unaddressed.

Core Mechanisms #

  1. Modal eval time shift: modals shift the temporal evaluation context, parallel to how attitude verbs shift it
  2. Tense under modals: embedded tense is checked against the modal's eval time, not speech time

Key Innovation #

Most tense theories (Abusch, Von Stechow, Kratzer, Ogihara) only address tense under attitude verbs. Klecha extends the eval-time shift to modals: "John might have left" involves past tense checked against the modal's evaluation time, not against speech time.

This is formalized via the evalTimeIndex field on TensePronoun: modals update this index just as attitude verbs do.

source
def Semantics.Tense.ModalTense.modalEvalTimeShift {Time : Type u_1} (modalEvalTime : Time) (g : Core.Tense.TemporalAssignment Time) (evalIdx : ℕ) :
Core.Tense.TemporalAssignment Time

Klecha's modal eval time shift: a modal operator shifts the temporal evaluation context for its complement, parallel to attitude verbs.

modalEvalTime: the time at which the modal is evaluated g: temporal assignment evalIdx: index of the eval time variable

The result is a new assignment where g(evalIdx) = modalEvalTime.

Equations
Instances For
    source
    theorem Semantics.Tense.ModalTense.modalShift_gives_evalTime {Time : Type u_1} (modalEvalTime : Time) (g : Core.Tense.TemporalAssignment Time) (evalIdx : ℕ) :
    Core.Tense.interpTense evalIdx (modalEvalTimeShift modalEvalTime g evalIdx) = modalEvalTime

    After modal eval time shift, the eval time IS the modal's eval time.

    source
    def Semantics.Tense.ModalTense.modalTenseInteraction {Time : Type u_1} [LinearOrder Time] (tenseFeature : Core.Tense.GramTense) (refTime modalEvalTime : Time) :
    Prop

    Klecha's modal-tense interaction: tense constraint checked against the modal's eval time, not against speech time.

    Example: "John might have left"

    • Modal "might" shifts eval time
    • Past "have left" is checked against modal eval time
    • Result: the leaving is past relative to the modal evaluation, not necessarily past relative to speech time
    Equations
    Instances For
      source
      theorem Semantics.Tense.ModalTense.klecha_derives_modal_tense {Time : Type u_1} [LinearOrder Time] (tp : Core.Tense.TensePronoun) (g : Core.Tense.TemporalAssignment Time) (modalEvalTime : Time) (hPast : tp.constraint = Core.Tense.GramTense.past) (hShift : tp.evalTime (modalEvalTimeShift modalEvalTime g tp.evalTimeIndex) = modalEvalTime) (hBefore : tp.resolve (modalEvalTimeShift modalEvalTime g tp.evalTimeIndex) < modalEvalTime) :
      modalTenseInteraction Core.Tense.GramTense.past (tp.resolve (modalEvalTimeShift modalEvalTime g tp.evalTimeIndex)) modalEvalTime

      Klecha derives the modal-tense interaction: past tense under a modal is checked against the modal's eval time.

      This is THE key result: eval time is visible to modals, not just to attitude verbs.

      source
      theorem Semantics.Tense.ModalTense.evalTimeIndex_grounds_klecha {Time : Type u_1} (tp : Core.Tense.TensePronoun) (g : Core.Tense.TemporalAssignment Time) (modalEvalTime : Time) :
      tp.evalTime (modalEvalTimeShift modalEvalTime g tp.evalTimeIndex) = modalEvalTime

      The evalTimeIndex on TensePronoun IS Klecha's mechanism: modals update this index to shift the eval time for embedded tense.