[Ret20]: Antonymy + Aspectual Coercion

[Ret20] [Ret26] [JK21] [Kri10]before and after are antonyms on converse scales, with strong defaults [dS98] [Dol14] (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 Degree 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 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

• Tense.TemporalConnectives.Rett.before A B = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, ∃ m ∈ Degree.maxOnScale Core.Order.Comparison.lt (Tense.TemporalConnectives.timeTrace B), t < m

def 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

• Tense.TemporalConnectives.Rett.after A B = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, ∃ m ∈ Degree.maxOnScale Core.Order.Comparison.gt (Tense.TemporalConnectives.timeTrace B), t > m

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

Inchoative coercion / GLB ([Ret20], eq. 19; [dS98]; [Dol14]). 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 Tense.TemporalConnectives.COMPLET {Time : Type u_1} [LinearOrder Time] (p : SentDenotation Time) : SentDenotation Time

Completive coercion / LUB ([Ret20], eq. 21; [Dol14]). 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 Tense.TemporalConnectives.inchoat_bridges_inception {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : INCHOAT (stativeDenotation i) = {j : NonemptyInterval Time | j = NonemptyInterval.pure i.toProd.1}

INCHOAT extracts the start point of a stative denotation.

theorem Tense.TemporalConnectives.complet_bridges_cessation {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : COMPLET (accomplishmentDenotation i) = {j : NonemptyInterval Time | j = NonemptyInterval.pure i.toProd.2}

COMPLET extracts the finish point of an accomplishment denotation.

theorem Tense.TemporalConnectives.anscombe_rett_agree_stative_before_start {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : NonemptyInterval 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.fst (the GLB), and t < B.fst ↔ t < all times in B.

theorem Tense.TemporalConnectives.rett_implies_anscombe_telic_after_finish {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : NonemptyInterval 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.snd). These differ when A overlaps B without extending past B's endpoint.

theorem 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 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

[Ret26] 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 ([JK21]: 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 Tense.TemporalConnectives.before_determined_by_max {Time : Type u_1} [LinearOrder Time] (A B₁ B₂ : SentDenotation Time) (h : Degree.maxOnScale Core.Order.Comparison.lt (timeTrace B₁) = Degree.maxOnScale Core.Order.Comparison.lt (timeTrace B₂)) : Rett.before A B₁ ↔ Rett.before A B₂

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

theorem 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 Tense.TemporalConnectives.complet_stative {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : COMPLET (stativeDenotation i) = {j : NonemptyInterval Time | j = NonemptyInterval.pure i.toProd.2}

COMPLET on a stative denotation extracts the finish point.

def Tense.TemporalConnectives.preEventDenotation {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.toProd.1) : SentDenotation Time

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

Equations

• Tense.TemporalConnectives.preEventDenotation bot i hbot = Tense.TemporalConnectives.stativeDenotation { fst := bot, snd := i.toProd.1, fst_le_snd := hbot }

theorem Tense.TemporalConnectives.timeTrace_stative_closedInterval {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : timeTrace (stativeDenotation i) = {t : Time | i.toProd.1 ≤ t ∧ t ≤ i.toProd.2}

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

theorem Tense.TemporalConnectives.maxOnScale_lt_stative {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : Degree.maxOnScale Core.Order.Comparison.lt (timeTrace (stativeDenotation i)) = {i.toProd.1}

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

theorem Tense.TemporalConnectives.timeTrace_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.toProd.1) : timeTrace (COMPLET (preEventDenotation bot i hbot)) = {t : Time | i.toProd.1 ≤ t ∧ t ≤ i.toProd.1}

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

theorem Tense.TemporalConnectives.maxOnScale_lt_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.toProd.1) : Degree.maxOnScale Core.Order.Comparison.lt (timeTrace (COMPLET (preEventDenotation bot i hbot))) = {i.toProd.1}

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

theorem Tense.TemporalConnectives.before_preEvent_ambidirectional {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (i_B : NonemptyInterval Time) (bot : Time) (hbot : bot ≤ i_B.toProd.1) : 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 Tense.TemporalConnectives.after_not_ambidirectional {Time : Type u_1} [LinearOrder Time] (hab : ∃ (a : Time) (b : Time), a < b) : ¬∀ (A : SentDenotation Time) (B : Set Time), Degree.isAmbidirectional (fun (X : Set Time) => ∃ t ∈ timeTrace A, ∃ m ∈ Degree.maxOnScale Core.Order.Comparison.gt X, t > m) B

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

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

While is not ambidirectional.

Temporal Connective Truth-Condition Examples

[Hei74] [Ret20] [Kar74]

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

Scenarios 1–6 verify [Ret20] Table 1 for before/after. Scenarios 7–10 verify [Hei74] 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 Rett2020.Examples.me_early : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_early = NonemptyInterval.pure 1

def Rett2020.Examples.me_late : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_late = NonemptyInterval.pure 12

def Rett2020.Examples.me_inside : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_inside = NonemptyInterval.pure 7

def Rett2020.Examples.ee_stative : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.ee_stative = { fst := 5, snd := 10, fst_le_snd := Rett2020.Examples.ee_stative._proof_2 }

def Rett2020.Examples.ee_accomplishment : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.ee_accomplishment = { fst := 3, snd := 8, fst_le_snd := Rett2020.Examples.ee_accomplishment._proof_2 }

@[reducible, inline]

abbrev Rett2020.Examples.A_early : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_early = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_early

@[reducible, inline]

abbrev Rett2020.Examples.A_late : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_late = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_late

@[reducible, inline]

abbrev Rett2020.Examples.A_inside : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_inside = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_inside

@[reducible, inline]

abbrev Rett2020.Examples.B_stative : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.B_stative = Tense.TemporalConnectives.stativeDenotation Rett2020.Examples.ee_stative

@[reducible, inline]

abbrev Rett2020.Examples.B_telic : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.B_telic = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.ee_accomplishment

theorem Rett2020.Examples.scenario1_anscombe : 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 Rett2020.Examples.scenario1_rett : 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 Rett2020.Examples.scenario2_anscombe : 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 Rett2020.Examples.scenario2_rett : 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 Rett2020.Examples.scenario3_anscombe : 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 Rett2020.Examples.scenario3_rett : 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 Rett2020.Examples.scenario4_anscombe : 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 Rett2020.Examples.scenario4_rett : 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 Rett2020.Examples.scenario5_anscombe_false : ¬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 Rett2020.Examples.scenario6_rett_false : ¬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 Rett2020.Examples.scenario1_agree : Tense.TemporalConnectives.Anscombe.before A_early B_stative ∧ Tense.TemporalConnectives.Rett.before A_early B_stative

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

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

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

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

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

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

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

theorem Rett2020.Examples.inchoat_stative_ee : Tense.TemporalConnectives.INCHOAT B_stative = {j : NonemptyInterval ℕ | j = NonemptyInterval.pure 5}

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

theorem Rett2020.Examples.complet_telic_ee : Tense.TemporalConnectives.COMPLET B_telic = {j : NonemptyInterval ℕ | j = NonemptyInterval.pure 8}

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

@[reducible, inline]

abbrev Rett2020.Examples.A_stative : Tense.TemporalConnectives.SentDenotation ℕ

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

Equations

• Rett2020.Examples.A_stative = Tense.TemporalConnectives.stativeDenotation Rett2020.Examples.ee_stative

def Rett2020.Examples.ee_onset : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.ee_onset = NonemptyInterval.pure 5

@[reducible, inline]

abbrev Rett2020.Examples.B_onset : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.B_onset = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.ee_onset

def Rett2020.Examples.me_at_deadline : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_at_deadline = NonemptyInterval.pure 3

@[reducible, inline]

abbrev Rett2020.Examples.A_at_deadline : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_at_deadline = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_at_deadline

def Rett2020.Examples.ee_deadline : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.ee_deadline = NonemptyInterval.pure 3

@[reducible, inline]

abbrev Rett2020.Examples.B_deadline : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.B_deadline = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.ee_deadline

theorem Rett2020.Examples.scenario_since : 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 Rett2020.Examples.scenario_since_veridical : Tense.TemporalConnectives.Karttunen.since A_stative B_onset → ∃ (t : ℕ), t ∈ Tense.TemporalConnectives.timeTrace B_onset

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

theorem Rett2020.Examples.scenario_by_strict : 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 Rett2020.Examples.scenario_by_coincidence : 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 Rett2020.Examples.scenario_before_coincidence_false : ¬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 Rett2020.Examples.by_without_before : Tense.TemporalConnectives.Karttunen.by_ A_at_deadline B_deadline ∧ ¬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 Rett2020.Examples.scenario_till : 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 Rett2020.Examples.till_matches_until_scenario : Tense.TemporalConnectives.Karttunen.till A_stative B_onset ↔ 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 Rett2020.Examples.me_wake_early : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_wake_early = NonemptyInterval.pure 3

def Rett2020.Examples.ee_kiss : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.ee_kiss = NonemptyInterval.pure 5

@[reducible, inline]

abbrev Rett2020.Examples.A_wake_early : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_wake_early = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_wake_early

@[reducible, inline]

abbrev Rett2020.Examples.B_kiss : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.B_kiss = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.ee_kiss

theorem Rett2020.Examples.scenario11_before_true : 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 Rett2020.Examples.scenario11_notUntil_false : ¬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 Rett2020.Examples.me_wake_at_kiss : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_wake_at_kiss = NonemptyInterval.pure 5

@[reducible, inline]

abbrev Rett2020.Examples.A_wake_at : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_wake_at = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_wake_at_kiss

theorem Rett2020.Examples.scenario12_notUntil_true : 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 Rett2020.Examples.scenario12_presupposition : Tense.TemporalConnectives.Anscombe.before A_wake_at B_kiss ∨ 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 Rett2020.Examples.scenario12_derives_when : 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 Rett2020.Examples.me_wake_late : NonemptyInterval ℕ

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

Equations

• Rett2020.Examples.me_wake_late = NonemptyInterval.pure 7

@[reducible, inline]

abbrev Rett2020.Examples.A_wake_late : Tense.TemporalConnectives.SentDenotation ℕ

Equations

• Rett2020.Examples.A_wake_late = Tense.TemporalConnectives.accomplishmentDenotation Rett2020.Examples.me_wake_late

theorem Rett2020.Examples.scenario13_notUntil_true : 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 Rett2020.Examples.scenario13_not_when : ¬Tense.TemporalConnectives.Karttunen.when_ A_wake_late B_kiss

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

theorem Rett2020.Examples.scenario13_presup_fails : ¬(Tense.TemporalConnectives.Anscombe.before A_wake_late B_kiss ∨ 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.