@cite{rett-2020}: Antonymy + Aspectual Coercion

@cite{rett-2020} @cite{rett-2026} @cite{jin-koenig-2021} @cite{krifka-2010b}before and after are antonyms on converse scales, with strong defaults @cite{de-swart-1998} @cite{dolling-2014} (before-start, after-finish). Non-default readings require aspectual coercion: INCHOAT (GLB, atelic → onset) or COMPLET (LUB, telic → telos), which incur processing cost.

Rett's formal analysis (eqs. 22a-b):

• ⟦A before B⟧ = ∃t ∈ A [t ≺ MAX(B_≺)]
• ⟦A after B⟧ = ∃t ∈ A [t ≻ MAX(B_≻)]

Both theories use ∃ over the main clause A: "some time in A bears the relation to (some characterization) B." They differ in how B's reference point is selected (all of B vs MAX of B).

Level

Level 2 (interval sets): operates on SentDenotation directly, using maxOnScale from Core.Scale to select the informative bound.

Bridges

• INCHOAT extracts the same point as CoSType.inception (onset of a state)
• COMPLET extracts the dual: the finish point of a telic event
• stativeDenotation has the subinterval property (connects to Krifka CUM)
• Both theories agree on unambiguous cases (stative before, telic after)

Ambidirectionality

before is truth-conditionally insensitive to negation of its argument (ambidirectional), which is why it licenses expletive negation cross- linguistically. after and while are not ambidirectional.

