Documentation

Linglib.Phenomena.TemporalConnectives.Compare

Before/After Semantics: Four-Theory Comparison #

@cite{alstott-aravind-2026} @cite{anscombe-1964} @cite{beaver-condoravdi-2003} @cite{ogihara-steinert-threlkeld-2024} @cite{rett-2020} @cite{heinamaki-1974}

Compares four theories of English temporal connectives at different levels of semantic representation:

  1. Level 1 — Under-specification: Point-level. Single lexical entry per connective. Multiple readings from under-specification

    • pragmatic strengthening. No covert aspectual operators.

  2. Level 2 — Ambiguity: Interval-set-level. Strong defaults (before-start, after-finish). Non-default readings require covert INCHOAT or COMPLET operators that incur measurable processing cost.

  3. Level 4 — Intensional Uniform (@cite{beaver-condoravdi-2003}): World–time pairs with historical alternatives. Uniform earliest operator for both connectives. Derives veridicality from branching time (initial branch point condition).

  4. Level 4 — Intensional Revised (@cite{ogihara-steinert-threlkeld-2024}): Extends B&C with eventuality-relative equivalence (≃_{I,e}) and revamped alt(w,I,e). Derives veridicality from the same branching-time architecture but adds CAUSE and event continuation. The ∃∀/∃∃ quantificational asymmetry (from @cite{anscombe-1964}) is employed but is not O&ST's contribution.

Empirical Discriminators #

The theories make identical truth-conditional predictions for all 6 scenario/connective combinations (Table 1 of @cite{rett-2020}). They diverge on:

  1. Processing cost: Rett predicts coercion costs; Anscombe/O&ST/B&C do not
  2. Cross-linguistic morphology: Rett's covert operators have overt reflexes (Tagalog PFV.NEUT/AIA, Serbo-Croatian PFV/IMPF)
  3. NPI licensing mechanism: Anscombe/O&ST from ∀; Rett from Strawson-entailment; B&C from the earliest operator's universal force
  4. Veridicality derivation: O&ST and B&C derive it; Anscombe and Rett stipulate it
source
inductive Phenomena.TemporalConnectives.Compare.BeforeAfterTheory :
Type

