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

Temporal Connective Truth-Condition Examples

@cite{heinamaki-1974} @cite{rett-2020} @cite{karttunen-1974}

Concrete scenarios verifying that the Anscombe, Rett, and Karttunen formalizations produce correct truth-value judgments.

Scenarios 1–6 verify @cite{rett-2020} Table 1 for before/after. Scenarios 7–10 verify @cite{heinamaki-1974} Chs. 6, 8, 9 for since, by, till.

Scenarios (ℕ time points)

#	ME	EE	Connective	Result
1	point(1)	stative [5,10]	before	True
2	point(12)	stative [5,10]	after	True
3	point(1)	accomplishment [3,8]	before	True
4	point(12)	accomplishment [3,8]	after	True
5	point(7)	stative [5,10]	before	False
6	point(7)	stative [5,10]	after	False
7	stative[5,10]	point(5)	since	True
8	point(1)	point(3)	by	True
9	point(3)	point(3)	by	True
9'	point(3)	point(3)	before	False
10	stative[5,10]	point(5)	till	True

def Phenomena.TemporalConnectives.Examples.me_early : Core.Time.Interval ℕ

ME: "John left" — punctual event at time 1 (early).

Equations

• Phenomena.TemporalConnectives.Examples.me_early = Core.Time.Interval.point 1

def Phenomena.TemporalConnectives.Examples.me_late : Core.Time.Interval ℕ

ME: "John left" — punctual event at time 12 (late).

Equations

• Phenomena.TemporalConnectives.Examples.me_late = Core.Time.Interval.point 12

def Phenomena.TemporalConnectives.Examples.me_inside : Core.Time.Interval ℕ

ME: punctual event at time 7 (inside the stative EE).

Equations

• Phenomena.TemporalConnectives.Examples.me_inside = Core.Time.Interval.point 7

def Phenomena.TemporalConnectives.Examples.ee_stative : Core.Time.Interval ℕ

EE: "she was president" — stative, running [5, 10].

Equations

• Phenomena.TemporalConnectives.Examples.ee_stative = { start := 5, finish := 10, valid := Phenomena.TemporalConnectives.Examples.ee_stative._proof_2 }

def Phenomena.TemporalConnectives.Examples.ee_accomplishment : Core.Time.Interval ℕ

EE: "she climbed the mountain" — accomplishment, [3, 8].

Equations

• Phenomena.TemporalConnectives.Examples.ee_accomplishment = { start := 3, finish := 8, valid := Phenomena.TemporalConnectives.Examples.ee_accomplishment._proof_2 }

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_early : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_early = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_early

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_late : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_late = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_late

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_inside : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_inside = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_inside

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.B_stative : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.B_stative = Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TemporalConnectives.Examples.ee_stative

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.B_telic : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.B_telic = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.ee_accomplishment

theorem Phenomena.TemporalConnectives.Examples.scenario1_anscombe : Semantics.Tense.TemporalConnectives.Anscombe.before A_early B_stative

"John left₁ before she was president₅₋₁₀" — True under Anscombe. Witness: t = 1 ∈ ME, and 1 < all t' ∈ [5, 10].

theorem Phenomena.TemporalConnectives.Examples.scenario1_rett : Semantics.Tense.TemporalConnectives.Rett.before A_early B_stative

"John left₁ before she was president₅₋₁₀" — True under Rett. Witness: t = 1, m = 5 (the GLB of [5, 10] on the ≺ scale).

theorem Phenomena.TemporalConnectives.Examples.scenario2_anscombe : Semantics.Tense.TemporalConnectives.Anscombe.after A_late B_stative

"John left₁₂ after she was president₅₋₁₀" — True under Anscombe. Witness: t = 12, t' = 5 (any point in EE suffices).

theorem Phenomena.TemporalConnectives.Examples.scenario2_rett : Semantics.Tense.TemporalConnectives.Rett.after A_late B_stative

"John left₁₂ after she was president₅₋₁₀" — True under Rett. Witness: t = 12, m = 10 (the LUB of [5, 10] on the ≻ scale).

theorem Phenomena.TemporalConnectives.Examples.scenario3_anscombe : Semantics.Tense.TemporalConnectives.Anscombe.before A_early B_telic

