Run times

import Linglib.Semantics.Tense.RunTimes · namespace Tense

After Krifka, a clause denotes its run times, the set of intervals at which it holds. A stative clause holding throughout i denotes i with all its subintervals, the principal lower set Set.Iic i, an accomplishment over i the singleton {i}, and an event predicate the image of its events under the temporal trace (Event.TemporalTrace). This file defines the time trace of a set of intervals, the time points it covers, and Anscombe's universal before, a time of one clause before every time of the other, the reading Anscombe gives before ever. The times before every time of a clause are its strict lower bounds, the complement of its upward closure: before is not yet, the negation of when or after. They form a lower set, so before ever is anti-additive in its temporal clause. The other analyses of temporal connectives built on run times live in their studies.

Main definitions

Tense.timeTrace: the time points that a set of intervals covers.
Tense.beforeEver: Anscombe's universal before.

Main statements

Tense.beforeEver_iff_not_subset_upperClosure: before is not yet.
Tense.beforeEver_union_right: before ever is anti-additive in its temporal clause.

References

Krifka 1989, Nominal Reference, Temporal Constitution and Quantification in Event Semantics formalized
Anscombe 1964, Before and After formalized

Declarations

The time trace of a set of intervals is the set of time points they contain.

def timeTrace L49–51

{T : Type u_1} [Preorder T] (p : Set (NonemptyInterval T)) :

Set T

timeTrace p = {t : T | ∃ i ∈ p, t ∈ i}

Used by mem_timeTrace, timeTrace_image, timeTrace_empty, timeTrace_union, isLeast_timeTrace_singleton, isGreatest_timeTrace_singleton, beforeEver, beforeEver_iff, beforeEver_iff_of_isLeast, timeTrace_singleton, timeTrace_insert, mem_timeTrace_pure, timeTrace_Iic, mem_timeTrace_Iic, isLeast_timeTrace_Iic, isGreatest_timeTrace_Iic, beforeEver_iff_not_subset_upperClosure

Used in Anscombe1964, BeaverCondoravdi2003, JinKoenig2021, Karttunen1974, Rett2020a and 2 more

Before ever

p before ever q holds when a time of p precedes every time of q, Anscombe's universal rendering of before (Anscombe 1964 §IV–V).

def beforeEver L78–81

{T : Type u_1} [Preorder T] (A B : Set (NonemptyInterval T)) :

Prop

beforeEver A B = ∃ t ∈ timeTrace A, ∀ t' ∈ timeTrace B, t < t'

Built from

Used by beforeEver_iff, beforeEver_iff_of_isLeast, beforeEver_singleton_right, beforeEver_iff_not_subset_upperClosure, beforeEver_union_right

Used in Semantics/Events/Lifespan, Anscombe1964, ArreguiKusumoto1998, BeaverCondoravdi2003, Giannakidou2002 and 4 more

Before is not yet. A is before ever B exactly when some time of A lies outside the upward closure of B's times, the times at which B holds or has held.

theorem beforeEver_iff_not_subset_upperClosure L139–143

{T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} :

beforeEver A B ↔ ¬timeTrace A ⊆ ↑(upperClosure (timeTrace B))

Built from ,

Before ever is anti-additive in its temporal clause, since the times before every time of a clause form a lower set and the lower sets of a linear order are nested.

theorem beforeEver_union_right L145–154

{T : Type u_1} [LinearOrder T] {A B C : Set (NonemptyInterval T)} :

beforeEver A (B ∪ C) ↔ beforeEver A B ∧ beforeEver A C

Built from