Karttunen (1974): Until #

Karttunen argues that English has two untils. Durative until modifies a durative sentence and marks the minimum length of its interval: some run-time of A reaches a time of B. Punctual until is a negative polarity item whose logical form is that of before, A not until T being the negation of Anscombe's quantificational before (33). What distinguishes it from before is a pragmatic presupposition of lateness, A before T or A when T (34), with Heinämäki's when. Since the logical form holds of a clause that never happens, the commitment to A when T follows from assertion and presupposition by disjunctive syllogism (36), which is why Nancy didn't get married until she died (23) commits the speaker to a marriage at her death.

Main statements #

notUntil_iff, not_notUntil_iff: every occurrence of A has a time of T at or before it, and the denial is A before T.
notUntil_empty: the logical form holds of a clause that never happens.
notUntil_when: assertion and presupposition together yield A when T.
notUntil_iff_when_of_presupposition: for point events the two logical forms coincide given the presupposition, as with Finnish vasta and German erst (38)–(39).

References #

source

def Karttunen1974.until_ {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

Prop

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

Equations

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

Instances For

source

def Karttunen1974.notUntil {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

Prop

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

Equations

Karttunen1974.notUntil A B = ¬Tense.beforeEver A B

Instances For

source

def Karttunen1974.presupposition {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

Prop

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

Equations

Karttunen1974.presupposition A B = (Tense.beforeEver A B ∨ Heinamaki1974.when_ A B)

Instances For

source

theorem Karttunen1974.until_veridical_complement {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

until_ A B → ∃ (t : T), t ∈ Tense.timeTrace B

source

theorem Karttunen1974.notUntil_iff {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

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.

source

theorem Karttunen1974.not_notUntil_iff {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) :

¬notUntil A B ↔ Tense.beforeEver A B

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

source

theorem Karttunen1974.notUntil_empty {T : Type u_1} [LinearOrder T] (B : Set (NonemptyInterval T)) :

notUntil ∅ B

The logical form holds of a clause that never happens.

source

theorem Karttunen1974.notUntil_when {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) (h : notUntil A B) (hp : presupposition A B) :

Heinamaki1974.when_ A B

By disjunctive syllogism, (36), assertion and presupposition together yield A when B.

source

theorem Karttunen1974.notUntil_iff_when_of_presupposition {T : Type u_1} [LinearOrder T] (a b : T) (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.