"John met Mary₁ before she climbed the mountain₃₋₈" — True under Anscombe. Witness: t = 1, and 1 < all t' in [3, 8].

theorem Phenomena.TemporalConnectives.Examples.scenario3_rett : Semantics.Tense.TemporalConnectives.Rett.before A_early B_telic

"John met Mary₁ before she climbed the mountain₃₋₈" — True under Rett. Witness: t = 1, m = 3 (the GLB of [3, 8] on the ≺ scale).

theorem Phenomena.TemporalConnectives.Examples.scenario4_anscombe : Semantics.Tense.TemporalConnectives.Anscombe.after A_late B_telic

"John met Mary₁₂ after she climbed the mountain₃₋₈" — True under Anscombe. Witness: t = 12, t' = 3.

theorem Phenomena.TemporalConnectives.Examples.scenario4_rett : Semantics.Tense.TemporalConnectives.Rett.after A_late B_telic

"John met Mary₁₂ after she climbed the mountain₃₋₈" — True under Rett. Witness: t = 12, m = 8 (the LUB of [3, 8] on the ≻ scale).

theorem Phenomena.TemporalConnectives.Examples.scenario5_anscombe_false : ¬Semantics.Tense.TemporalConnectives.Anscombe.before A_inside B_stative

"John left₇ before she was president₅₋₁₀" — False under Anscombe. Any witness t from ME (t=7) fails: t'=7 ∈ EE and ¬(7 < 7).

theorem Phenomena.TemporalConnectives.Examples.scenario6_rett_false : ¬Semantics.Tense.TemporalConnectives.Rett.after A_inside B_stative

"John left₇ after she was president₅₋₁₀" — False under Rett. The max on the ≻ scale is 10, and ¬(7 > 10).

theorem Phenomena.TemporalConnectives.Examples.scenario1_agree : Semantics.Tense.TemporalConnectives.Anscombe.before A_early B_stative ∧ Semantics.Tense.TemporalConnectives.Rett.before A_early B_stative

Both theories agree on scenario 1 (ME before stative EE).

theorem Phenomena.TemporalConnectives.Examples.scenario2_agree : Semantics.Tense.TemporalConnectives.Anscombe.after A_late B_stative ∧ Semantics.Tense.TemporalConnectives.Rett.after A_late B_stative

Both theories agree on scenario 2 (ME after stative EE).

theorem Phenomena.TemporalConnectives.Examples.scenario3_agree : Semantics.Tense.TemporalConnectives.Anscombe.before A_early B_telic ∧ Semantics.Tense.TemporalConnectives.Rett.before A_early B_telic

Both theories agree on scenario 3 (ME before accomplishment EE).

theorem Phenomena.TemporalConnectives.Examples.scenario4_agree : Semantics.Tense.TemporalConnectives.Anscombe.after A_late B_telic ∧ Semantics.Tense.TemporalConnectives.Rett.after A_late B_telic

Both theories agree on scenario 4 (ME after accomplishment EE).

theorem Phenomena.TemporalConnectives.Examples.inchoat_stative_ee : Semantics.Tense.TemporalConnectives.INCHOAT B_stative = {j : Core.Time.Interval ℕ | j = Core.Time.Interval.point 5}

INCHOAT of "she was president₅₋₁₀" = {point(5)}. Verifies that inchoative coercion extracts the onset.

theorem Phenomena.TemporalConnectives.Examples.complet_telic_ee : Semantics.Tense.TemporalConnectives.COMPLET B_telic = {j : Core.Time.Interval ℕ | j = Core.Time.Interval.point 8}

COMPLET of "she climbed the mountain₃₋₈" = {point(8)}. Verifies that completive coercion extracts the telos.

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_stative : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

ME: stative [5, 10] — "He has been happy."

Equations

• Phenomena.TemporalConnectives.Examples.A_stative = Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TemporalConnectives.Examples.ee_stative

def Phenomena.TemporalConnectives.Examples.ee_onset : Core.Time.Interval ℕ

EE: punctual event at time 5 — "she arrived."

Equations

• Phenomena.TemporalConnectives.Examples.ee_onset = Core.Time.Interval.point 5

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.B_onset : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.B_onset = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.ee_onset

def Phenomena.TemporalConnectives.Examples.me_at_deadline : Core.Time.Interval ℕ

