Documentation

Linglib.Theories.Semantics.Tense.CounterfactualTense

@cite{deal-2020}: Counterfactual Tense and the Upper Limit Constraint #

@cite{deal-2020} @cite{iatridou-2000}

Deal's theory: past morphology in counterfactuals encodes modal distance, not temporal precedence. This explains why counterfactual "were" does not locate events in the past ("If I were rich..." is about the present).

Core Mechanisms #

  1. Counterfactual distance: past morphology marks modal remoteness from actuality, not temporal precedence
  2. ULC refinement: the Upper Limit Constraint holds for temporal tense but not for counterfactual tense (which is not truly temporal)

Key Innovation #

Abusch's ULC says embedded R ≤ matrix E. But counterfactuals violate this: "If I were rich, I would buy a house" — the "were" does not refer to a time before the attitude event. Deal resolves this by distinguishing temporal tense (subject to ULC) from counterfactual tense (exempt from ULC).

source
inductive Semantics.Tense.CounterfactualTense.PastMorphologyUse :
Type

The 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)

Iatridou'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
    instance Semantics.Tense.CounterfactualTense.instDecidableEqPastMorphologyUse :
    DecidableEq PastMorphologyUse
    Equations
    source
    instance Semantics.Tense.CounterfactualTense.instReprPastMorphologyUse :
    Repr PastMorphologyUse
    Equations
    source
    def Semantics.Tense.CounterfactualTense.instReprPastMorphologyUse.repr :
    PastMorphologyUse → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Semantics.Tense.CounterfactualTense.instBEqPastMorphologyUse.beq :
      PastMorphologyUse → PastMorphologyUse → Bool
      Equations
      Instances For
        source
        instance Semantics.Tense.CounterfactualTense.instBEqPastMorphologyUse :
        BEq PastMorphologyUse
        Equations
        source
        structure Semantics.Tense.CounterfactualTense.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.CounterfactualTense.refinedULC {Time : Type u_1} [LE Time] (use : PastMorphologyUse) (embeddedR matrixE : Time) :
          Prop

          Deal's 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.CounterfactualTense.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.CounterfactualTense.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.CounterfactualTense.deal_counterfactual_overrides_ulc {Time : Type u_1} [LinearOrder Time] (embeddedR matrixE : Time) (h_forward : embeddedR > matrixE) :
            refinedULC PastMorphologyUse.counterfactual embeddedR matrixE

            Deal derives the counterfactual override: counterfactual morphology is not subject to the ULC, because it doesn't encode temporal precedence.

            source
            theorem Semantics.Tense.CounterfactualTense.deal_refines_ulc {Time : Type u_1} [LinearOrder Time] (embeddedR matrixE : Time) (h_forward : embeddedR > matrixE) :
            ¬refinedULC PastMorphologyUse.temporal embeddedR matrixE ∧ refinedULC PastMorphologyUse.counterfactual embeddedR matrixE

            Deal refines the ULC: it holds for temporal tense but not for counterfactual tense. The temporal and counterfactual uses of past morphology have different formal properties.

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

            The two uses of past morphology are genuinely distinct: temporal tense ≠ counterfactual tense.