Documentation

Linglib.Theories.Semantics.Tense.Counterfactual.Defs

Counterfactual past — the two-uses-of-past machinery #

@cite{iatridou-2000}

The structural commitment that past morphology is ambiguous between temporal and counterfactual uses, with only the temporal use subject to the Upper Limit Constraint. Originally proposed by @cite{iatridou-2000} (The Grammatical Ingredients of Counterfactuality); the substrate-side machinery lives here, and @cite{iatridou-2000}'s paper-anchored derivation theorems live in Phenomena/Conditionals/Studies/Iatridou2000.lean.

Core Machinery #

  1. PastMorphologyUse: 2-case enum distinguishing temporal vs counterfactual past morphology.
  2. CounterfactualDistance: world-pair structure for the modal- distance interpretation.
  3. refinedULC: dispatch on PastMorphologyUse — temporal use carries the standard upperLimitConstraint, counterfactual use is exempt (True).

The split between this concept-file and the paper-anchored theorems parallels Tense/SOT/Ambiguity.lean ↔ Studies/Ogihara1996.lean.

source
inductive Semantics.Tense.Counterfactual.PastMorphologyUse :
Type

Two uses of past morphology, following @cite{iatridou-2000}.

Past morphology is ambiguous between:

  1. Temporal precedence (genuine past tense)
  2. Modal remoteness (counterfactual distance from actuality)

@cite{iatridou-2000}'s "exclusion feature": past morphology marks exclusion from the set of relevant times/worlds. Temporal past excludes present times; counterfactual past excludes actual worlds.

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Tense.Counterfactual.instDecidableEqPastMorphologyUse :
    DecidableEq PastMorphologyUse
    Equations
    source
    @[implicit_reducible]
    instance Semantics.Tense.Counterfactual.instReprPastMorphologyUse :
    Repr PastMorphologyUse
    Equations
    source
    def Semantics.Tense.Counterfactual.instReprPastMorphologyUse.repr :
    PastMorphologyUse → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      structure Semantics.Tense.Counterfactual.CounterfactualDistance (World : Type u_1) :
      Type u_1

      Counterfactual distance: past morphology marks modal remoteness, not temporal precedence. The "reference world" is remote from the actual world.

      • actual : World

        The actual world

      • counterfactual : World

        The counterfactual world

      • distinct : self.actual ≠ self.counterfactual

        The worlds are distinct (modal distance > 0)

      Instances For
        source
        def Semantics.Tense.Counterfactual.refinedULC {Time : Type u_1} [LE Time] (use : PastMorphologyUse) (embeddedR matrixE : Time) :
        Prop

        The refined ULC: the upper limit constraint applies only to temporal tense, not to counterfactual tense.

        If the past morphology is temporal, ULC holds (R ≤ E_matrix). If the past morphology is counterfactual, ULC does not apply.

        Equations
        Instances For
          source
          theorem Semantics.Tense.Counterfactual.temporal_has_ulc {Time : Type u_1} [LE Time] (embeddedR matrixE : Time) (h : embeddedR ≤ matrixE) :
          refinedULC PastMorphologyUse.temporal embeddedR matrixE

          Temporal tense is subject to ULC.

          source
          theorem Semantics.Tense.Counterfactual.counterfactual_exempt_from_ulc {Time : Type u_1} [LE Time] (embeddedR matrixE : Time) :
          refinedULC PastMorphologyUse.counterfactual embeddedR matrixE

          Counterfactual tense is exempt from ULC.

          source
          theorem Semantics.Tense.Counterfactual.temporal_ne_counterfactual :
          PastMorphologyUse.temporal ≠ PastMorphologyUse.counterfactual

          The two uses of past morphology are genuinely distinct.