[OST24] — Data

[OST24]

Theory-neutral empirical data on the veridicality asymmetry between temporal connectives before and after.

Key Empirical Generalizations

1. After is veridical: "He left after she arrived" entails "she arrived".
2. Before is non-veridical: "He left before she arrived" is compatible with her not arriving (the "barely prevented" reading).
3. Before is non-veridical even with perfective complements: "The bomb exploded before anyone defused it" does not entail anyone defused it.

Data Sources

• Ogihara, T. & Steinert-Threlkeld, S. (2024), §2–3.
• Anscombe, E. (1964), §3 (original observation of the asymmetry).
• Beaver, D. & Condoravdi, C. (2003), §2 (three readings of before).

def OgiharaSteinertThrelkeld2024.flagOf (e : Data.Examples.LinguisticExample) (k : String) : Bool

A paperFeatures flag read as a Bool (true iff the value is "true").

Equations

• OgiharaSteinertThrelkeld2024.flagOf e k = (e.feature? k == some "true")

structure OgiharaSteinertThrelkeld2024.VeridicalityDatum : Type

An empirical judgment about whether a temporal connective entails the truth of its complement clause. Stimuli live in Data/Examples/OgiharaSteinertThrelkeld2024.json (generated OgiharaSteinertThrelkeld2024.Examples); this record is derived from a LinguisticExample by ofVeridicality.

• sentence : String

  The example sentence

• connective : String

  The temporal connective

• complementEntailed : Bool

  Does the sentence entail that the complement event occurred?

• gloss : String

  Brief gloss of the entailment pattern

@[implicit_reducible]

instance OgiharaSteinertThrelkeld2024.instReprVeridicalityDatum : Repr VeridicalityDatum

Equations

• OgiharaSteinertThrelkeld2024.instReprVeridicalityDatum = { reprPrec := OgiharaSteinertThrelkeld2024.instReprVeridicalityDatum.repr }

def OgiharaSteinertThrelkeld2024.instReprVeridicalityDatum.repr : VeridicalityDatum → ℕ → Std.Format

Equations

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

def OgiharaSteinertThrelkeld2024.ofVeridicality (e : Data.Examples.LinguisticExample) : VeridicalityDatum

Derive a VeridicalityDatum from a generated LinguisticExample: the sentence is the primaryText; the connective and complement-entailment are paperFeatures tags.

Equations

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

def OgiharaSteinertThrelkeld2024.after_veridical : VeridicalityDatum

"He left after she arrived" entails "she arrived".

Equations

• OgiharaSteinertThrelkeld2024.after_veridical = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_after_veridical

def OgiharaSteinertThrelkeld2024.before_nonveridical : VeridicalityDatum

"He left before she arrived" does NOT entail "she arrived" (compatible with the veridical, counterfactual, or non-committal reading).

Equations

• OgiharaSteinertThrelkeld2024.before_nonveridical = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_before_nonveridical

def OgiharaSteinertThrelkeld2024.before_counterfactual : VeridicalityDatum

"The bomb exploded before anyone defused it" — counterfactual before: the defusing did not occur ([BC03], "barely prevented").

Equations

• OgiharaSteinertThrelkeld2024.before_counterfactual = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_before_counterfactual

def OgiharaSteinertThrelkeld2024.after_veridical_2 : VeridicalityDatum

"She finished her coffee after he left" entails "he left".

Equations

• OgiharaSteinertThrelkeld2024.after_veridical_2 = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_after_veridical_2

def OgiharaSteinertThrelkeld2024.before_noncommittal : VeridicalityDatum

