Rett (2020): Eliminating EARLIEST: a general semantics for before and after

This file formalizes the paper's semantics for before and after as antonyms over converse scales. Each relates some time of its main clause to the most informative time of its embedded clause, the least on the before scale and the greatest on the after scale, before and after, with maximality relativized to the scale as in the degree domain, Degree.maxOnScale. Two aspectual coercions supply the remaining readings: a process may denote the onset of its duration, inchoative, and a culmination its telos, completive, so that against a process an after clause is ambiguous between the end and the onset while a before clause is not, and against a culmination a before clause is ambiguous between the start and the telos while an after clause is not: the six readings of the paper's Table 1 and no seventh, before_process, before_culmination_telos, after_process_onset, after_culmination, instantiated by the paper's (23) and (24). The default readings are downward entailing in the embedded clause, before_antitone and after_antitone, the account's route to NPI licensing, and the coerced readings are not, not_before_completive_antitone. Anscombe's before, a time of the main clause before every time of the embedded clause, is the default reading whenever the embedded clause has a first time, before_iff_beforeEver.

Implementation notes

Run times are sets of intervals, and an eventuality's duration is its timeTrace; the coercions act on the trace, so an eventuality's class enters only through which coercion readings makes available, as in the paper's (19) and (21). Of the typological survey of section 2.4, the rows record the Serbo-Croatian and Tagalog sentences whose overt aspect selects a reading, Marking.select, with the unambiguous Tagalog before and German after sentences; the veridicality asymmetry and the NPI facts of (25) and (26) receive no proposal in the paper beyond monotonicity.

References

• J. Rett, Eliminating EARLIEST: a general semantics for before and after (2020)
• G. E. M. Anscombe, Before and after (1964)
• O. Heinämäki, Semantics of English temporal connectives (1974)
• D. Beaver, C. Condoravdi, A uniform analysis of before and after (2003)
• C. Condoravdi, NPI licensing in temporal clauses (2010)
• M. Krifka, Before and after without coercion: comment on the paper by Cleo Condoravdi (2010)
• H. de Swart, Aspect shift and coercion (1998)
• J. Dölling, Aspectual coercion and eventuality structure (2014)
• H. Rullmann, Maximality in the semantics of wh-constructions (1995)
• C. Kennedy, Projecting the adjective (1997)

The relations and the coercions

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

A before B (22a) holds when some time of A precedes the most informative time of B on the before scale, its least.

Equations

• Rett2020a.before A B = ∃ t ∈ Tense.timeTrace A, ∃ m ∈ Degree.maxOnScale Degree.Comparison.lt (Tense.timeTrace B), t < m

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

A after B (22b) holds when some time of A follows the most informative time of B on the after scale, its greatest.

Equations

• Rett2020a.after A B = ∃ t ∈ Tense.timeTrace A, ∃ m ∈ Degree.maxOnScale Degree.Comparison.gt (Tense.timeTrace B), m < t

def Rett2020a.inchoative {T : Type u_1} [LinearOrder T] (p : Set (NonemptyInterval T)) : Set (NonemptyInterval T)

Under inchoative coercion (19) a process may denote the onset of its duration, the greatest lower bound of its times.

Equations

• Rett2020a.inchoative p = {i : NonemptyInterval T | ∃ (g : T), IsLeast (Tense.timeTrace p) g ∧ i = NonemptyInterval.pure g}

def Rett2020a.completive {T : Type u_1} [LinearOrder T] (p : Set (NonemptyInterval T)) : Set (NonemptyInterval T)

Under completive coercion (21) a culmination may denote its telos, the least upper bound of its times.

Equations

• Rett2020a.completive p = {i : NonemptyInterval T | ∃ (l : T), IsGreatest (Tense.timeTrace p) l ∧ i = NonemptyInterval.pure l}

inductive Rett2020a.Class : Type

The paper groups the aspectual classes of Moens and Steedman into processes, states and activities, and culminations, accomplishments and achievements.

• process : Class
• culmination : Class

def Rett2020a.readings {T : Type u_1} [LinearOrder T] : Class → Set (NonemptyInterval T) → Set (Set (NonemptyInterval T))

