Heinämäki (1974): English temporal connectives

[Hei74] gives truth conditions for the English temporal connectives in terms of the times at which the two clauses hold. On run-time denotations they are relations between the clauses' time traces: A when B asserts that the two hold at a common time (when_), A while B that every time of A is a time of B (while_), A whenever B the converse containment (whenever), A since B that some time of B lies at or before every time of A (since), and A by B that some time of A lies at or before every time of B (by_). Since and by are the non-strict counterparts of [Ans64]'s before, with the roles of the clauses exchanged, so before entails by but not conversely (before_by, by_not_before). The existential connectives commit the speaker to both clauses (when_veridical_complement, since_veridical_complement, by_veridical_main); the universal ones do so only given the clause they quantify over (while_veridical_complement), and are not symmetric (while_not_symm).

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

A when B: A and B hold at a common time.

Equations

• Heinamaki1974.when_ A B = ∃ t ∈ Tense.timeTrace A, t ∈ Tense.timeTrace B

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

A while B: every time of A is a time of B.

Equations

• Heinamaki1974.while_ A B = ∀ t ∈ Tense.timeTrace A, t ∈ Tense.timeTrace B

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

A whenever B: every time of B is a time of A.

Equations

• Heinamaki1974.whenever A B = ∀ t ∈ Tense.timeTrace B, t ∈ Tense.timeTrace A

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

A since B: some time of B is at or before every time of A.

Equations

• Heinamaki1974.since A B = ∃ t ∈ Tense.timeTrace B, ∀ t' ∈ Tense.timeTrace A, t ≤ t'

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

A by B: some time of A is at or before every time of B.

Equations

• Heinamaki1974.by_ A B = ∃ t ∈ Tense.timeTrace A, ∀ t' ∈ Tense.timeTrace B, t ≤ t'

theorem Heinamaki1974.when_comm {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : when_ A B ↔ when_ B A

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

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

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

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

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

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

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

theorem Heinamaki1974.before_by {Time : Type u_1} [LinearOrder Time] (A B : Tense.SentDenotation Time) : Anscombe1964.Anscombe.before A B → by_ A B

Before is strict by.

theorem Heinamaki1974.while_not_symm : ¬∀ (A B : Tense.SentDenotation ℤ), while_ A B → while_ B A

While is not symmetric: a moment inside a stretch.

theorem Heinamaki1974.by_not_before : ¬∀ (A B : Tense.SentDenotation ℤ), by_ A B → Anscombe1964.Anscombe.before A B

By allows coincidence where before does not: an arrival exactly at the deadline.