"I left the party before there was any trouble" — non-committal ([BC03], ex. 43; B&C's (22) Supreme Court case is counterfactual).

Equations

• OgiharaSteinertThrelkeld2024.before_noncommittal = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_before_noncommittal

def OgiharaSteinertThrelkeld2024.before_counterfactual_mozart : VeridicalityDatum

"Mozart died before he finished the Requiem" — counterfactual ([BC03], ex. 24).

Equations

• OgiharaSteinertThrelkeld2024.before_counterfactual_mozart = OgiharaSteinertThrelkeld2024.ofVeridicality OgiharaSteinertThrelkeld2024.Examples.ost2024_before_counterfactual_mozart

structure OgiharaSteinertThrelkeld2024.BCCounterexampleDatum : Type

A counterexample to B&C's branching-time analysis. In each case, the complement eventuality is temporally bounded to an interval that ends at or before the A-time. B&C's alt(w,t) branches only after t, so it cannot place the complement in an alternative world at a time after the A-time.

The boundedBefore field captures the formal crux: the complement's temporal bound ends at or before the A-time.

• sentence : String

  The example sentence

• aTime : ℤ

  The A-clause time (e.g., end of MLB season, end of 2020)

• complementUpperBound : ℤ

  Upper bound of the complement's temporal window

• boundedBefore : self.complementUpperBound ≤ self.aTime

  The complement is temporally bounded before the A-time

• reading : Tense.TemporalConnectives.BeaverCondoravdi.BeforeReading

  Which B&C reading is involved?

theorem OgiharaSteinertThrelkeld2024.bc_cannot_place_bounded_complement {W : Type u_1} (alt : Tense.TemporalConnectives.BeaverCondoravdi.HistAlt 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 ∈ Tense.TemporalConnectives.BeaverCondoravdi.instTimes (alt w tA) B → te ≤ tA

B&C's before requires earliestAlt to find a B-instantiation in some alternative world. When B is temporally bounded to [lo, hi] with hi ≤ tA, and alt(w,tA) only contains worlds that agree with w up to tA, B cannot be instantiated after tA in any alternative.

This is the formal content of O&ST's §5.1 critique: B&C's forward- branching architecture cannot handle complements whose temporal bound falls before the A-time.

def OgiharaSteinertThrelkeld2024.ost_counterexample_ohtani : BCCounterexampleDatum

(20a) "Unfortunately, the 2021 MLB season will be over before Shohei Ohtani earns his 10th win of the season." (Uttered in the middle of September 2021.) The A-time is the end of the 2021 MLB season (October 3, 2021 = day 276). The complement (Ohtani's 10th win) can only occur during the season (before day 276). (O&[OST24], §5.1, ex. 20a)

Equations

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

def OgiharaSteinertThrelkeld2024.ost_counterexample_snow : BCCounterexampleDatum

(20b) "2020 might come to an end before it snows for the first time this year." (Uttered on Christmas Day in 2020.) The expression this year refers back to 2020. Since the first snow of 2020 can only occur in 2020, the modal proposal that posits a fictitious snow event after the end of 2020 does not work. (O&[OST24], §5.1, ex. 20b)

Equations

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

def OgiharaSteinertThrelkeld2024.ost_counterexample_nostradamus : BCCounterexampleDatum

(20c) "July 1999 will come to an end before Nostradamus' prophecy about the end of the world comes true." (Uttered a few minutes before the end of July 1999. Assumes Michel de Nostradamus predicted that in July 1999, a great King of terror would come from the sky and destroy the world.) The prophecy can only come true if the world is destroyed in July 1999 — it cannot come true after the end of July 1999. (O&[OST24], §5.1, ex. 20c)

Equations

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

structure OgiharaSteinertThrelkeld2024.NonCommittalDatum : Type

A datum recording asymmetries in the availability of non-committal readings, which B&C's Event Continuation Condition should but cannot fully predict.

• sentence : String

  The example sentence

• nonCommittalAvailable : Bool

  Is the non-committal reading available?

• explanation : String

  Why the availability is as it is

def OgiharaSteinertThrelkeld2024.instReprNonCommittalDatum.repr : NonCommittalDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance OgiharaSteinertThrelkeld2024.instReprNonCommittalDatum : Repr NonCommittalDatum

Equations

• OgiharaSteinertThrelkeld2024.instReprNonCommittalDatum = { reprPrec := OgiharaSteinertThrelkeld2024.instReprNonCommittalDatum.repr }

def OgiharaSteinertThrelkeld2024.ofNonCommittal (e : Data.Examples.LinguisticExample) : NonCommittalDatum

Derive a NonCommittalDatum from a generated LinguisticExample.

Equations

• OgiharaSteinertThrelkeld2024.ofNonCommittal e = { sentence := e.primaryText, nonCommittalAvailable := OgiharaSteinertThrelkeld2024.flagOf e "noncommittal_available", explanation := e.comment }

def OgiharaSteinertThrelkeld2024.noncommittal_available : NonCommittalDatum

"Mary will leave the party before Bill gets drunk" — non-committal reading available (getting drunk is a normal continuation). (O&[OST24], §5.2)

Equations

• OgiharaSteinertThrelkeld2024.noncommittal_available = OgiharaSteinertThrelkeld2024.ofNonCommittal OgiharaSteinertThrelkeld2024.Examples.ost2024_noncommittal_available

def OgiharaSteinertThrelkeld2024.noncommittal_unavailable : NonCommittalDatum

"Mary will leave the party before Quebec becomes an independent country" — non-committal reading unavailable (Quebec independence is not a normal continuation); B&C's Event Continuation Condition should block this. (O&[OST24], §5.2)

Equations

• OgiharaSteinertThrelkeld2024.noncommittal_unavailable = OgiharaSteinertThrelkeld2024.ofNonCommittal OgiharaSteinertThrelkeld2024.Examples.ost2024_noncommittal_unavailable

theorem OgiharaSteinertThrelkeld2024.noncommittal_plausibility_sensitive : noncommittal_available.nonCommittalAvailable = true ∧ noncommittal_unavailable.nonCommittalAvailable = false

The non-committal reading is sensitive to contextual plausibility: available when the complement is a normal continuation, unavailable when it is pragmatically impossible.

structure OgiharaSteinertThrelkeld2024.CrossLinguisticDatum : Type

Cross-linguistic morphological evidence for the veridicality asymmetry.

• language : String

  Language

• connective : String

  The temporal connective (in the object language)

• gloss : String

  English gloss

• observation : String

  Key morphological observation

• supportsNonveridicality : Bool

  Does this support the non-veridical analysis of before?

@[implicit_reducible]

instance OgiharaSteinertThrelkeld2024.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

• OgiharaSteinertThrelkeld2024.instReprCrossLinguisticDatum = { reprPrec := OgiharaSteinertThrelkeld2024.instReprCrossLinguisticDatum.repr }

def OgiharaSteinertThrelkeld2024.instReprCrossLinguisticDatum.repr : CrossLinguisticDatum → ℕ → Std.Format

Equations

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

def OgiharaSteinertThrelkeld2024.japanese_mae : CrossLinguisticDatum

Japanese mae ('before') requires non-past tense in its complement, even when describing past events. This independently supports the non-veridical analysis: the complement is presented as unrealized from the perspective of the main-clause event. (O&[OST24], §3)

Equations

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

def OgiharaSteinertThrelkeld2024.japanese_ato : CrossLinguisticDatum

Japanese ato ('after') allows past tense in its complement, consistent with the veridical analysis: the complement event is presented as having occurred. (O&[OST24], §3)

Equations

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

theorem OgiharaSteinertThrelkeld2024.japanese_tense_mirrors_veridicality : japanese_mae.supportsNonveridicality = true ∧ japanese_ato.supportsNonveridicality = false

The Japanese tense asymmetry mirrors the veridicality asymmetry: mae (non-past complement) patterns with non-veridical before, ato (past complement) patterns with veridical after.

theorem OgiharaSteinertThrelkeld2024.after_data_veridical : after_veridical.complementEntailed = true ∧ after_veridical_2.complementEntailed = true

After is uniformly veridical across examples.

theorem OgiharaSteinertThrelkeld2024.before_data_nonveridical : before_nonveridical.complementEntailed = false ∧ before_counterfactual.complementEntailed = false ∧ before_noncommittal.complementEntailed = false ∧ before_counterfactual_mozart.complementEntailed = false

Before is uniformly non-veridical across all examples.

theorem OgiharaSteinertThrelkeld2024.veridicality_asymmetry : after_veridical.complementEntailed ≠ before_nonveridical.complementEntailed

The asymmetry: after and before differ on complement entailment.

theorem OgiharaSteinertThrelkeld2024.after_fragment_matches_datum : English.TemporalExpressions.after_.complementVeridical = after_veridical.complementEntailed

The Fragment entry for after matches the empirical datum: both record complement veridicality as true.

theorem OgiharaSteinertThrelkeld2024.before_fragment_matches_datum : English.TemporalExpressions.before_.complementVeridical = before_nonveridical.complementEntailed

The Fragment entry for before matches the empirical datum: both record complement veridicality as false.

theorem OgiharaSteinertThrelkeld2024.fragment_veridicality_asymmetry : English.TemporalExpressions.after_.complementVeridical = true ∧ English.TemporalExpressions.before_.complementVeridical = false

The veridicality asymmetry is reflected in the Fragment entries.

theorem OgiharaSteinertThrelkeld2024.after_veridicality_derived (P Q : Event ℤ → Prop) : Tense.TemporalConnectives.AnscombeEvent.after P Q → ∃ (e : Event ℤ), Q e

O&ST's theory derives after's veridicality from the double-existential quantificational structure: ∃e₁∃e₂[P(e₁) ∧ Q(e₂) ∧...] entails ∃e₂, Q(e₂).

This is not a stipulation in the Fragment — it follows from the semantics.

theorem OgiharaSteinertThrelkeld2024.before_nonveridicality_derived : ∃ (P : Event ℤ → Prop) (Q : Event ℤ → Prop), Tense.TemporalConnectives.AnscombeEvent.before P Q ∧ ¬∃ (e : Event ℤ), Q e

O&ST's theory derives before's non-veridicality from the universal quantification over the complement: ∃e₁[P(e₁) ∧ ∀e₂[Q(e₂) →...]] is vacuously true when Q has no witnesses.

Concretely: any P-event with an empty Q yields before(P, Q).

theorem OgiharaSteinertThrelkeld2024.scenario_after_punctual : have leave := { runtime := { fst := 1, snd := 1, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; have arrive := { runtime := { fst := 0, snd := 0, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; Tense.TemporalConnectives.AnscombeEvent.after (fun (x : Event ℤ) => x = leave) fun (x : Event ℤ) => x = arrive

Scenario: "He left₁ after she arrived₀" with punctual events.

• leaving event at time 1
• arriving event at time 0 O&ST predicts: after(leave, arrive) holds (τ(arrive) ≺ τ(leave)).

theorem OgiharaSteinertThrelkeld2024.scenario_before_punctual : have leave := { runtime := { fst := 1, snd := 1, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; have arrive := { runtime := { fst := 3, snd := 3, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; Tense.TemporalConnectives.AnscombeEvent.before (fun (x : Event ℤ) => x = leave) fun (x : Event ℤ) => x = arrive

Scenario: "He left₁ before she arrived₃" with punctual events.

• leaving event at time 1
• arriving event at time 3 O&ST predicts: before(leave, arrive) holds (τ(leave) ≺ τ(arrive)).

theorem OgiharaSteinertThrelkeld2024.scenario_before_counterfactual : have explode := { runtime := { fst := 5, snd := 5, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; Tense.TemporalConnectives.AnscombeEvent.before (fun (x : Event ℤ) => x = explode) fun (x : Event ℤ) => False

Scenario: "The bomb exploded₅ before anyone defused it" (nobody defused it). O&ST predicts: before(explode, defuse) holds vacuously (no defuse-events).

theorem OgiharaSteinertThrelkeld2024.scenario_after_projects : have leave := { runtime := { fst := 1, snd := 1, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; have arrive := { runtime := { fst := 0, snd := 0, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; Tense.TemporalConnectives.Anscombe.after (eventDenotation fun (x : Event ℤ) => x = leave) (eventDenotation fun (x : Event ℤ) => x = arrive)

The punctual after-scenario projects correctly through eventDenotation: O&ST.after implies Anscombe.after on the projected interval sets.

theorem OgiharaSteinertThrelkeld2024.scenario_before_projects : have leave := { runtime := { fst := 1, snd := 1, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; have arrive := { runtime := { fst := 3, snd := 3, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }; Tense.TemporalConnectives.Anscombe.before (eventDenotation fun (x : Event ℤ) => x = leave) (eventDenotation fun (x : Event ℤ) => x = arrive)

The punctual before-scenario projects correctly through eventDenotation.

theorem OgiharaSteinertThrelkeld2024.japanese_mae_matches_datum : Japanese.TemporalConnectives.mae.complementVeridical = false ∧ japanese_mae.supportsNonveridicality = true

The Japanese Fragment entry for mae agrees with the cross-linguistic datum: both record that mae supports the non-veridicality analysis.

theorem OgiharaSteinertThrelkeld2024.japanese_ato_matches_datum : Japanese.TemporalConnectives.ato.complementVeridical = true ∧ japanese_ato.supportsNonveridicality = false

The Japanese Fragment entry for ato agrees with the cross-linguistic datum: ato is veridical and does not support non-veridicality.

[OST24] §3 observe that the progressive and anti-veridical before share the same modal-temporal structure:

- **Progressive** "Mozart was composing the Requiem (when he died)":
  at the reference time, there is an ongoing event (composing) that in
  some **inertia worlds** ([landman-1992]) reaches completion.

- **Anti-veridical before** "Mozart died before he finished the Requiem":
  at the A-time, there is an ongoing event (composing) that in some
  **historical alternatives** reaches the before-clause eventuality
  (finishing).

Both reduce to: ∃ event e ongoing at t such that in some accessible
world w', the continuation of e leads to a target outcome.

The formal parallel:
- `IMPF P w t` ↔ ∃ e, t ⊂ τ(e) ∧ P w e  (event extends beyond t)
- `alt(w,t)` contains worlds where the counterpart of e develops
  beyond t (event continuation condition, def 18b)

This structural identity is captured by the following bridge: given
an IMPF predication and an "inertia" alternative set, the reference time
sits inside the event's runtime in the actual world, while alternatives
contain worlds where the continuation reaches a target. 

Imperfective paradox ↔ before non-veridicality: shared vacuous-∀ structure.

Both arise from a universal quantification that can be vacuously satisfied:

• Before's non-veridicality: ∀ e₂, Q(e₂) → τ(e₁) ≺ τ(e₂) is vacuously true when no Q-event exists. The complement need not occur.

• Imperfective paradox: For accomplishments lacking CSIP, IMPF P w t does not entail PRFV P w t — the event is ongoing at t but the telos (completion) may not be reached. The universal quantification over subintervals that CSIP would provide is absent.

Both are "resolved" modally in the same way:

• Progressive: in inertia worlds, the ongoing event reaches completion
• Anti-veridical before: in historical alternatives, the complement event occurs

The following theorems make this structural parallel precise.

theorem OgiharaSteinertThrelkeld2024.csip_entails_completion {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (hCSIP : Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P) (w : W) (t : NonemptyInterval Time) : Semantics.Aspect.IMPF P w t → Semantics.Aspect.PRFV P w t

CSIP predicates are "before-veridical": if P has the closed subinterval property, then IMPF(P)(w)(t) guarantees P-completion at t (PRFV). This is the aspectual analogue of after's veridicality — both arise from existential (not universal) quantificational structure.

Formally: CSIP(P) → IMPF(P)(w)(t) → PRFV(P)(w)(t). This is impf_entails_prfv_of_csub from SubintervalProperty.lean.

theorem OgiharaSteinertThrelkeld2024.non_csip_lacks_completion {W : Type u_1} (w : W) (t₁ t₂ : ℤ) (hlt : t₁ < t₂) : ¬∀ (P : W → Event ℤ → Prop), Semantics.Aspect.SubintervalProperty.HasSubintervalProp P

Non-CSIP predicates may lack completion: the imperfective paradox shows that not all predicates support the IMPF→PRFV entailment. This is the aspectual analogue of before's non-veridicality — both arise from a universal quantification (over subintervals / over complement events) that can be vacuously satisfied.

Formally: ¬(∀ P, HasSubintervalProp P). This is imperfective_paradox_possible from SubintervalProperty.lean.

theorem OgiharaSteinertThrelkeld2024.progressive_before_modal_resolution {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P Q : W → Event Time → Prop) (alternatives : Event Time → Set W) (w : W) (t : NonemptyInterval Time) (hIMPF : Semantics.Aspect.IMPF P w t) (hContinuation : ∀ (e : Event Time), P w e → t < e.τ → ∀ w' ∈ alternatives e, ∃ (e' : Event Time), Q w' e') : ∃ (e : Event Time), t < e.τ ∧ P w e ∧ ∀ w' ∈ alternatives e, ∃ (e' : Event Time), Q w' e'

Progressive–before modal resolution: When P lacks CSIP (accomplishment), IMPF(P)(w)(t) gives an ongoing event e that does not (yet) satisfy PRFV. The progressive "resolves" this by positing inertia worlds where the continuation of e reaches a target Q. Anti-veridical before does the same with historical alternatives.

This theorem captures the shared structure: given an IMPF predication and a modal accessibility relation (alternatives) that maps ongoing events to worlds where a target Q is reached, there exists an ongoing event whose continuation satisfies Q in accessible worlds.

theorem OgiharaSteinertThrelkeld2024.csip_determines_modal_need {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : (Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P → Semantics.Aspect.IMPF P w t → Semantics.Aspect.PRFV P w t) ∧ (Semantics.Aspect.IMPF P w t → ¬Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P → (¬∀ t' ≤ t, ∃ (e : Event Time), e.τ = t' ∧ P w e) → ∃ (e : Event Time), t < e.τ ∧ P w e)

The parallel is precise: the progressive and anti-veridical before have identical formal structure. Progressive: IMPF(P)(w)(t) + inertia(e) → Q reachable. Before (anti-veridical): ongoing event at A-time + alt(w,I,e) → complement reachable. The only difference is the name of the accessibility relation (inertia vs historical alternatives).

This theorem shows that CSIP is the dividing line: predicates WITH CSIP don't need modal resolution (IMPF directly entails PRFV, like after directly entails its complement). Predicates WITHOUT CSIP require modal resolution (the progressive / anti-veridical before).

The paper's central formal contribution: revamped truth conditions for before that incorporate eventuality-relative alternatives (def 18) and a CAUSE relation. Three cases for ⟦A before B⟧ evaluated at ⟨w₀, I₀, e₀⟩:

**(i) Definitely true (veridical)**: A holds at ⟨w₀,I₀,e₀⟩ AND B already
holds at some later interval I₂ > I₀ in w₀. The complement already
occurred after A — straightforwardly true.

**(ii) Definitely false**: A holds at ⟨w₀,I₀,e₀⟩ AND B already holds at
some interval I₂ ≤ I₀ in w₀. The complement already occurred before/at
A — so A is NOT before B.

**(iii) Modal case (anti-veridical / non-committal)**: A holds at
⟨w₀,I₀,e₀⟩ and I₀ precedes the earliest I₁ such that ∃ eventuality e₁
ongoing at I₀ in w₀, ∃ world w₁ ∈ alt(w₀,I₀,e₁), ∃ e₂ counterpart of
e₁ in w₁, the continuation of e₂ CAUSES an eventuality e₃ with
⟨w₁,I₁,e₃⟩ ∈ ⟦B⟧.

The authors note these truth conditions are "very weak and need to be
strengthened by some contextual and pragmatic factors." 

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

Two intervals abut: the first ends where the second begins (no gap).

Equations

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

def OgiharaSteinertThrelkeld2024.holdsAtAbutting {T : Type u_2} {E : Type u_3} [LinearOrder T] (runtime : E → NonemptyInterval T) (e₁ : E) (I₀ : NonemptyInterval T) : Prop

An eventuality e₁ "holds throughout" an interval that abuts I₀: e₁'s runtime extends from before I₀ through to (at least) I₀'s start.

Equations

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

@[reducible, inline]

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

Denotation type for O&ST's truth conditions: sets of world–interval–eventuality triples.

Equations

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

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

Case (i): ⟦A before B⟧ = 1 when the complement B already 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_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (A B : SitDenot W T E) (w₀ : W) (I₀ : NonemptyInterval T) (e₀ : E) : Prop

Case (ii): ⟦A before B⟧ = 0 when the complement B already 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_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (A B : SitDenot W T E) (runtime : E → NonemptyInterval T) (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

Case (iii): The modal case. ⟦A before B⟧ = 1 when A holds at ⟨w₀,I₀,e₀⟩ and I₀ precedes the earliest I₁ such that:

• there is an eventuality e₁ in w₀ whose runtime abuts I₀,
• there is an alternative world w₁ ∈ alt(w₀, I₀, e₁),
• in w₁, the counterpart e₂ of e₁ continues and CAUSES an eventuality e₃,
• ⟨w₁, I₁, e₃⟩ ∈ ⟦B⟧.

Equations

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

def OgiharaSteinertThrelkeld2024.OST.before {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (A B : SitDenot W T E) (runtime : E → NonemptyInterval T) (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

O&ST's revamped before (def 19): the disjunction of the three cases. Evaluated at ⟨w₀, I₀, e₀⟩, "A before B" is true iff either:

• (i) B already occurred after I₀ (veridical), or
• (iii) The modal case via alt(w₀,I₀,e₁) + CAUSE holds, AND case (ii) does not hold (B did not already occur before I₀).

Equations

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

theorem OgiharaSteinertThrelkeld2024.beforeCase_veridical_entails_complement {W : Type u_1} {T : Type u_2} {E : Type u_3} [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: when the complement has already occurred (after I₀), the complement is instantiated in the actual world.

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

Case (iii) is non-veridical: the complement need not be instantiated in w₀ — it may only exist in an alternative world w₁.

Scenario: w₀ = false (actual), w₁ = true (alternative). A = {(false, [0,0], ())} — main clause holds only in w₀. B = {(true, [2,2], ())} — complement holds only in w₁. The modal case holds because alt gives w₁, with trivial cause/counterpart. But B has no witness in w₀.

theorem OgiharaSteinertThrelkeld2024.cases_i_ii_exclusive {T : Type u_2} [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) are mutually exclusive when the complement occurs at a single interval: it cannot be both before and after I₀.

theorem OgiharaSteinertThrelkeld2024.mozart_is_case_iii {W : Type u_4} {E : Type u_5} (A B : SitDenot W ℤ E) (runtime : E → NonemptyInterval ℤ) (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 runtime alt cause counterpart w₀ I₀ e₀) : OST.before A B runtime alt cause counterpart w₀ I₀ e₀

The Mozart scenario: "Mozart died before he finished the Requiem." This is the anti-veridical reading (case iii). Mozart's death (e₀) is at I₀. In some alternative world w₁, Mozart's composing (e₁, ongoing at I₀) has a counterpart e₂ whose continuation CAUSES a finishing event e₃ at I₁. B ("finishing the Requiem") holds at ⟨w₁, I₁, e₃⟩ but NOT in w₀.

Veridicality ↔ Presupposition Bridge

[BC03] [Hei83] [OST24]

Connects three layers of the temporal connective formalization:

1. Fragment field: TemporalExprEntry.complementVeridical : Bool
2. Theory proof: e.g., Anscombe.after A B → ∃ t, t ∈ timeTrace B
3. Presupposition theory: veridical connectives presuppose their complement (modeled as PartialProp with complement occurrence as presupposition)

For each temporal connective, the Fragment's complementVeridical field is grounded in a theory-level proof, and matches the empirical data.

Veridical connectives

For each connective with complementVeridical = true, the theory proves that the connective entails the existence of a complement witness.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.after_veridicality_grounded : English.TemporalExpressions.after_.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Anscombe.after A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

after is veridical: Fragment field matches theory proof. Theory: Anscombe.after A B → ∃ t, t ∈ timeTrace B. Fragment: after_.complementVeridical = true.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.when_veridicality_grounded : English.TemporalExpressions.when_conn.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.when_ A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

when is veridical: Fragment field matches theory proof.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.until_veridicality_grounded : English.TemporalExpressions.until_.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.until A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

until (durative) is veridical: Fragment field matches theory proof.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.since_veridicality_grounded : English.TemporalExpressions.since_conn.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.since A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

since is veridical: Fragment field matches theory proof.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.by_veridicality_grounded : English.TemporalExpressions.by_deadline.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.by_ A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace A

by is veridical w.r.t. its main clause: Fragment field matches theory proof.

Non-veridical connectives

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.before_nonveridicality_grounded : English.TemporalExpressions.before_.complementVeridical = false ∧ ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Anscombe.before A B ∧ ¬∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

before is non-veridical: Fragment field matches theory counterexample. The counterexample uses A = {point(0)}, B = ∅: "A before nothing" is vacuously true because ∀t'∈∅, 0 < t'.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.after_fragment_matches_data : English.TemporalExpressions.after_.complementVeridical = after_veridical.complementEntailed

Fragment matches data for after.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.before_fragment_matches_data : English.TemporalExpressions.before_.complementVeridical = before_nonveridical.complementEntailed

Fragment matches data for before.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.after_three_layer : after_veridical.complementEntailed = true ∧ English.TemporalExpressions.after_.complementVeridical = true ∧ ∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Anscombe.after A B → ∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

Three-layer consistency for after: data, fragment, and theory all agree.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.before_three_layer : before_nonveridical.complementEntailed = false ∧ English.TemporalExpressions.before_.complementVeridical = false ∧ ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Anscombe.before A B ∧ ¬∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace B

Three-layer consistency for before: data, fragment, and theory all agree.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.veridicality_from_quantifiers : English.TemporalExpressions.after_.complementVeridical = true ∧ English.TemporalExpressions.when_conn.complementVeridical = true ∧ English.TemporalExpressions.until_.complementVeridical = true ∧ English.TemporalExpressions.since_conn.complementVeridical = true ∧ English.TemporalExpressions.whenever_conn.complementVeridical = true ∧ English.TemporalExpressions.asSoonAs.complementVeridical = true ∧ English.TemporalExpressions.asLongAs.complementVeridical = true ∧ English.TemporalExpressions.before_.complementVeridical = false

The veridicality pattern is determined by quantifier force: ∃-based connectives are veridical; ∀-based (before) is non-veridical.

def OgiharaSteinertThrelkeld2024.VeridicalityBridge.connPartialProp (complementInstantiated connHolds : Bool) : Semantics.Presupposition.PartialProp Unit

A temporal connective modeled as a presuppositional proposition. Veridical connectives presuppose their complement (like factives); non-veridical connectives carry no complement presupposition.

Equations

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

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.veridical_presupposes_complement : (connPartialProp true true).presup () = (true = true)

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.nonveridical_no_presupposition : (connPartialProp false true).presup () = (false = true)

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.negation_preserves_presup : (connPartialProp true true).neg.presup () = (true = true)

Negation preserves complement presupposition (projection through negation).

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.all_before_readings_nonveridical : English.TemporalExpressions.before_.complementVeridical = false

All three readings are compatible with complementVeridical = false.

theorem OgiharaSteinertThrelkeld2024.VeridicalityBridge.bc_readings_in_data : before_nonveridical.complementEntailed = false ∧ before_counterfactual.complementEntailed = false ∧ before_noncommittal.complementEntailed = false

The O&ST data covers all three B&C readings.