An embedded eventuality of a class with run times p may denote the run times themselves or the coercion its class allows.

Equations

• Rett2020a.readings Rett2020a.Class.process x✝ = {x✝, Rett2020a.inchoative x✝}
• Rett2020a.readings Rett2020a.Class.culmination x✝ = {x✝, Rett2020a.completive x✝}

theorem Rett2020a.timeTrace_inchoative {T : Type u_1} [LinearOrder T] (p : Set (NonemptyInterval T)) : Tense.timeTrace (inchoative p) = {g : T | IsLeast (Tense.timeTrace p) g}

theorem Rett2020a.timeTrace_completive {T : Type u_1} [LinearOrder T] (p : Set (NonemptyInterval T)) : Tense.timeTrace (completive p) = {l : T | IsGreatest (Tense.timeTrace p) l}

theorem Rett2020a.before_iff_of_isLeast {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsLeast (Tense.timeTrace B) m) : before A B ↔ ∃ t ∈ Tense.timeTrace A, t < m

Against an embedded clause with a first time, before is precedence of that time.

theorem Rett2020a.after_iff_of_isGreatest {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsGreatest (Tense.timeTrace B) m) : after A B ↔ ∃ t ∈ Tense.timeTrace A, m < t

Against an embedded clause with a last time, after is succession of that time.

theorem Rett2020a.timeTrace_completive_of_isGreatest {T : Type u_1} [LinearOrder T] {B : Set (NonemptyInterval T)} {m : T} (h : IsGreatest (Tense.timeTrace B) m) : Tense.timeTrace (completive B) = {m}

theorem Rett2020a.timeTrace_inchoative_of_isLeast {T : Type u_1} [LinearOrder T] {B : Set (NonemptyInterval T)} {m : T} (h : IsLeast (Tense.timeTrace B) m) : Tense.timeTrace (inchoative B) = {m}

theorem Rett2020a.before_completive_iff {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsGreatest (Tense.timeTrace B) m) : before A (completive B) ↔ ∃ t ∈ Tense.timeTrace A, t < m

Completive coercion turns before into precedence of the telos.

theorem Rett2020a.after_inchoative_iff {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsLeast (Tense.timeTrace B) m) : after A (inchoative B) ↔ ∃ t ∈ Tense.timeTrace A, m < t

Inchoative coercion turns after into succession of the onset.

theorem Rett2020a.before_inchoative_iff {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsLeast (Tense.timeTrace B) m) : before A (inchoative B) ↔ before A B

Inchoative coercion leaves before as it is, since the onset is already its point.