ME: punctual event at time 3 — "arrived at 3pm" (for by coincidence case).

Equations

• Phenomena.TemporalConnectives.Examples.me_at_deadline = Core.Time.Interval.point 3

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_at_deadline : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_at_deadline = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_at_deadline

def Phenomena.TemporalConnectives.Examples.ee_deadline : Core.Time.Interval ℕ

EE: punctual event at time 3 — "3pm" (deadline).

Equations

• Phenomena.TemporalConnectives.Examples.ee_deadline = Core.Time.Interval.point 3

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.B_deadline : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.B_deadline = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.ee_deadline

theorem Phenomena.TemporalConnectives.Examples.scenario_since : Semantics.Tense.TemporalConnectives.Karttunen.since A_stative B_onset

"He has been happy₅₋₁₀ since she arrived₅" — True under Karttunen.since. Witness: t = 5 ∈ B, and ∀t' ∈ A (i.e., 5 ≤ t' ≤ 10), 5 ≤ t'.

theorem Phenomena.TemporalConnectives.Examples.scenario_since_veridical : Semantics.Tense.TemporalConnectives.Karttunen.since A_stative B_onset → ∃ (t : ℕ), t ∈ Semantics.Tense.TemporalConnectives.timeTrace B_onset

Since is veridical for its complement in scenario: she arrived.

theorem Phenomena.TemporalConnectives.Examples.scenario_by_strict : Semantics.Tense.TemporalConnectives.Karttunen.by_ A_early B_deadline

"He arrived₁ by 3pm₃" — True under Karttunen.by_. Witness: t = 1 ∈ A, and ∀t' ∈ B (t' = 3), 1 ≤ 3.

theorem Phenomena.TemporalConnectives.Examples.scenario_by_coincidence : Semantics.Tense.TemporalConnectives.Karttunen.by_ A_at_deadline B_deadline

"He arrived₃ by 3pm₃" — True under Karttunen.by_. Witness: t = 3 ∈ A, 3 ≤ 3 (coincidence allowed).

theorem Phenomena.TemporalConnectives.Examples.scenario_before_coincidence_false : ¬Semantics.Tense.TemporalConnectives.Anscombe.before A_at_deadline B_deadline

"He arrived₃ before 3pm₃" — FALSE under Anscombe.before. Need 3 < 3, which fails. Shows by ⊋ before.

theorem Phenomena.TemporalConnectives.Examples.by_without_before : Semantics.Tense.TemporalConnectives.Karttunen.by_ A_at_deadline B_deadline ∧ ¬Semantics.Tense.TemporalConnectives.Anscombe.before A_at_deadline B_deadline

By but not before on the same scenario: demonstrates the strict weakening from before_implies_by.

theorem Phenomena.TemporalConnectives.Examples.scenario_till : Semantics.Tense.TemporalConnectives.Karttunen.till A_stative B_onset

"He slept₅₋₁₀ till she arrived₅" — True under Karttunen.till. Witness: t = 5 ∈ both time traces (overlap).

theorem Phenomena.TemporalConnectives.Examples.till_matches_until_scenario : Semantics.Tense.TemporalConnectives.Karttunen.till A_stative B_onset ↔ Semantics.Tense.TemporalConnectives.Karttunen.until A_stative B_onset

Till agrees with until on the same scenario (definitional).

Not...until scenarios

Karttunen's identity: punctual until = ¬before (eq. 33). We verify this on concrete time points.

#	ME	EE	Construction	Result
11	point(3)	point(5)	not...until	True
12	point(3)	point(5)	presup + assert	when
13	point(7)	point(5)	not...until	False

def Phenomena.TemporalConnectives.Examples.me_wake_early : Core.Time.Interval ℕ

ME: "The princess woke up" — punctual event at time 3 (early).

Equations

• Phenomena.TemporalConnectives.Examples.me_wake_early = Core.Time.Interval.point 3

def Phenomena.TemporalConnectives.Examples.ee_kiss : Core.Time.Interval ℕ

EE: "The prince kissed her" — punctual event at time 5.

Equations

• Phenomena.TemporalConnectives.Examples.ee_kiss = Core.Time.Interval.point 5

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_wake_early : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_wake_early = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_wake_early

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.B_kiss : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.B_kiss = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.ee_kiss

