[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 Rett2020.Rett.before {Time : Type u_1} [LinearOrder Time] (A B : Tense.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

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

def Rett2020.Rett.after {Time : Type u_1} [LinearOrder Time] (A B : Tense.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

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

def Rett2020.INCHOAT {Time : Type u_1} [LinearOrder Time] (p : Tense.SentDenotation Time) : Tense.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 Rett2020.COMPLET {Time : Type u_1} [LinearOrder Time] (p : Tense.SentDenotation Time) : Tense.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 Rett2020.inchoat_bridges_inception {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : INCHOAT (Tense.stativeDenotation i) = {j : NonemptyInterval Time | j = NonemptyInterval.pure i.toProd.1}

INCHOAT extracts the start point of a stative denotation.

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

COMPLET extracts the finish point of an accomplishment denotation.

theorem Rett2020.anscombe_rett_agree_stative_before_start {Time : Type u_1} [LinearOrder Time] (A : Tense.SentDenotation Time) (i_B : NonemptyInterval Time) : Anscombe1964.Anscombe.before A (Tense.stativeDenotation i_B) ↔ Rett.before A (Tense.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 Rett2020.rett_implies_anscombe_telic_after_finish {Time : Type u_1} [LinearOrder Time] (A : Tense.SentDenotation Time) (i_B : NonemptyInterval Time) : Rett.after A (Tense.accomplishmentDenotation i_B) → Anscombe1964.Anscombe.after A (Tense.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 Rett2020.rett_before_implies_anscombe {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Rett.before A B → Anscombe1964.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 Rett2020.rett_after_implies_anscombe {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Rett.after A B → Anscombe1964.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 Rett2020.before_determined_by_max {Time : Type u_1} [LinearOrder Time] (A B₁ B₂ : Tense.SentDenotation Time) (h : Core.Order.maxOnScale Core.Order.Comparison.lt (Tense.timeTrace B₁) = Core.Order.maxOnScale Core.Order.Comparison.lt (Tense.timeTrace B₂)) : Rett.before A B₁ ↔ Rett.before A B₂

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

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

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

theorem Rett2020.complet_stative {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : COMPLET (Tense.stativeDenotation i) = {j : NonemptyInterval Time | j = NonemptyInterval.pure i.toProd.2}

COMPLET on a stative denotation extracts the finish point.

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

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

Equations

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

theorem Rett2020.timeTrace_stative_closedInterval {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : Tense.timeTrace (Tense.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 Rett2020.maxOnScale_lt_stative {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : Core.Order.maxOnScale Core.Order.Comparison.lt (Tense.timeTrace (Tense.stativeDenotation i)) = {i.toProd.1}

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

theorem Rett2020.timeTrace_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.toProd.1) : Tense.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 Rett2020.maxOnScale_lt_complet_preEvent {Time : Type u_1} [LinearOrder Time] (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.toProd.1) : Core.Order.maxOnScale Core.Order.Comparison.lt (Tense.timeTrace (COMPLET (preEventDenotation bot i hbot))) = {i.toProd.1}

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

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

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

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

While is not ambidirectional.

Temporal Connective Truth-Condition Examples

[Hei74] [Ret20] [Kar74b]

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]'s since and by and [Kar74b]'s durative until (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.SentDenotation ℕ

Equations

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

@[reducible, inline]

abbrev Rett2020.Examples.A_late : Tense.SentDenotation ℕ

Equations

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

@[reducible, inline]

abbrev Rett2020.Examples.A_inside : Tense.SentDenotation ℕ

Equations

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

@[reducible, inline]

abbrev Rett2020.Examples.B_stative : Tense.SentDenotation ℕ

Equations

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

@[reducible, inline]

abbrev Rett2020.Examples.B_telic : Tense.SentDenotation ℕ

Equations

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

theorem Rett2020.Examples.scenario1_anscombe : Anscombe1964.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 : 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 : Anscombe1964.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 : 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 : Anscombe1964.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 : 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 : Anscombe1964.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 : 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 : ¬Anscombe1964.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 : ¬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 : Anscombe1964.Anscombe.before A_early B_stative ∧ Rett.before A_early B_stative

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

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

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

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

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

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

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

theorem Rett2020.Examples.inchoat_stative_ee : 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 : 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.SentDenotation ℕ

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

Equations

• Rett2020.Examples.A_stative = Tense.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.SentDenotation ℕ

Equations

• Rett2020.Examples.B_onset = Tense.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.SentDenotation ℕ

Equations

• Rett2020.Examples.A_at_deadline = Tense.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.SentDenotation ℕ

Equations

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

theorem Rett2020.Examples.scenario_since : Heinamaki1974.since A_stative B_onset

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

theorem Rett2020.Examples.scenario_since_veridical : Heinamaki1974.since A_stative B_onset → ∃ (t : ℕ), t ∈ Tense.timeTrace B_onset

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

theorem Rett2020.Examples.scenario_by_strict : Heinamaki1974.by_ A_early B_deadline

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

theorem Rett2020.Examples.scenario_by_coincidence : Heinamaki1974.by_ A_at_deadline B_deadline

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

theorem Rett2020.Examples.scenario_before_coincidence_false : ¬Anscombe1964.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 : Heinamaki1974.by_ A_at_deadline B_deadline ∧ ¬Anscombe1964.Anscombe.before A_at_deadline B_deadline

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

theorem Rett2020.Examples.scenario_till : Karttunen1974.until_ A_stative B_onset

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

Not...until scenarios

Karttunen's identity (33): punctual until = ¬before, with the presupposition (34) before ∨ when. We verify this on concrete time points.

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

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.SentDenotation ℕ

Equations

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

@[reducible, inline]

abbrev Rett2020.Examples.B_kiss : Tense.SentDenotation ℕ

Equations

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

theorem Rett2020.Examples.scenario11_before_true : Anscombe1964.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 : ¬Karttunen1974.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.SentDenotation ℕ

Equations

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

theorem Rett2020.Examples.scenario12_notUntil_true : Karttunen1974.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 : Karttunen1974.presupposition A_wake_at B_kiss

Scenario 12': the presupposition (34) holds — the waking is when the kiss is.

theorem Rett2020.Examples.scenario12_derives_when : Heinamaki1974.when_ A_wake_at B_kiss

Scenario 12'': assertion and presupposition derive when by disjunctive syllogism, Karttunen's (36).

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.SentDenotation ℕ

Equations

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

theorem Rett2020.Examples.scenario13_notUntil_true : Karttunen1974.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 : ¬Heinamaki1974.when_ A_wake_late B_kiss

Scenario 13': wake₇ is not when kiss₅.

theorem Rett2020.Examples.scenario13_presup_fails : ¬Karttunen1974.presupposition A_wake_late B_kiss

Scenario 13'': the presupposition (34) fails, so not...until is true but infelicitous when she woke up well after the kiss — [Kar74b]'s (29b) allows only "shortly thereafter", which (34) does not capture (his fn. 7).