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 3 — Quantificational Event: Event-level. Derives the veridicality asymmetry from quantificational structure (∃∃ for after, ∃∀ for before).

4. Level 4 — Intensional Uniform: World–time pairs with historical alternatives. Uniform earliest operator for both connectives. Derives veridicality from branching time (initial branch point condition).

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

inductive Phenomena.TemporalConnectives.Compare.BeforeAfterTheory : Type

Theories of temporal connective semantics.

• underspecification : BeforeAfterTheory
• ambiguity : BeforeAfterTheory
• quantificationalEvent : BeforeAfterTheory
• intensionalUniform : BeforeAfterTheory

instance Phenomena.TemporalConnectives.Compare.instDecidableEqBeforeAfterTheory : DecidableEq BeforeAfterTheory

Equations

• Phenomena.TemporalConnectives.Compare.instDecidableEqBeforeAfterTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory.repr : BeforeAfterTheory → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory : Repr BeforeAfterTheory

Equations

• Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory = { reprPrec := Phenomena.TemporalConnectives.Compare.instReprBeforeAfterTheory.repr }

def Phenomena.TemporalConnectives.Compare.instBEqBeforeAfterTheory.beq : BeforeAfterTheory → BeforeAfterTheory → Bool

Equations

• Phenomena.TemporalConnectives.Compare.instBEqBeforeAfterTheory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TemporalConnectives.Compare.instBEqBeforeAfterTheory : BEq BeforeAfterTheory

Equations

• Phenomena.TemporalConnectives.Compare.instBEqBeforeAfterTheory = { beq := Phenomena.TemporalConnectives.Compare.instBEqBeforeAfterTheory.beq }

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)

instance Phenomena.TemporalConnectives.Compare.instReprTheoryProfile : Repr TheoryProfile

Equations

• Phenomena.TemporalConnectives.Compare.instReprTheoryProfile = { reprPrec := Phenomena.TemporalConnectives.Compare.instReprTheoryProfile.repr }

def Phenomena.TemporalConnectives.Compare.instReprTheoryProfile.repr : TheoryProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

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.

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.

def Phenomena.TemporalConnectives.Compare.ostProfile : TheoryProfile

O&ST: event-level quantificational asymmetry derives the veridicality contrast directly from the semantics (∃∃ for after, ∃∀ for before).

Equations

• One or more equations did not get rendered due to their size.

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.

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.

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.

theorem Phenomena.TemporalConnectives.Compare.coercion_cost_discriminates : rettPredictsCoercionCost = true

theorem Phenomena.TemporalConnectives.Compare.morphology_discriminates : rettPredictsOvertMorphology = true

theorem Phenomena.TemporalConnectives.Compare.theories_distinct : anscombeProfile.theory ≠ rettProfile.theory

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. O&ST derives it from quantificational asymmetry (∃∃ vs ∃∀); B&C derives it from branching time (initial branch point condition).

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

The four theories form a strict level hierarchy: Anscombe (1) < Rett (2) < O&ST (3) < B&C (4).

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.

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

theorem Phenomena.TemporalConnectives.Compare.telic_after_default_is_finish : Fragments.English.TemporalExpressions.after_.defaultReading = Fragments.English.TemporalExpressions.Reading.afterFinish

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.

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

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.