Karttunen (1974): Until

[Kar74b] argues that English has two untils. Durative until modifies a durative sentence (1a–d) and marks the minimum length of its interval (12)–(14), (21): on run-time denotations, where a durative clause holds throughout each of its run-times, some run-time of A reaches a time of B (until_). Punctual until (1e) is a negative polarity item that locates an event in time; negation takes wide scope over it (3b), and the standard one-until arguments that negation makes a sentence durative fail (8)–(10). Its logical form is that of before: A not until T is NOT(A BEFORE T) (33) (notUntil, the negation of [Ans64]'s before), so every occurrence of A has a time of T at or before it (notUntil_iff), and its denial is A before T (30)–(31) (not_notUntil_iff). What distinguishes it from before is a pragmatic presupposition of lateness, (34): A before T or A when T (presupposition, with [Hei74]'s when). The logical form holds of a clause that never happens (notUntil_empty), so the commitment to A when T (29b) is not asserted but follows from assertion and presupposition by disjunctive syllogism, (36) (notUntil_when) — whence Nancy didn't get married until she died (23) commits the speaker to a marriage at her death, which before would not. Finnish separates the two untils, kunnes/saakka against ennenkuin (37), and its positive-polarity vasta, like German erst, asserts A when T under the same presupposition (38)–(39): for point events the two logical forms coincide given the presupposition (notUntil_iff_when_of_presupposition).

def Karttunen1974.until_ {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Prop

Durative A until B: some run-time of A reaches a time of B.

Equations

• Karttunen1974.until_ A B = ∃ t ∈ Tense.timeTrace A, t ∈ Tense.timeTrace B

def Karttunen1974.notUntil {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Prop

Punctual A not until B, (33): A not before B.

Equations

• Karttunen1974.notUntil A B = ¬Anscombe1964.Anscombe.before A B

def Karttunen1974.presupposition {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Prop

The presupposition of lateness, (34): A before B or A when B.

Equations

• Karttunen1974.presupposition A B = (Anscombe1964.Anscombe.before A B ∨ Heinamaki1974.when_ A B)

theorem Karttunen1974.until_veridical_complement {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : until_ A B → ∃ (t : Time), t ∈ Tense.timeTrace B

theorem Karttunen1974.notUntil_iff {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : notUntil A B ↔ ∀ t ∈ Tense.timeTrace A, ∃ t' ∈ Tense.timeTrace B, t' ≤ t

Every occurrence of A has a time of B at or before it.

theorem Karttunen1974.not_notUntil_iff {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : ¬notUntil A B ↔ Anscombe1964.Anscombe.before A B

Denying A not until B is asserting A before B, (30)–(31).

theorem Karttunen1974.notUntil_empty {Time : Type u_1} [LinearOrder Time] (B : Tense.SentDenotation Time) : notUntil ∅ B

The logical form holds of a clause that never happens.

theorem Karttunen1974.notUntil_when {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) (h : notUntil A B) (hp : presupposition A B) : Heinamaki1974.when_ A B

Disjunctive syllogism, (36): assertion and presupposition together yield A when B.

theorem Karttunen1974.mem_timeTrace_pure {Time : Type u_1} [LinearOrder Time] (a t : Time) : t ∈ Tense.timeTrace {NonemptyInterval.pure a} ↔ t = a

theorem Karttunen1974.notUntil_iff_when_of_presupposition {Time : Type u_1} [LinearOrder Time] (a b : Time) (hp : presupposition {NonemptyInterval.pure a} {NonemptyInterval.pure b}) : notUntil {NonemptyInterval.pure a} {NonemptyInterval.pure b} ↔ Heinamaki1974.when_ {NonemptyInterval.pure a} {NonemptyInterval.pure b}

For point events under the presupposition, A not until B and A when B — the logical forms of Finnish ennenkuin and vasta, (39) — say the same.