@cite{karttunen-1974}: Until, When, and the Two-Until Hypothesis

@cite{karttunen-1974} @cite{heinamaki-1974} @cite{dowty-1979}Karttunen argues that English has two untils:

• Durative until: "John slept until 3pm." The main clause is durative (stative/activity), and until marks the minimum extent of the main event. Truth-conditionally, this is temporal overlap: A holds at the time of B.

• Punctual until: "The princess didn't wake up until the prince kissed her." Requires negation in the main clause. Karttunen's key identity (§5, eq. 33): this has the logical form NOT(A BEFORE T).

The punctual until presupposes A BEFORE T ∨ A WHEN T — the event eventually happens, either before or at the complement time. The assertion ¬(A BEFORE T) then derives, via disjunctive syllogism, that A occurs at T (temporal coincidence, i.e., when).

Level

Level 1 (point sets): all definitions operate on timeTrace projections, at the same level as Anscombe. The eight English temporal connectives reduce to four Level 1 primitives:

• before = ∃∀ + strict ordering (Anscombe)
• after = ∃∃ + strict ordering (Anscombe)
• when = ∃ overlap (this file)
• while = ∀ containment (this file)
• until = ¬before (punctual) or when (durative) — derived, not primitive
• till = until (dialectal variant, Heinämäki Ch. 9)
• since = ∃∈B ∀∈A + ≤ ordering (starting-point, Heinämäki Ch. 6)
• by = ∃∈A ∀∈B + ≤ ordering (deadline, Heinämäki Ch. 8)

Cross-Linguistic Evidence

Finnish lexicalizes the two-until distinction: kunnes / siihen saakka (durative) vs ennenkuin (punctual, literally 'before-than'). The Finnish punctual form is morphologically before, confirming Karttunen's analysis.

