Heinämäki (1974): Semantics of English Temporal Connectives

Heinämäki gives the truth conditions of 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 Anscombe's quantificational before, with the roles of the clauses exchanged, so before ever entails by but not conversely (before_by, by_not_before). The existential connectives commit the speaker to both clauses; the universal ones do so only given the clause they quantify over, and are not symmetric (while_not_symm).

References

• [Hei74]
• [Ans64]

def Heinamaki1974.when_ {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

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

Equations

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

def Heinamaki1974.while_ {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

A while B holds when 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 {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

A whenever B holds when 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 {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

A since B holds when 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_ {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

A by B holds when 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 {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : when_ A B ↔ when_ B A

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

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

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

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

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

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

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

theorem Heinamaki1974.before_by {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Tense.beforeEver A B → by_ A B

Before ever is strict by.

def Heinamaki1974.before {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (lb : T) : Prop

A before B by the reference point holds when some time of A precedes B's first time lb.

Equations

• Heinamaki1974.before A lb = ∃ t ∈ Tense.timeTrace A, t < lb

def Heinamaki1974.after {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (lb : T) : Prop

A after B by the reference point holds when some time of A follows B's first time lb.

Equations

• Heinamaki1974.after A lb = ∃ t ∈ Tense.timeTrace A, lb < t

theorem Heinamaki1974.before_iff_anscombe {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) {lb : T} (hlb : IsLeast (Tense.timeTrace B) lb) : before A lb ↔ Tense.beforeEver A B

When B has a first time, the reference-point before is [Ans64]'s quantificational one.

theorem Heinamaki1974.after_iff_anscombe {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) {lb : T} (hlb : IsLeast (Tense.timeTrace B) lb) : after A lb ↔ Anscombe1964.Anscombe.after A B

When B has a first time, the reference-point after is [Ans64]'s.

theorem Heinamaki1974.while_not_symm : ¬∀ (A B : Set (NonemptyInterval ℤ)), while_ A B → while_ B A

While is not symmetric, as a moment inside a stretch shows.

theorem Heinamaki1974.by_not_before : ¬∀ (A B : Set (NonemptyInterval ℤ)), by_ A B → Tense.beforeEver A B

By allows coincidence where before does not, as an arrival exactly at the deadline shows.