theorem Phenomena.TemporalConnectives.Examples.scenario11_before_true : Semantics.Tense.TemporalConnectives.Anscombe.before A_wake_early B_kiss

Scenario 11: "The princess woke up₃ before the prince kissed her₅" — TRUE. 3 < 5. This is the base before that gets negated in punctual until.

theorem Phenomena.TemporalConnectives.Examples.scenario11_notUntil_false : ¬Semantics.Tense.TemporalConnectives.Karttunen.notUntil A_wake_early B_kiss

Scenario 11': "The princess didn't wake up₃ until the prince kissed her₅" — FALSE. NOT(BEFORE) = NOT(wake₃ before kiss₅) = ¬(3 < 5) = False. The princess DID wake up before the kiss, so "not until" is false.

def Phenomena.TemporalConnectives.Examples.me_wake_at_kiss : Core.Time.Interval ℕ

ME: "The princess woke up" — punctual event at time 5 (AT the kiss).

Equations

• Phenomena.TemporalConnectives.Examples.me_wake_at_kiss = Core.Time.Interval.point 5

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_wake_at : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_wake_at = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_wake_at_kiss

theorem Phenomena.TemporalConnectives.Examples.scenario12_notUntil_true : Semantics.Tense.TemporalConnectives.Karttunen.notUntil A_wake_at B_kiss

Scenario 12: "The princess didn't wake up₅ until the prince kissed her₅" — TRUE. NOT(BEFORE) = NOT(wake₅ before kiss₅) = ¬(5 < 5) = True. She woke up at exactly the time of the kiss.

theorem Phenomena.TemporalConnectives.Examples.scenario12_presupposition : Semantics.Tense.TemporalConnectives.Anscombe.before A_wake_at B_kiss ∨ Semantics.Tense.TemporalConnectives.Karttunen.when_ A_wake_at B_kiss

Scenario 12': Presupposition (wake₅ before kiss₅ ∨ wake₅ when kiss₅) is satisfied: the waking happens at the kiss time (when), so the left disjunct is false but the right is true.

theorem Phenomena.TemporalConnectives.Examples.scenario12_derives_when : Semantics.Tense.TemporalConnectives.Karttunen.when_ A_wake_at B_kiss

Scenario 12'': Presupposition + assertion → when (disjunctive syllogism). This is Karttunen's key result: "not until" + presupposition derives "when".

def Phenomena.TemporalConnectives.Examples.me_wake_late : Core.Time.Interval ℕ

ME: "The princess woke up" — punctual event at time 7 (AFTER the kiss).

Equations

• Phenomena.TemporalConnectives.Examples.me_wake_late = Core.Time.Interval.point 7

@[reducible, inline]

abbrev Phenomena.TemporalConnectives.Examples.A_wake_late : Semantics.Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Phenomena.TemporalConnectives.Examples.A_wake_late = Semantics.Tense.TemporalConnectives.accomplishmentDenotation Phenomena.TemporalConnectives.Examples.me_wake_late

theorem Phenomena.TemporalConnectives.Examples.scenario13_notUntil_true : Semantics.Tense.TemporalConnectives.Karttunen.notUntil A_wake_late B_kiss

Scenario 13: "The princess didn't wake up₇ until the prince kissed her₅" — TRUE. NOT(BEFORE) = NOT(wake₇ before kiss₅) = ¬(7 < 5) = True. She woke up after the kiss, so she didn't wake up before it.

theorem Phenomena.TemporalConnectives.Examples.scenario13_not_when : ¬Semantics.Tense.TemporalConnectives.Karttunen.when_ A_wake_late B_kiss

Scenario 13': wake₇ is NOT when kiss₅ (no overlap at any time point).

theorem Phenomena.TemporalConnectives.Examples.scenario13_presup_fails : ¬(Semantics.Tense.TemporalConnectives.Anscombe.before A_wake_late B_kiss ∨ Semantics.Tense.TemporalConnectives.Karttunen.when_ A_wake_late B_kiss)

Scenario 13'': The presupposition (before ∨ when) is NOT satisfied, so not...until is vacuously true but pragmatically infelicitous. This models why "She didn't wake up until the prince kissed her" is odd when she woke up AFTER the kiss — the presupposition fails.