Documentation

Linglib.Theories.Semantics.Tense.SOT.Ambiguity

Past-tense ambiguity (concept-level) #

@cite{ogihara-1996}

The structural commitment that past tense morphology in embedded contexts is ambiguous between a genuine-past reading (temporal precedence) and a zero-tense reading (bound variable, no independent temporal content). Originally proposed by @cite{ogihara-1996}; rejected by @cite{kratzer-1998} (who treats past as never ambiguous, with the simultaneous reading deriving from deletion at LF) and finessed by @cite{klecha-2016} (who derives the simultaneous reading from modal-base × tense composition without past-tense ambiguity).

This file carries the type-level commitment (the 2-case enum). The paper-attributed theorems and the Ogihara-vs-Kratzer divergence claim live in Phenomena/TenseAspect/Studies/Ogihara1996.lean.

Mathlib analogue: this is a Mathlib/Order/SuccPred/Basic.lean-style substrate — orders that aren't successor-preorders simply don't import it; theories that don't share Ogihara's ambiguity thesis simply don't import this file.

source
inductive Semantics.Tense.SOT.Ambiguity.PastReading :
Type

Two readings of past morphology in embedded contexts (Ogihara).

  • genuinePast : PastReading

    Genuine past: temporal precedence (R < eval time).

  • zeroTense : PastReading

    Zero tense: bound variable, no independent temporal content.

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Tense.SOT.Ambiguity.instDecidableEqPastReading :
    DecidableEq PastReading
    Equations
    source
    def Semantics.Tense.SOT.Ambiguity.instReprPastReading.repr :
    PastReading → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Tense.SOT.Ambiguity.instReprPastReading :
      Repr PastReading
      Equations
      source
      def Semantics.Tense.SOT.Ambiguity.pastUnderPastReadings :
      List PastReading

      Both readings are available for past-under-past in SOT languages.

      Equations
      Instances For
        source
        theorem Semantics.Tense.SOT.Ambiguity.genuinePast_ne_zeroTense :
        PastReading.genuinePast ≠ PastReading.zeroTense

        Structural distinctness of the two readings. The theoretical significance of the distinction (i.e., that this is the Ogihara-vs-Kratzer divide) is in the Studies file.