Ogihara and Steinert-Threlkeld (2024): Limitations of a Modal Analysis of Before and After

Ogihara and Steinert-Threlkeld argue against Beaver and Condoravdi's branching-time analysis of before and propose an eventuality-based revision. After is veridical and before is not: Mozart died before he finished the Requiem is true although he never finished it. Over event predicates the asymmetry is quantificational, after being existential over both events and before universal over the complement, and whole-run-time precedence is strictly stronger than Anscombe's point-wise relation. Alternatives that branch only after the main-clause time cannot place a complement whose window closes at or before that time, as with Ohtani's tenth win, the first snow of 2020 and Nostradamus's prophecy. The revision relativizes world equivalence to an interval and an eventuality, and states the truth conditions of before as three cases, veridical, false and modal.

Main definitions

• eventAfter: after over event predicates.
• eventBefore: before over event predicates.
• equivIE: event-relative equivalence of worlds.
• OST.before: the revamped truth conditions of before.

Main results

• before_nonveridicality_derived: before is not veridical.
• not_eventBefore_of_anscombe: Anscombe's before is strictly weaker.
• bc_cannot_place_bounded_complement: forward-branching alternatives cannot place a bounded complement.
• histAlt_subset_altIE_trivial: the event-relative alternatives contain the branching ones.
• beforeCase_modal_nonveridical: the modal case is not veridical.

Implementation notes

The paper's third section draws a parallel between the modal case of before and the English progressive under the imperfective paradox; the parallel is not formalized here, the subinterval lemmas of Aspect stating the aspectual side on their own. The truth conditions of the fourth section are, in the paper's words, very weak and in need of strengthening by contextual and pragmatic factors; the fifth section's remaining problems for the revamped proposal, the non-committal readings that contextual plausibility governs, are recorded in the example rows only.

References

• [OST24]
• [BC03]
• [Ans64]
• [Hei74]
• [Lan92]

The connectives over event predicates: after is doubly existential — both events exist and the complement's run-time wholly precedes the main event's — while before is existential over the main clause and universal over the complement, so it is vacuously satisfied when no complement event exists.

def OgiharaSteinertThrelkeld2024.eventAfter {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] (P Q : E → Prop) : Prop

P after Q holds when some Q-event's run time wholly precedes some P-event's.

Equations

• OgiharaSteinertThrelkeld2024.eventAfter P Q = ∃ (e₁ : E) (e₂ : E), P e₁ ∧ Q e₂ ∧ (Event.τ e₂).Precedes (Event.τ e₁)

def OgiharaSteinertThrelkeld2024.eventBefore {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] (P Q : E → Prop) : Prop

P before Q holds when some P-event's run time wholly precedes every Q-event's.

Equations

• OgiharaSteinertThrelkeld2024.eventBefore P Q = ∃ (e₁ : E), P e₁ ∧ ∀ (e₂ : E), Q e₂ → (Event.τ e₁).Precedes (Event.τ e₂)