theorem Rett2020a.after_completive_iff {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {m : T} (h : IsGreatest (Tense.timeTrace B) m) : after A (completive B) ↔ after A B

Completive coercion leaves after as it is, since the telos is already its point.

Table 1

theorem Rett2020a.isLeast_timeTrace_stative {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : IsLeast (Tense.timeTrace (Set.Iic i)) i.toProd.1

theorem Rett2020a.isGreatest_timeTrace_stative {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : IsGreatest (Tense.timeTrace (Set.Iic i)) i.toProd.2

theorem Rett2020a.isLeast_timeTrace_accomplishment {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : IsLeast (Tense.timeTrace {i}) i.toProd.1

theorem Rett2020a.isGreatest_timeTrace_accomplishment {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : IsGreatest (Tense.timeTrace {i}) i.toProd.2

theorem Rett2020a.before_process {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) (B : Set (NonemptyInterval T)) : B ∈ readings Class.process (Set.Iic i) → (before A B ↔ ∃ t ∈ Tense.timeTrace A, t < i.toProd.1)

Against a process, before has one reading, precedence of its onset ((4a)), since inchoative coercion changes nothing and completive coercion is unavailable.

theorem Rett2020a.before_culmination_start {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) : before A {i} ↔ ∃ t ∈ Tense.timeTrace A, t < i.toProd.1

Against a culmination, before reads as precedence of its start ((5a), the paper's (23a)) ...

theorem Rett2020a.before_culmination_telos {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) : before A (completive {i}) ↔ ∃ t ∈ Tense.timeTrace A, t < i.toProd.2

... or, under completive coercion, of its telos ((23b)).

theorem Rett2020a.after_process_end {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) : after A (Set.Iic i) ↔ ∃ t ∈ Tense.timeTrace A, i.toProd.2 < t

Against a process, after reads as succession of its end ((5b), the paper's (24a)) ...

theorem Rett2020a.after_process_onset {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) : after A (inchoative (Set.Iic i)) ↔ ∃ t ∈ Tense.timeTrace A, i.toProd.1 < t

... or, under inchoative coercion, of its onset ((24b)).

theorem Rett2020a.after_culmination {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) (B : Set (NonemptyInterval T)) : B ∈ readings Class.culmination {i} → (after A B ↔ ∃ t ∈ Tense.timeTrace A, i.toProd.2 < t)

Against a culmination, after has one reading, succession of its telos ((4b)), since completive coercion changes nothing and inchoative coercion is unavailable.

theorem Rett2020a.before_stative_iff {T : Type u_1} [LinearOrder T] {B : Set (NonemptyInterval T)} {m : T} (i : NonemptyInterval T) (h : IsLeast (Tense.timeTrace B) m) : before (Set.Iic i) B ↔ i.toProd.1 < m

A stative main clause is before an embedded clause with a first time iff its onset precedes that time.

theorem Rett2020a.after_stative_iff {T : Type u_1} [LinearOrder T] {B : Set (NonemptyInterval T)} {m : T} (i : NonemptyInterval T) (h : IsGreatest (Tense.timeTrace B) m) : after (Set.Iic i) B ↔ m < i.toProd.2

A stative main clause is after an embedded clause with a last time iff its end follows that time.

theorem Rett2020a.before_stative_accomplishment_iff {T : Type u_1} [LinearOrder T] (i j : NonemptyInterval T) : before (Set.Iic i) {j} ↔ i.toProd.1 < j.toProd.1

theorem Rett2020a.before_stative_completive_iff {T : Type u_1} [LinearOrder T] (i j : NonemptyInterval T) : before (Set.Iic i) (completive {j}) ↔ i.toProd.1 < j.toProd.2

theorem Rett2020a.after_stative_stative_iff {T : Type u_1} [LinearOrder T] (i j : NonemptyInterval T) : after (Set.Iic i) (Set.Iic j) ↔ j.toProd.2 < i.toProd.2

theorem Rett2020a.after_stative_inchoative_iff {T : Type u_1} [LinearOrder T] (i j : NonemptyInterval T) : after (Set.Iic i) (inchoative (Set.Iic j)) ↔ j.toProd.1 < i.toProd.2

theorem Rett2020a.example23 : ¬before {NonemptyInterval.pure 15} {{ fst := 13, snd := 16, fst_le_snd := example23._proof_2 }} ∧ before {NonemptyInterval.pure 15} (completive {{ fst := 13, snd := 16, fst_le_snd := example23._proof_2 }})

In (23) John met Mary at three and Mary climbed the mountain from one to four, so before the start of the climb is false and before its telos true.

theorem Rett2020a.example24 : ¬after {NonemptyInterval.pure 2022} (Set.Iic { fst := 2021, snd := 2028, fst_le_snd := example24._proof_2 }) ∧ after {NonemptyInterval.pure 2022} (inchoative (Set.Iic { fst := 2021, snd := 2028, fst_le_snd := example24._proof_2 }))

In (24) John met Mary in 2022 and Mary was president from 2021 to 2028, so after the end of her term is false and after its onset true.

Monotonicity

theorem Rett2020a.before_antitone {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) {B B' : Set (NonemptyInterval T)} (h : Tense.timeTrace B' ⊆ Tense.timeTrace B) (hB' : ∃ (m' : T), IsLeast (Tense.timeTrace B') m') : before A B → before A B'

Before on its default reading is downward entailing in the embedded clause, since a sub-eventuality with a first time starts no earlier.

theorem Rett2020a.after_antitone {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) {B B' : Set (NonemptyInterval T)} (h : Tense.timeTrace B' ⊆ Tense.timeTrace B) (hB' : ∃ (m' : T), IsGreatest (Tense.timeTrace B') m') : after A B → after A B'

After on its default reading is downward entailing in the embedded clause, since a sub-eventuality with a last time ends no later.

theorem Rett2020a.not_before_completive_antitone {T : Type u_1} [LinearOrder T] (h₃ : ∃ (a : T) (b : T) (c : T), a < b ∧ b < c) : ¬∀ (A B B' : Set (NonemptyInterval T)), Tense.timeTrace B' ⊆ Tense.timeTrace B → (∃ (l' : T), IsGreatest (Tense.timeTrace B') l') → before A (completive B) → before A (completive B')

The coerced reading is not downward entailing, since precedence of a telos does not carry over to a sub-eventuality with an earlier telos, so a before clause licenses NPIs only on its default reading (25).

Anscombe

theorem Rett2020a.before_iff_beforeEver {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) {B : Set (NonemptyInterval T)} {m : T} (h : IsLeast (Tense.timeTrace B) m) : before A B ↔ Tense.beforeEver A B

Anscombe's before, a time of the main clause before every time of the embedded clause, is the default reading whenever the embedded clause has a first time.

theorem Rett2020a.after_imp_after {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) {B : Set (NonemptyInterval T)} : after A B → Anscombe1964.Anscombe.after A B

After entails Anscombe's existential after, a time of the main clause after some time of the embedded clause.

Overt aspect marking

inductive Rett2020a.Marking : Type

In a language that grammaticizes the coercion, the aspect of an embedded culmination decides it. The Serbo-Croatian perfective and the Tagalog ability-and-involuntary-action perfective are culminating, and their imperfective and neutral-perfective counterparts non-culminating, (11) and (12).

• nonCulminating : Marking
• culminating : Marking

@[instance_reducible]

instance Rett2020a.instDecidableEqMarking : DecidableEq Marking

Equations

• Rett2020a.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2020a.Marking.select {T : Type u_1} [LinearOrder T] : Marking → Set (NonemptyInterval T) → Set (NonemptyInterval T)

A marking selects a culmination's run times, or under a culminating marking their telos.

Equations

• Rett2020a.Marking.nonCulminating.select x✝ = x✝
• Rett2020a.Marking.culminating.select x✝ = Rett2020a.completive x✝

theorem Rett2020a.Marking.select_mem_readings {T : Type u_1} [LinearOrder T] (m : Marking) (p : Set (NonemptyInterval T)) : m.select p ∈ readings Class.culmination p

inductive Rett2020a.Bound : Type

The bound of the embedded eventuality a before clause is read against.

• initial : Bound
• final : Bound

@[instance_reducible]

instance Rett2020a.instDecidableEqBound : DecidableEq Bound

Equations

• Rett2020a.instDecidableEqBound x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2020a.Bound.time {T : Type u_1} [LinearOrder T] : Bound → NonemptyInterval T → T

The time of a bound of an interval.

Equations

• Rett2020a.Bound.initial.time x✝ = x✝.toProd.1
• Rett2020a.Bound.final.time x✝ = x✝.toProd.2

def Rett2020a.Marking.bound : Marking → Bound

A non-culminating marking reads before against the onset, a culminating one against the telos.

Equations

• Rett2020a.Marking.nonCulminating.bound = Rett2020a.Bound.initial
• Rett2020a.Marking.culminating.bound = Rett2020a.Bound.final

theorem Rett2020a.before_select {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) (i : NonemptyInterval T) (m : Marking) : before A (m.select {i}) ↔ ∃ t ∈ Tense.timeTrace A, t < m.bound.time i

Against a culmination, before under a marking is precedence of the bound the marking selects.

def Rett2020a.marking? (r : Datum) : Option Marking

The marking of a row's embedded clause.

Equations

• One or more equations did not get rendered due to their size.

def Rett2020a.bounds (r : Datum) : List Bound

The bounds a row's accepted readings are read against.

Equations

• One or more equations did not get rendered due to their size.

theorem Rett2020a.rows_marking (r : Datum) : r ∈ Examples.all → ∀ m ∈ marking? r, bounds r = [m.bound]

A marked before sentence has the one reading its marking selects.