Theories of temporal connective semantics.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.TemporalConnectives.Compare.instDecidableEqBeforeAfterTheory :
    DecidableEq BeforeAfterTheory
    Equations
    source
    @[implicit_reducible]
    instance Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory :
    Repr BeforeAfterTheory
    Equations
    source
    def Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory.repr :
    BeforeAfterTheory → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      structure Phenomena.TemporalConnectives.Compare.TheoryProfile :
      Type

      Theory profile: what each theory posits and predicts.

      • theory : BeforeAfterTheory
      • singleLexicalEntry : Bool

        Single lexical entry per connective (vs. default + coerced pair)?

      • positsCoercion : Bool

        Does the theory posit covert aspectual coercion operators?

      • predictsProcessingCost : Bool

        Does the theory predict measurable processing cost for non-default readings?

      • npiMechanism : String

        Mechanism for NPI licensing in before-clauses

      • derivesVeridicality : Bool

        Does the theory derive the veridicality asymmetry from its semantics?

      • level : ℕ

        Level of semantic representation (1 = point, 2 = interval, 3 = event, 4 = intensional)

      Instances For
        source
        def Phenomena.TemporalConnectives.Compare.instReprTheoryProfile.repr :
        TheoryProfile → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Phenomena.TemporalConnectives.Compare.instReprTheoryProfile :
          Repr TheoryProfile
          Equations
          source
          def Phenomena.TemporalConnectives.Compare.anscombeProfile :
          TheoryProfile

          Anscombe/Krifka: single entry, no coercion, NPIs from ∀ + strong alternatives.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Phenomena.TemporalConnectives.Compare.rettProfile :
            TheoryProfile

            Rett: dual entries via coercion, processing cost predicted, NPIs from Strawson-entailment of the strong default reading.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.TemporalConnectives.Compare.ostProfile :
              TheoryProfile

              O&ST: extends B&C's intensional framework with eventuality-relative equivalence (≃_{I,e}) and revamped alt(w,I,e). Derives veridicality from branching time + event continuation, with CAUSE mediating the non-veridical reading. The quantificational asymmetry (∃∀ vs ∃∃) comes from @cite{anscombe-1964}, not from O&ST's own contribution.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Phenomena.TemporalConnectives.Compare.bcProfile :
                TheoryProfile

                B&C: uniform analysis with earliest across historical alternatives. Veridicality derived from branching time (initial branch point condition), not from quantificational asymmetry. Single lexical entry per connective.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Phenomena.TemporalConnectives.Compare.rettPredictsCoercionCost :
                  Bool

                  Rett predicts processing cost for non-default readings; Anscombe does not. This is the core empirical discriminator tested by @cite{alstott-aravind-2026}. Completive coercion (Exps 1b, 2), inchoative in after-clauses (Exp 4), and cross-linguistic morphology all support the coercion account.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Phenomena.TemporalConnectives.Compare.rettPredictsOvertMorphology :
                    Bool

                    Rett posits covert operators with cross-linguistic morphological reflexes (Tagalog PFV.NEUT/AIA, Serbo-Croatian PFV/IMPF). Anscombe does not.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem Phenomena.TemporalConnectives.Compare.coercion_cost_discriminates :
                      rettPredictsCoercionCost = true
                      source
                      theorem Phenomena.TemporalConnectives.Compare.morphology_discriminates :
                      rettPredictsOvertMorphology = true
                      source
                      theorem Phenomena.TemporalConnectives.Compare.theories_distinct :
                      anscombeProfile.theory ≠ rettProfile.theory
                      source
                      theorem Phenomena.TemporalConnectives.Compare.veridicality_derivation :
                      ostProfile.derivesVeridicality = true ∧ bcProfile.derivesVeridicality = true ∧ anscombeProfile.derivesVeridicality = false ∧ rettProfile.derivesVeridicality = false

                      O&ST and B&C both derive veridicality; Anscombe and Rett do not. Both O&ST and B&C derive it from branching time; O&ST additionally uses eventuality-relative equivalence and CAUSE.

                      source
                      theorem Phenomena.TemporalConnectives.Compare.level_hierarchy :
                      anscombeProfile.level < rettProfile.level ∧ rettProfile.level < bcProfile.level ∧ ostProfile.level = bcProfile.level

                      The theories span three levels: Anscombe (1) < Rett (2) < B&C = O&ST (4). B&C and O&ST are both Level 4 (intensional with branching time); O&ST extends B&C with eventuality-relative equivalence.

                      source
                      theorem Phenomena.TemporalConnectives.Compare.all_theories_distinct :
                      anscombeProfile.theory ≠ rettProfile.theory ∧ anscombeProfile.theory ≠ ostProfile.theory ∧ anscombeProfile.theory ≠ bcProfile.theory ∧ rettProfile.theory ≠ ostProfile.theory ∧ rettProfile.theory ≠ bcProfile.theory ∧ ostProfile.theory ≠ bcProfile.theory

                      All four theories are distinct.

                      source
                      theorem Phenomena.TemporalConnectives.Compare.stative_before_default_is_start :
                      Fragments.English.TemporalExpressions.before_.defaultReading = Fragments.English.TemporalExpressions.Reading.beforeStart

                      Both theories make identical truth-conditional predictions for all 6 scenario types in @cite{rett-2020}'s Table 1. They diverge only on processing predictions and cross-linguistic morphology.

                      The 6 scenarios:

                      1. process EE + before → ≺ initial
                      2. culmination EE + before → ≺ initial OR ≺ final
                      3. process EE + after → ≻ initial OR ≻ final
                      4. culmination EE + after → ≻ final
                      5. Stative EE + before → ≺ initial
                      6. Stative EE + after → ≻ initial OR ≻ final

                      The theory-level agreement proofs for the unambiguous cases (scenarios 1, 4) are in TemporalConnectives.anscombe_rett_agree_stative_before_start and rett_implies_anscombe_telic_after_finish (one-directional: the ↔ is false because Anscombe only requires some B-time to precede A, while Rett requires A after B's finish).

                      source
                      theorem Phenomena.TemporalConnectives.Compare.telic_after_default_is_finish :
                      Fragments.English.TemporalExpressions.after_.defaultReading = Fragments.English.TemporalExpressions.Reading.afterFinish
                      source
                      theorem Phenomena.TemporalConnectives.Compare.npi_asymmetry :
                      Fragments.English.TemporalExpressions.before_.licensesNPI = true ∧ Fragments.English.TemporalExpressions.after_.licensesNPI = false

                      The Fragment entries correctly reflect the universal NPI asymmetry: before licenses NPIs, after does not.

                      source
                      theorem Phenomena.TemporalConnectives.Compare.both_universal :
                      Fragments.English.TemporalExpressions.before_.crossLinguisticBasic = true ∧ Fragments.English.TemporalExpressions.after_.crossLinguisticBasic = true

                      Both connectives are cross-linguistically basic (attested in all 17 languages of Rett's typological survey).

                      source
                      theorem Phenomena.TemporalConnectives.Compare.both_telicity_sensitive :
                      Fragments.English.TemporalExpressions.before_.embeddedTelicityEffect = true ∧ Fragments.English.TemporalExpressions.after_.embeddedTelicityEffect = true

                      The before/after asymmetry is reflected in telicity sensitivity: both are sensitive to embedded clause telicity.