theorem OgiharaSteinertThrelkeld2024.after_veridicality_derived {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {P Q : E → Prop} (h : eventAfter P Q) : ∃ (e : E), Q e

After's veridicality follows from its double existential.

theorem OgiharaSteinertThrelkeld2024.before_nonveridicality_derived : ∃ (P : NonemptyInterval ℤ → Prop) (Q : NonemptyInterval ℤ → Prop), eventBefore P Q ∧ ¬∃ (e : NonemptyInterval ℤ), Q e

Before's non-veridicality follows from its universal, since any P-event with an empty Q satisfies it.

theorem OgiharaSteinertThrelkeld2024.eventBefore_veridical_main {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {P Q : E → Prop} (h : eventBefore P Q) : ∃ (e : E), P e

Both connectives commit to the main clause.

theorem OgiharaSteinertThrelkeld2024.anscombe_after_of_eventAfter {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {P Q : E → Prop} (h : eventAfter P Q) : Anscombe1964.Anscombe.after (Event.τ '' {e : E | P e}) (Event.τ '' {e : E | Q e})

The event-level after projects to [Ans64]'s on run-time denotations.

theorem OgiharaSteinertThrelkeld2024.anscombe_before_of_eventBefore {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {P Q : E → Prop} (h : eventBefore P Q) : Tense.beforeEver (Event.τ '' {e : E | P e}) (Event.τ '' {e : E | Q e})

The event-level before projects to [Ans64]'s quantificational one.

theorem OgiharaSteinertThrelkeld2024.not_eventBefore_of_anscombe : ¬∀ (P Q : NonemptyInterval ℤ → Prop), Tense.beforeEver (Event.τ '' {e : NonemptyInterval ℤ | P e}) (Event.τ '' {e : NonemptyInterval ℤ | Q e}) → eventBefore P Q

The projection is strict, since [Ans64]'s point-wise before allows the main run-time to reach into the complement's, which whole-run-time precedence forbids.

structure OgiharaSteinertThrelkeld2024.BCCounterexampleDatum : Type

A counterexample to Beaver and Condoravdi's branching-time analysis has a complement bounded to an interval that ends at or before the A-time, where alternatives branching only after that time cannot place it.

• sentence : String

  The example sentence.

• aTime : ℤ

  The A-clause time, such as the end of the season.

• complementUpperBound : ℤ

  The upper bound of the complement's temporal window.

• boundedBefore : self.complementUpperBound ≤ self.aTime

  The complement is bounded before the A-time.

• reading : BeaverCondoravdi2003.BeforeReading

  The reading of Beaver and Condoravdi at issue.

theorem OgiharaSteinertThrelkeld2024.bc_cannot_place_bounded_complement {W : Type u_3} (alt : HistoricalAlternatives W ℤ) (B : Set (W × ℤ)) (w : W) (tA hi : ℤ) (hBound : hi ≤ tA) (_hBounded : ∀ (w' : W) (t : ℤ), (w', t) ∈ B → t ≤ hi) (hNoFuture : ∀ w' ∈ alt (w, tA), ∀ (t : ℤ), (w', t) ∈ B → t ≤ hi) (te : ℤ) : te ∈ BeaverCondoravdi2003.instTimes (alt (w, tA)) B → te ≤ tA

When the complement is bounded at or before the A-time in every alternative at that time, no alternative instantiates it after the A-time, so Beaver and Condoravdi's forward branching cannot place a complement whose window closes before the A-time.

def OgiharaSteinertThrelkeld2024.ost_counterexample_ohtani : BCCounterexampleDatum

In (20a), Unfortunately, the 2021 MLB season will be over before Shohei Ohtani earns his 10th win of the season, uttered in mid-September 2021, the A-time is the end of the season, day 276, and Ohtani's tenth win can only occur before it.

Equations

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

def OgiharaSteinertThrelkeld2024.ost_counterexample_snow : BCCounterexampleDatum

In (20b), 2020 might come to an end before it snows for the first time this year, uttered on Christmas Day 2020, this year refers back to 2020, so the first snow can only occur in 2020 and no snow after the end of the year can witness the modal reading.

Equations

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

def OgiharaSteinertThrelkeld2024.ost_counterexample_nostradamus : BCCounterexampleDatum

In (20c), July 1999 will come to an end before Nostradamus' prophecy about the end of the world comes true, uttered minutes before the end of July 1999, the prophecy can only come true in July 1999.

Equations

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

The event-relative equivalence and alternatives (defs 17–18)

The paper's positive proposal replaces [BC03]'s world–time equivalence with one relative to an interval I and an eventuality e: alternative worlds must contain a counterpart of e that co-occurs with it up to I, and be identical at all earlier times.

@[reducible, inline]

abbrev OgiharaSteinertThrelkeld2024.Counterpart (W : Type u_5) (T : Type u_6) : Type (max u_5 u_6)

A counterpart relation relates eventualities across worlds that share essential properties such as starting time and thematic participants (fn. 18).

Equations

• OgiharaSteinertThrelkeld2024.Counterpart W T = (W → T → W → T → Prop)

def OgiharaSteinertThrelkeld2024.equivIE {W : Type u_3} {T : Type u_4} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (agree : T → W → W → Prop) (w₁ w₂ : W) (startI e₁_start : T) : Prop

Event-relative equivalence ≃_{I,e₁} (def 17) holds when a counterpart of e₁ exists in w₂, the two co-occur throughout [START(e₁), START(I)), and the worlds are identical at all earlier times.

Equations

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

def OgiharaSteinertThrelkeld2024.altIE {W : Type u_3} {T : Type u_4} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (agree : T → W → W → Prop) (w : W) (startI e_start : T) : Set W

The event-relative alternatives alt(w, I, e) (def 18a) are the worlds event-relatively equivalent to w.

Equations

• OgiharaSteinertThrelkeld2024.altIE counterpart coOccur agree w startI e_start = {w' : W | OgiharaSteinertThrelkeld2024.equivIE counterpart coOccur agree w w' startI e_start}

def OgiharaSteinertThrelkeld2024.eventContinuation {W : Type u_3} (alt : Set W) (continues : W → Prop) : Set W

Event continuation (def 18b) keeps only the alternatives in which the counterpart eventuality develops beyond I.

Equations

• OgiharaSteinertThrelkeld2024.eventContinuation alt continues = {w' : W | w' ∈ alt ∧ continues w'}

theorem OgiharaSteinertThrelkeld2024.equivIE_downward_closed {W : Type u_3} {T : Type u_4} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (coOccur_mono : ∀ (w₁ : W) (e₁ : T) (w₂ : W) (e₂ s₁ s₂ s₂' : T), s₂' ≤ s₂ → coOccur w₁ e₁ w₂ e₂ s₁ s₂ → coOccur w₁ e₁ w₂ e₂ s₁ s₂') (agree : T → W → W → Prop) (w₁ w₂ : W) (startI startI' e_start : T) (hle : startI' ≤ startI) (h : equivIE counterpart coOccur agree w₁ w₂ startI e_start) : equivIE counterpart coOccur agree w₁ w₂ startI' e_start

Event-relative equivalence is downward closed (def 18c), equivalence at I implying equivalence at any earlier I'.

theorem OgiharaSteinertThrelkeld2024.equivIE_trivial_iff_agree {W : Type u_3} {T : Type u_4} [LinearOrder T] (agree : T → W → W → Prop) (w₁ w₂ : W) (startI e_start : T) : equivIE (fun (x : W) (x_1 : T) (x_2 : W) (x_3 : T) => True) (fun (x : W) (x_1 : T) (x_2 : W) (x_3 x_4 x_5 : T) => True) agree w₁ w₂ startI e_start ↔ ∀ t' < e_start, agree t' w₁ w₂

With trivial counterpart and co-occurrence, ≃_{I,e} is agreement at all earlier times, Beaver and Condoravdi's initial branch point condition for a pair of worlds.

theorem OgiharaSteinertThrelkeld2024.histAlt_subset_altIE_trivial {W : Type u_3} {T : Type u_4} [LinearOrder T] {F : Temporal.TWFrame W T} {B : Set (W × T)} (a : BeaverCondoravdi2003.Alternatives F B) (w : W) (t : T) : a.alt (w, t) ⊆ altIE (fun (x : W) (x_1 : T) (x_2 : W) (x_3 : T) => True) (fun (x : W) (x_1 : T) (x_2 : W) (x_3 x_4 x_5 : T) => True) (fun (t : T) => ⇑(F.sim t)) w t t

Beaver and Condoravdi's alternatives over a T × W frame land inside the trivial event-relative alternatives for agreement by the frame, so the event-relative equivalence generalizes Beaver and Condoravdi's.

The revamped truth conditions for before (def 19) use the event-relative alternatives and a CAUSE relation. At ⟨w₀, I₀, e₀⟩ where A holds, ⟦A before B⟧ is true when B holds at a later interval in w₀ (case i), false when B holds at an interval at or before I₀ in w₀ (case ii), and otherwise true when I₀ precedes an interval at which, in an alternative for an eventuality ongoing at I₀, the continuation of its counterpart causes a B-eventuality (case iii).

def OgiharaSteinertThrelkeld2024.abuts {T : Type u_4} [LinearOrder T] (I₀ I₁ : NonemptyInterval T) : Prop

Two intervals abut when the first ends where the second begins.

Equations

• OgiharaSteinertThrelkeld2024.abuts I₀ I₁ = (I₀.toProd.2 = I₁.toProd.1)

def OgiharaSteinertThrelkeld2024.holdsAtAbutting {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] (e₁ : E) (I₀ : NonemptyInterval T) : Prop

holdsAtAbutting e₁ I₀ says that the run time of e₁ contains the start of I₀, so that e₁ is ongoing at I₀.

Equations

• OgiharaSteinertThrelkeld2024.holdsAtAbutting e₁ I₀ = ((Event.τ e₁).toProd.1 ≤ I₀.toProd.1 ∧ I₀.toProd.1 ≤ (Event.τ e₁).toProd.2)

@[reducible, inline]

abbrev OgiharaSteinertThrelkeld2024.SitDenot (W : Type u_6) (T : Type u_7) (E : Type u_8) [LinearOrder T] : Type (max (max u_8 u_7) u_6)

A situation denotation is a set of world–interval–eventuality triples.

Equations

• OgiharaSteinertThrelkeld2024.SitDenot W T E = Set (W × NonemptyInterval T × E)

def OgiharaSteinertThrelkeld2024.beforeCase_veridical {W : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] (A B : SitDenot W T E) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : Prop

In case (i), ⟦A before B⟧ is true because B holds at some interval after I₀ in the actual world w₀.

Equations

• OgiharaSteinertThrelkeld2024.beforeCase_veridical A B w₀ I₀ e₀ = ((w₀, I₀, e₀) ∈ A ∧ ∃ (I₂ : NonemptyInterval T), I₀.toProd.2 < I₂.toProd.1 ∧ ∃ (e₄ : E), (w₀, I₂, e₄) ∈ B)

def OgiharaSteinertThrelkeld2024.beforeCase_false {W : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] (A B : SitDenot W T E) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : Prop

In case (ii), ⟦A before B⟧ is false because B holds at some interval at or before I₀ in the actual world w₀.

Equations

• OgiharaSteinertThrelkeld2024.beforeCase_false A B w₀ I₀ e₀ = ((w₀, I₀, e₀) ∈ A ∧ ∃ (I₂ : NonemptyInterval T), I₂.toProd.2 ≤ I₀.toProd.1 ∧ ∃ (e₅ : E), (w₀, I₂, e₅) ∈ B)

def OgiharaSteinertThrelkeld2024.beforeCase_modal {W : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] (A B : SitDenot W T E) (alt : W → NonemptyInterval T → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : Prop

In the modal case (iii), ⟦A before B⟧ is true when A holds at ⟨w₀,I₀,e₀⟩ and I₀ precedes an interval I₁ at which, in an alternative w₁ for an eventuality e₁ ongoing at I₀, a counterpart of e₁ causes an eventuality e₃ with ⟨w₁, I₁, e₃⟩ ∈ ⟦B⟧.

Equations

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

def OgiharaSteinertThrelkeld2024.OST.before {W : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] (A B : SitDenot W T E) (alt : W → NonemptyInterval T → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : Prop

The revamped before (def 19) holds when case (ii) fails and case (i) or the modal case (iii) holds.

Equations

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

theorem OgiharaSteinertThrelkeld2024.beforeCase_veridical_entails_complement {W : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] (A B : SitDenot W T E) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : beforeCase_veridical A B w₀ I₀ e₀ → ∃ (I : NonemptyInterval T) (e : E), (w₀, I, e) ∈ B

Case (i) is veridical, the complement occurring after I₀ in the actual world.

theorem OgiharaSteinertThrelkeld2024.beforeCase_modal_nonveridical : ∃ (A : SitDenot Bool ℤ (NonemptyInterval ℤ)) (B : SitDenot Bool ℤ (NonemptyInterval ℤ)) (alt : Bool → NonemptyInterval ℤ → NonemptyInterval ℤ → Set Bool) (cause : Bool → NonemptyInterval ℤ → NonemptyInterval ℤ → Prop) (counterpart : Bool → NonemptyInterval ℤ → Bool → NonemptyInterval ℤ → Prop) (w₀ : Bool) (I₀ : NonemptyInterval ℤ) (e₀ : NonemptyInterval ℤ), beforeCase_modal A B alt cause counterpart w₀ I₀ e₀ ∧ ¬∃ (I : NonemptyInterval ℤ) (e : NonemptyInterval ℤ), (w₀, I, e) ∈ B

The modal case is not veridical, as a model shows in which the main clause holds only at the actual world false and the complement only at the alternative true.

theorem OgiharaSteinertThrelkeld2024.cases_i_ii_exclusive {T : Type u_4} [LinearOrder T] (I₀ I_B : NonemptyInterval T) (hAfter : I₀.toProd.2 < I_B.toProd.1) (hBefore : I_B.toProd.2 ≤ I₀.toProd.1) : False

Cases (i) and (ii) exclude each other for a complement at a single interval, which cannot lie both after and before I₀.

theorem OgiharaSteinertThrelkeld2024.mozart_is_case_iii {W : Type u_6} {E : Type u_7} [Event.TemporalTrace E ℤ] (A B : SitDenot W ℤ E) (alt : W → NonemptyInterval ℤ → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : NonemptyInterval ℤ) (e₀ : E) (hNoFinish : ¬∃ (I : NonemptyInterval ℤ) (e : E), (w₀, I, e) ∈ B) (hModal : beforeCase_modal A B alt cause counterpart w₀ I₀ e₀) : OST.before A B alt cause counterpart w₀ I₀ e₀

With no finishing in the actual world and the modal case holding, the revamped before holds, so Mozart died before he finished the Requiem has the anti-veridical reading of case (iii).