def Semantics.Tense.TemporalConnectives.Rett.before {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Rett's before (eq. 22a): ∃t ∈ times(A) [t ≺ MAX(times(B)_≺)]. Some time in A precedes the maximal (on the ≺ scale) time of B.

Equations

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

def Semantics.Tense.TemporalConnectives.Rett.after {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Rett's after (eq. 22b): ∃t ∈ times(A) [t ≻ MAX(times(B)_≻)]. Some time in A succeeds the maximal (on the ≻ scale) time of B.

Equations

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

def Semantics.Tense.TemporalConnectives.INCHOAT {Time : Type u_1} [LinearOrder Time] (p : SentDenotation Time) : SentDenotation Time

Inchoative coercion / GLB (@cite{rett-2020}, eq. 19; @cite{de-swart-1998}; @cite{dolling-2014}). Maps a process (atelic) denotation to a singleton containing its onset point. GLB(T) = ιt[t ∈ T ∧ ∀t' ∈ T, t ≤ t']

Linguistically: "Amy was surprised" → "the start of Amy being surprised". Cross-linguistically realized as inchoative morphology (Russian -sja, Tagalog PFV.NEUT).

Equations

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

def Semantics.Tense.TemporalConnectives.COMPLET {Time : Type u_1} [LinearOrder Time] (p : SentDenotation Time) : SentDenotation Time

Completive coercion / LUB (@cite{rett-2020}, eq. 21; @cite{dolling-2014}). Maps a culmination (telic) denotation to a singleton containing its telos. LUB(T) = ιt[t ∈ T ∧ ∀t' ∈ T, t ≥ t']

Linguistically: "Jane climbed the mountain" → "the moment Jane reached the top". Cross-linguistically realized as completive morphology (Tagalog AIA).

Equations

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

theorem Semantics.Tense.TemporalConnectives.inchoat_bridges_inception {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : INCHOAT (stativeDenotation i) = {j : Core.Time.Interval Time | j = Core.Time.Interval.point i.start}

INCHOAT extracts the start point of a stative denotation.

theorem Semantics.Tense.TemporalConnectives.complet_bridges_cessation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : COMPLET (accomplishmentDenotation i) = {j : Core.Time.Interval Time | j = Core.Time.Interval.point i.finish}

COMPLET extracts the finish point of an accomplishment denotation.

theorem Semantics.Tense.TemporalConnectives.anscombe_rett_agree_stative_before_start {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : Core.Time.Interval Time) : Anscombe.before A (stativeDenotation i_B) ↔ Rett.before A (stativeDenotation i_B)

Both theories predict "before-start" for statives.

When B is stative (subinterval-closed), both theories reduce to "some time in A precedes all times in B":

• Anscombe directly: ∃ t ∈ A, ∀ t' ∈ B, t < t'
• Rett: ∃ t ∈ A, t < MAX(B_≺). For statives, MAX on ≺ picks B.start (the GLB), and t < B.start ↔ t < all times in B.

theorem Semantics.Tense.TemporalConnectives.rett_implies_anscombe_telic_after_finish {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : Core.Time.Interval Time) : Rett.after A (accomplishmentDenotation i_B) → Anscombe.after A (accomplishmentDenotation i_B)

Rett's analysis implies Anscombe's for telic "after".

The converse does NOT hold: Anscombe.after only requires some point of B to precede some point of A (∃ t' ∈ B, t' < t), while Rett requires A to follow B's finish (t > MAX₍>₎(B) = i_B.finish). These differ when A overlaps B without extending past B's endpoint.

theorem Semantics.Tense.TemporalConnectives.rett_before_implies_anscombe {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Rett.before A B → Anscombe.before A B

Rett's before implies Anscombe's before in general.

From Rett: t < m where m = min(timeTrace B). Since m < all other points in timeTrace B (by maxOnScale), t < every point in timeTrace B. This gives Anscombe's ∀-quantified conclusion.

theorem Semantics.Tense.TemporalConnectives.rett_after_implies_anscombe {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Rett.after A B → Anscombe.after A B

Rett's after implies Anscombe's after in general.

Immediate: m ∈ maxOnScale(timeTrace B) implies m ∈ timeTrace B, and t > m gives the existential witness for Anscombe.after.

Expletive negation and ambidirectionality

@cite{rett-2026} shows that before is ambidirectional: negating B in "A before B" doesn't change truth conditions. This is why before-clauses license expletive negation cross-linguistically (@cite{jin-koenig-2021}: 50 of 74 EN-attesting languages, from a 722-language survey).

The mechanism: for B = [s, f], both B and its pre-event complement (−∞, s] share s as their "most informative closed bound" on the < scale. The before construction relates A only to this bound, so negating B is truth-conditionally vacuous.

After is NOT ambidirectional: negating B shifts the relevant bound. While requires total temporal overlap; ¬B fails when A overlaps B.

theorem Semantics.Tense.TemporalConnectives.before_determined_by_max {Time : Type u_1} [LinearOrder Time] (A B₁ B₂ : SentDenotation Time) (h : Core.Scale.maxOnScale (fun (x1 x2 : Time) => x1 < x2) (timeTrace B₁) = Core.Scale.maxOnScale (fun (x1 x2 : Time) => x1 < x2) (timeTrace B₂)) : Rett.before A B₁ ↔ Rett.before A B₂

Before truth conditions depend only on MAX₍<₎ of B's time trace.

theorem Semantics.Tense.TemporalConnectives.rett_before_closedTrace_eq {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (s f : Time) (hsf : s ≤ f) (htrace : timeTrace B = {t : Time | s ≤ t ∧ t ≤ f}) : Rett.before A B ↔ ∃ t ∈ timeTrace A, t < s

When B's time trace is a closed interval [s, f], Rett.before reduces to "∃ t ∈ A, t < s".

theorem Semantics.Tense.TemporalConnectives.complet_stative {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : COMPLET (stativeDenotation i) = {j : Core.Time.Interval Time | j = Core.Time.Interval.point i.finish}

COMPLET on a stative denotation extracts the finish point.

def Semantics.Tense.TemporalConnectives.preEventDenotation {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : Core.Time.Interval Time) (hbot : bot ≤ i.start) : SentDenotation Time

The pre-event complement of an event interval [s, f].

Equations

• Semantics.Tense.TemporalConnectives.preEventDenotation bot i hbot = Semantics.Tense.TemporalConnectives.stativeDenotation { start := bot, finish := i.start, valid := hbot }

theorem Semantics.Tense.TemporalConnectives.timeTrace_stative_closedInterval {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : timeTrace (stativeDenotation i) = {t : Time | i.start ≤ t ∧ t ≤ i.finish}

The time trace of a stative denotation is the closed interval [start, finish].

theorem Semantics.Tense.TemporalConnectives.maxOnScale_lt_stative {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : Core.Scale.maxOnScale (fun (x1 x2 : Time) => x1 < x2) (timeTrace (stativeDenotation i)) = {i.start}

MAX₍<₎ of a stative denotation's time trace is {start}.

theorem Semantics.Tense.TemporalConnectives.timeTrace_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : Core.Time.Interval Time) (hbot : bot ≤ i.start) : timeTrace (COMPLET (preEventDenotation bot i hbot)) = {t : Time | i.start ≤ t ∧ t ≤ i.start}

The time trace of COMPLET(preEventDenotation bot i) is the degenerate interval {i.start}.

theorem Semantics.Tense.TemporalConnectives.maxOnScale_lt_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : Core.Time.Interval Time) (hbot : bot ≤ i.start) : Core.Scale.maxOnScale (fun (x1 x2 : Time) => x1 < x2) (timeTrace (COMPLET (preEventDenotation bot i hbot))) = {i.start}

MAX₍<₎ of the COMPLET of a pre-event denotation is {start}.

theorem Semantics.Tense.TemporalConnectives.before_preEvent_ambidirectional {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : Core.Time.Interval Time) (bot : Time) (hbot : bot ≤ i_B.start) : Rett.before A (stativeDenotation i_B) ↔ Rett.before A (COMPLET (preEventDenotation bot i_B hbot))

Before is truth-conditionally insensitive to event polarity.

Both select the same boundary point s through different mechanisms: the original uses the default before-start reading (MAX₍<₎), while the negated version requires COMPLET coercion to extract the end of the pre-event interval.

theorem Semantics.Tense.TemporalConnectives.after_not_ambidirectional {Time : Type u_1} [LinearOrder Time] (hab : ∃ (a : Time) (b : Time), a < b) : ¬∀ (A : SentDenotation Time) (B : Set Time), Core.Scale.isAmbidirectional (fun (X : Set Time) => ∃ t ∈ timeTrace A, ∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : Time) => x1 > x2) X, t > m) B

After is NOT ambidirectional: negating B changes truth conditions because MAX₍>₎(B) ≠ MAX₍>₎(¬B).

theorem Semantics.Tense.TemporalConnectives.while_not_ambidirectional {Time : Type u_1} [Inhabited Time] : ¬∀ (A B : Set Time), Core.Scale.isAmbidirectional (fun (X : Set Time) => ∀ t ∈ A, t ∈ X) B

While is not ambidirectional.