def Semantics.Tense.TemporalConnectives.Karttunen.when_ {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

When: temporal coincidence (∃-overlap). "A when B" holds when some time point belongs to both A and B.

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.when_ A B = ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, t ∈ Semantics.Tense.TemporalConnectives.timeTrace B

def Semantics.Tense.TemporalConnectives.Karttunen.while_ {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

While: temporal containment (∀-inclusion). "A while B" holds when every time in A is also a time in B. Stronger than when (which requires only one shared point).

This matches the implicit definition in @cite{rett-2026} used to prove while is not ambidirectional.

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.while_ A B = ∀ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, t ∈ Semantics.Tense.TemporalConnectives.timeTrace B

def Semantics.Tense.TemporalConnectives.Karttunen.until {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Durative until: the main event persists at least to the complement time. Truth-conditionally equivalent to when at Level 1: ∃-overlap.

The difference from when is a selectional restriction: until requires A to be durative (stative/activity). Combined with the subinterval property of statives, overlap entails continuous persistence of A up to the time of B — the "minimum length" semantics.

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.until A B = ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, t ∈ Semantics.Tense.TemporalConnectives.timeTrace B

def Semantics.Tense.TemporalConnectives.Karttunen.till {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Till: dialectal variant of durative until. Truth-conditionally identical to durative until (= when = ∃-overlap). Dialectally restricted in English; some varieties use till where standard English uses until.

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.till A B = ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, t ∈ Semantics.Tense.TemporalConnectives.timeTrace B

def Semantics.Tense.TemporalConnectives.Karttunen.since {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Since: lower-bound / starting-point semantics. "A since B" holds when some B-time precedes or coincides with all A-times. This mirrors before with swapped arguments and non-strict ordering: before = ∃t∈A, ∀t'∈B, t < t'; since = ∃t∈B, ∀t'∈A, t ≤ t'.

Veridical for B (the ∃ over B forces a witness). Equivalent to by_ with swapped arguments: since A B ↔ by_ B A.

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.since A B = ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace B, ∀ t' ∈ Semantics.Tense.TemporalConnectives.timeTrace A, t ≤ t'

def Semantics.Tense.TemporalConnectives.Karttunen.by_ {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

By: deadline / upper-bound semantics. "A by B" holds when some A-time precedes or coincides with all B-times. "He arrived by 3pm" = his arrival has a time point at or before 3pm.

Weaker than before (allows temporal coincidence: ≤ rather than <). Veridical for A (the ∃ over A forces a witness).

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.by_ A B = ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, ∀ t' ∈ Semantics.Tense.TemporalConnectives.timeTrace B, t ≤ t'

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

Punctual until = ¬(before) (@cite{karttunen-1974}, eq. 33). "The princess didn't wake up until the prince kissed her" = NOT(the princess woke up BEFORE the prince kissed her).

Presupposes A BEFORE T ∨ A WHEN T (lateness: the event eventually happens).

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.notUntil A B = ¬Semantics.Tense.TemporalConnectives.Anscombe.before A B

theorem Semantics.Tense.TemporalConnectives.until_iff_when {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.until A B ↔ Karttunen.when_ A B

Durative until and when are truth-conditionally identical at Level 1. The linguistic differences (selectional restriction on durativity, endpoint semantics) are pragmatic, not truth-conditional.

theorem Semantics.Tense.TemporalConnectives.when_veridical_complement {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.when_ A B → ∃ (t : Time), t ∈ timeTrace B

When is veridical w.r.t. its complement: B must have a witness.

theorem Semantics.Tense.TemporalConnectives.when_veridical_main {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.when_ A B → ∃ (t : Time), t ∈ timeTrace A

When is veridical w.r.t. its main clause: A must have a witness.

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

Durative until is veridical w.r.t. its complement.

theorem Semantics.Tense.TemporalConnectives.while_veridical_complement {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (hne : ∃ (t : Time), t ∈ timeTrace A) : Karttunen.while_ A B → ∃ (t : Time), t ∈ timeTrace B

While is veridical w.r.t. the main clause when A is nonempty: if ∀t∈A, t∈B and A has a witness, then B has a witness.

theorem Semantics.Tense.TemporalConnectives.notUntil_not_veridical : ∃ (A : SentDenotation ℤ) (B : SentDenotation ℤ), Karttunen.notUntil A B ∧ ¬∃ (t : ℤ), t ∈ timeTrace A

Punctual until is NOT veridical by assertion alone: ¬(A before B) holds vacuously when A is empty.

theorem Semantics.Tense.TemporalConnectives.notUntil_unfold {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.notUntil A B ↔ ∀ t ∈ timeTrace A, ∃ t' ∈ timeTrace B, ¬t < t'

Karttunen's main result (eq. 33): punctual until unfolds to "every A-time has some B-time at or before it."

"not A until B" = ¬(∃t∈A, ∀t'∈B, t<t') = ∀t∈A, ∃t'∈B, t'≤t.

This is logically equivalent to: every occurrence of A is preceded by (or coincides with) some occurrence of B.

theorem Semantics.Tense.TemporalConnectives.finnish_confirms_identity {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.notUntil A B ↔ ¬Anscombe.before A B

Finnish confirms Karttunen: the punctual until form ennenkuin is morphologically ennen ('before') + kuin ('than'), i.e., literal before-than — the negation is external to the connective.

This is definitionally true since notUntil = ¬before.

theorem Semantics.Tense.TemporalConnectives.notUntil_with_presupposition {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (hpre : Anscombe.before A B ∨ Karttunen.when_ A B) (hassert : Karttunen.notUntil A B) : Karttunen.when_ A B

The presupposition of punctual until: A BEFORE T ∨ A WHEN T. The event eventually happens — either before or at the complement time.

Combined with the assertion ¬(A BEFORE T), the presupposition yields A WHEN T (temporal coincidence) by disjunctive syllogism.

This derives the intuitive meaning: "not until B" ≈ "at B".

theorem Semantics.Tense.TemporalConnectives.when_symmetric {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.when_ A B ↔ Karttunen.when_ B A

When is symmetric: if A overlaps B, then B overlaps A.

theorem Semantics.Tense.TemporalConnectives.while_implies_when {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (hne : ∃ (t : Time), t ∈ timeTrace A) : Karttunen.while_ A B → Karttunen.when_ A B

While implies when (when A is nonempty): containment is stronger than overlap.

theorem Semantics.Tense.TemporalConnectives.while_not_symmetric : ¬∀ (A B : SentDenotation ℤ), Karttunen.while_ A B → Karttunen.while_ B A

While is NOT symmetric: containment is asymmetric.

Counterexample: A = point at 5, B = interval [1,10]. A ⊆ B (5 ∈ [1,10]) but B ⊄ A (1 ∉ {5}).

theorem Semantics.Tense.TemporalConnectives.while_transitive {Time : Type u_1} [LinearOrder Time] (A B C : SentDenotation Time) : Karttunen.while_ A B → Karttunen.while_ B C → Karttunen.while_ A C

While is transitive: temporal containment composes.

theorem Semantics.Tense.TemporalConnectives.after_witness_excludes_before_witness {Time : Type u_1} [LinearOrder Time] {t t' : Time} (hlt : t' < t) : ¬t < t'

For a fixed time point t in A, if some B-time precedes t, then t cannot precede ALL of B. This is the per-witness form of the ordering consistency between after and before.

theorem Semantics.Tense.TemporalConnectives.veridicality_mirrors_quantifier_force {Time : Type u_1} [LinearOrder Time] : (∀ (A B : SentDenotation Time), Anscombe.after A B → ∃ (t : Time), t ∈ timeTrace B) ∧ (∀ (A B : SentDenotation Time), Karttunen.when_ A B → ∃ (t : Time), t ∈ timeTrace B) ∧ ∃ (A : SentDenotation ℤ) (B : SentDenotation ℤ), Anscombe.before A B ∧ ¬∃ (t : ℤ), t ∈ timeTrace B

Veridicality summary for the five temporal connectives at Level 1:

• before: complement NOT veridical (∀ vacuously true on empty B)
• after: complement veridical (∃ witness required)
• when: complement veridical (∃ overlap witness)
• while: complement veridical only when A nonempty (∀ vacuously true)
• until (durative): complement veridical (= when)
• until (punctual): complement NOT veridical by assertion alone

The veridical/non-veridical split mirrors the quantifier structure: ∃-based connectives (after, when, durative until) are veridical; ∀-based connectives (before, while, punctual until) are non-veridical or conditionally veridical.

theorem Semantics.Tense.TemporalConnectives.till_iff_until {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.till A B ↔ Karttunen.until A B

Till and until are truth-conditionally identical.

theorem Semantics.Tense.TemporalConnectives.till_iff_when {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.till A B ↔ Karttunen.when_ A B

Till and when are truth-conditionally identical.

theorem Semantics.Tense.TemporalConnectives.since_veridical_complement {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.since A B → ∃ (t : Time), t ∈ timeTrace B

Since is veridical w.r.t. its complement: B must have a witness.

theorem Semantics.Tense.TemporalConnectives.since_eq_by_swap {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.since A B ↔ Karttunen.by_ B A

Since is the argument-swapped form of by: "A since B" ↔ "B by A". Both have the form ∃t∈X, ∀t'∈Y, t ≤ t'.

theorem Semantics.Tense.TemporalConnectives.by_veridical_main {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.by_ A B → ∃ (t : Time), t ∈ timeTrace A

By is veridical w.r.t. its main clause: A must have a witness.

theorem Semantics.Tense.TemporalConnectives.before_implies_by {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Anscombe.before A B → Karttunen.by_ A B

Before implies by: strict temporal ordering entails non-strict. "He left before 3pm" → "He left by 3pm."

theorem Semantics.Tense.TemporalConnectives.by_not_implies_before : ¬∀ (A B : SentDenotation ℤ), Karttunen.by_ A B → Anscombe.before A B

By does NOT imply before: coincidence is allowed under by but not before.

Counterexample: A = B = {point 5}. "He arrived by 5" is true when he arrives at 5, but "he arrived before 5" is false.

def Semantics.Tense.TemporalConnectives.Karttunen.whenever {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Whenever: universally quantified temporal overlap. "A whenever B" holds when every time point in B is also a time point in A. Equivalent to while_ with swapped arguments (B ⊆ A in time).

"Whenever it rains, I carry an umbrella" = every rain-time is an umbrella-time. Implies habitual/generic interpretation.

@cite{heinamaki-1974} treats whenever as a universal quantifier over temporal overlap events, distinguishing it from the existential when (∃-overlap).

Equations

• Semantics.Tense.TemporalConnectives.Karttunen.whenever A B = ∀ t ∈ Semantics.Tense.TemporalConnectives.timeTrace B, t ∈ Semantics.Tense.TemporalConnectives.timeTrace A

theorem Semantics.Tense.TemporalConnectives.whenever_iff_while_swap {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Karttunen.whenever A B ↔ Karttunen.while_ B A

Whenever is while with swapped arguments: "A whenever B" ↔ "B while A". Both express temporal containment, but whenever puts the containing event as the main clause and the contained event as the subordinate clause.

theorem Semantics.Tense.TemporalConnectives.whenever_implies_when {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (hne : ∃ (t : Time), t ∈ timeTrace B) : Karttunen.whenever A B → Karttunen.when_ A B

Whenever implies when (when B is nonempty): universal overlap entails existential overlap.

theorem Semantics.Tense.TemporalConnectives.whenever_not_symmetric : ¬∀ (A B : SentDenotation ℤ), Karttunen.whenever A B → Karttunen.whenever B A

Whenever is NOT symmetric: containment is directional. Counterexample: same as while_not_symmetric — A ⊂ B gives "A whenever B" false but "B whenever A" true.