@cite{ogihara-steinert-threlkeld-2024} — Data

@cite{ogihara-steinert-threlkeld-2024}

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).

structure OgiharaST2024.VeridicalityDatum : Type

An empirical judgment about whether a temporal connective entails the truth of its complement clause.

• 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

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

Equations

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

@[implicit_reducible]

instance OgiharaST2024.instReprVeridicalityDatum : Repr VeridicalityDatum

Equations

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

def OgiharaST2024.after_veridical : VeridicalityDatum

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

Equations

• OgiharaST2024.after_veridical = { sentence := "He left after she arrived", connective := "after", complementEntailed := true, gloss := "after(leave, arrive) |= arrive" }

def OgiharaST2024.before_nonveridical : VeridicalityDatum

"He left before she arrived" does NOT entail "she arrived". Compatible with: she did arrive (veridical reading), she didn't arrive (counterfactual reading, e.g. "before she could arrive"), or indeterminate (non-committal reading).

Equations

• OgiharaST2024.before_nonveridical = { sentence := "He left before she arrived", connective := "before", complementEntailed := false, gloss := "before(leave, arrive) |/= arrive" }

def OgiharaST2024.before_counterfactual : VeridicalityDatum

"The bomb exploded before anyone defused it" — the complement event (defusing) did NOT occur. This is the counterfactual reading of before (@cite{beaver-condoravdi-2003}, "barely prevented").

Equations

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

def OgiharaST2024.after_veridical_2 : VeridicalityDatum

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

Equations

• OgiharaST2024.after_veridical_2 = { sentence := "She finished her coffee after he left", connective := "after", complementEntailed := true, gloss := "after(finish, leave) |= leave" }

def OgiharaST2024.before_noncommittal : VeridicalityDatum

"The Supreme Court decided the election before the votes were counted" — non-committal: compatible with votes eventually being counted or never counted (@cite{beaver-condoravdi-2003}, ex. 22).

Equations

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

def OgiharaST2024.before_counterfactual_mozart : VeridicalityDatum

"Mozart died before he finished the Requiem" — counterfactual: Mozart never finished the Requiem (@cite{beaver-condoravdi-2003}, ex. 24).

Equations

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

structure OgiharaST2024.LogicalPropertyDatum : Type

A judgment about a logical property of a temporal connective: does it hold, fail, or hold only under conditions?

• property : String

  Property name

• connective : String

  Connective

• holds : Bool

  Does the property hold?

• example_ : String

  Example sentence(s)

• gloss : String

  Brief explanation

def OgiharaST2024.instReprLogicalPropertyDatum.repr : LogicalPropertyDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance OgiharaST2024.instReprLogicalPropertyDatum : Repr LogicalPropertyDatum

Equations

• OgiharaST2024.instReprLogicalPropertyDatum = { reprPrec := OgiharaST2024.instReprLogicalPropertyDatum.repr }

def OgiharaST2024.before_antisymmetric : LogicalPropertyDatum

Before is antisymmetric: "Cleo was in America before David was" and "David was in America before Cleo was" cannot both be true (with non-overlapping intervals). (@cite{beaver-condoravdi-2003}, exx. 3-4)

Equations

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

def OgiharaST2024.after_not_antisymmetric : LogicalPropertyDatum

After is NOT antisymmetric: overlapping intervals allow both directions. (@cite{beaver-condoravdi-2003}, exx. 5-7, diagram 7)

Equations

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

def OgiharaST2024.before_transitive : LogicalPropertyDatum

Before is transitive: if A before B and B before C, then A before C. (@cite{beaver-condoravdi-2003}, exx. 12-14)

Equations

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

def OgiharaST2024.after_not_transitive : LogicalPropertyDatum

After is NOT transitive: overlapping intervals allow after(A,B) ∧ after(B,C) ∧ ¬after(A,C). (@cite{beaver-condoravdi-2003}, exx. 8-11)

Equations

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

def OgiharaST2024.before_licenses_npis : LogicalPropertyDatum

Before licenses NPIs; after does not. (@cite{beaver-condoravdi-2003}, exx. 15-18)

Equations

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

def OgiharaST2024.before_oddity_win : VeridicalityDatum

"David won the race before he entered it" — pragmatically odd because winning temporally presupposes entering: there is no historical alternative where one wins before entering. (@cite{beaver-condoravdi-2003}, ex. 32)

Equations

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

def OgiharaST2024.after_oddity_enter : VeridicalityDatum

"David entered the race after he won it" — same temporal impossibility viewed through after: entering after winning reverses the natural temporal order. (@cite{beaver-condoravdi-2003}, ex. 33)

Equations

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

structure OgiharaST2024.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 : Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BeforeReading

  Which B&C reading is involved?

theorem OgiharaST2024.bc_cannot_place_bounded_complement {W : Type u_1} (alt : Semantics.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 ∈ Semantics.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 OgiharaST2024.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&@cite{ogihara-steinert-threlkeld-2024}, §5.1, ex. 20a)

Equations

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

def OgiharaST2024.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&@cite{ogihara-steinert-threlkeld-2024}, §5.1, ex. 20b)

Equations

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

def OgiharaST2024.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&@cite{ogihara-steinert-threlkeld-2024}, §5.1, ex. 20c)

Equations

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

structure OgiharaST2024.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 OgiharaST2024.instReprNonCommittalDatum.repr : NonCommittalDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance OgiharaST2024.instReprNonCommittalDatum : Repr NonCommittalDatum

Equations

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

def OgiharaST2024.noncommittal_available : NonCommittalDatum

"Mary will leave the party before Bill gets drunk." Non-committal reading is available: maybe Bill gets drunk, maybe not. B&C's Event Continuation Condition is satisfied (Bill getting drunk is a normal continuation). (O&@cite{ogihara-steinert-threlkeld-2024}, §5.2)

Equations

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

def OgiharaST2024.noncommittal_unavailable : NonCommittalDatum

"Mary will leave the party before Quebec becomes an independent country." Non-committal reading is NOT available (sentence is odd): Quebec's independence is not a normal continuation of the party. B&C's Event Continuation Condition should block this, but the mechanism is unclear for before-clauses with pragmatically impossible complements. (O&@cite{ogihara-steinert-threlkeld-2024}, §5.2)

Equations

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

theorem OgiharaST2024.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 OgiharaST2024.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 OgiharaST2024.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

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

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

Equations

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

def OgiharaST2024.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&@cite{ogihara-steinert-threlkeld-2024}, §3)

Equations

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

def OgiharaST2024.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&@cite{ogihara-steinert-threlkeld-2024}, §3)

Equations

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

theorem OgiharaST2024.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 OgiharaST2024.after_data_veridical : after_veridical.complementEntailed = true ∧ after_veridical_2.complementEntailed = true

After is uniformly veridical across examples.

theorem OgiharaST2024.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 OgiharaST2024.veridicality_asymmetry : after_veridical.complementEntailed ≠ before_nonveridical.complementEntailed

The asymmetry: after and before differ on complement entailment.

theorem OgiharaST2024.logical_property_asymmetry : before_antisymmetric.holds ≠ after_not_antisymmetric.holds ∧ before_transitive.holds ≠ after_not_transitive.holds

Before and after are opposites on all logical properties tested.

theorem OgiharaST2024.after_fragment_matches_datum : Fragments.English.TemporalExpressions.after_.complementVeridical = after_veridical.complementEntailed

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

theorem OgiharaST2024.before_fragment_matches_datum : Fragments.English.TemporalExpressions.before_.complementVeridical = before_nonveridical.complementEntailed

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

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

The veridicality asymmetry is reflected in the Fragment entries.

theorem OgiharaST2024.after_veridicality_derived (P Q : Semantics.Events.EvPred ℤ) : Semantics.Tense.TemporalConnectives.AnscombeEvent.after P Q → ∃ (e : Semantics.Events.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 OgiharaST2024.before_nonveridicality_derived : ∃ (P : Semantics.Events.EvPred ℤ) (Q : Semantics.Events.EvPred ℤ), Semantics.Tense.TemporalConnectives.AnscombeEvent.before P Q ∧ ¬∃ (e : Semantics.Events.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 OgiharaST2024.scenario_after_punctual : have leave := { runtime := { start := 1, finish := 1, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; have arrive := { runtime := { start := 0, finish := 0, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.AnscombeEvent.after (fun (x : Semantics.Events.Event ℤ) => x = leave) fun (x : Semantics.Events.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 OgiharaST2024.scenario_before_punctual : have leave := { runtime := { start := 1, finish := 1, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; have arrive := { runtime := { start := 3, finish := 3, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.AnscombeEvent.before (fun (x : Semantics.Events.Event ℤ) => x = leave) fun (x : Semantics.Events.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 OgiharaST2024.scenario_before_counterfactual : have explode := { runtime := { start := 5, finish := 5, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.AnscombeEvent.before (fun (x : Semantics.Events.Event ℤ) => x = explode) fun (x : Semantics.Events.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 OgiharaST2024.scenario_after_projects : have leave := { runtime := { start := 1, finish := 1, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; have arrive := { runtime := { start := 0, finish := 0, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Event ℤ) => x = leave) (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Event ℤ) => x = arrive)

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

theorem OgiharaST2024.scenario_before_projects : have leave := { runtime := { start := 1, finish := 1, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; have arrive := { runtime := { start := 3, finish := 3, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Event ℤ) => x = leave) (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Event ℤ) => x = arrive)

The punctual before-scenario projects correctly through eventDenotation.

The logical properties of before and after noted by B&C follow directly from the quantificational structure. We verify each on concrete interval scenarios over ℤ, matching the B&C diagrams.

theorem OgiharaST2024.before_antisymmetric_scenario : Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_cleo_b✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_david_b✝) ∧ ¬Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_david_b✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_cleo_b✝)

Before is antisymmetric on non-overlapping statives: if A before B, then ¬(B before A). (@cite{beaver-condoravdi-2003}, exx. 3-4)

Scenario: Cleo [1,5], David [8,12]. Cleo before David holds; David before Cleo does not.

The ∀-quantifier in Anscombe.before enforces this: if all of B follows some point in A, then no point in B precedes all of A.

theorem OgiharaST2024.after_not_antisymmetric_scenario : Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_cleo_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_david_a✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_david_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_cleo_a✝)

After is NOT antisymmetric: overlapping intervals allow both after(A,B) and after(B,A). (@cite{beaver-condoravdi-2003}, exx. 5-7, diagram 7)

Scenario: Cleo [1,8], David [5,12]. Both Cleo-after-David and David-after-Cleo hold because ∃ requires only one witness.

theorem OgiharaST2024.before_transitive_scenario : Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_delores_t✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_ginger_t✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_ginger_t✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_fred_t✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_delores_t✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_fred_t✝)

Before is transitive: A before B ∧ B before C → A before C. (@cite{beaver-condoravdi-2003}, exx. 12-14)

Scenario: Delores [1,3], Ginger [6,8], Fred [11,13].

theorem OgiharaST2024.after_not_transitive_scenario : Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_fred_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_ginger_a✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_ginger_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_delores_a✝) ∧ ¬Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_fred_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation OgiharaST2024.i_delores_a✝)

After is NOT transitive: overlapping intervals allow after(A,B) ∧ after(B,C) ∧ ¬after(A,C). (@cite{beaver-condoravdi-2003}, exx. 8-11)

Scenario: Fred [1,3], Ginger [2,5], Delores [4,7]. Fred after Ginger: t=3, t'=2. ✓ Ginger after Delores: t=5, t'=4. ✓ Fred after Delores: need t ∈ [1,3], t' ∈ [4,7], t' < t — impossible since max(Fred)=3 < 4=min(Delores). ✗

theorem OgiharaST2024.before_antisymmetric_general {Time : Type u_1} [LinearOrder Time] (A B : Semantics.Tense.TemporalConnectives.SentDenotation Time) : Semantics.Tense.TemporalConnectives.Anscombe.before A B → ¬Semantics.Tense.TemporalConnectives.Anscombe.before B A

Before is antisymmetric in general: before(A,B) → ¬before(B,A).

From the ∀ in Anscombe's before: if ∃t ∈ A, ∀t' ∈ B, t < t', then for any s ∈ B we get t < s. But before(B,A) gives ∀ t ∈ A, s < t, so s < t and t < s — contradiction.

Note: no non-emptiness assumption needed.

theorem OgiharaST2024.before_transitive_general {Time : Type u_1} [LinearOrder Time] (A B C : Semantics.Tense.TemporalConnectives.SentDenotation Time) : Semantics.Tense.TemporalConnectives.Anscombe.before A B → Semantics.Tense.TemporalConnectives.Anscombe.before B C → Semantics.Tense.TemporalConnectives.Anscombe.before A C

Before is transitive in general: before(A,B) → before(B,C) → before(A,C).

From before(A,B): ∃t ∈ A, ∀t' ∈ B, t < t'. From before(B,C): ∃s ∈ B, ∀s' ∈ C, s < s'. Then t < s (from the first, since s ∈ B), and for any u ∈ C, s < u (from the second). So t < u by transitivity of <. Witness: t ∈ A.

Note: no non-emptiness assumption needed — s ∈ timeTrace B is provided by the second hypothesis.

theorem OgiharaST2024.npi_datum_matches_fragment : Fragments.English.TemporalExpressions.before_.licensesNPI = before_licenses_npis.holds

The NPI datum matches the Fragment entry: before licenses NPIs.

theorem OgiharaST2024.japanese_mae_matches_datum : Fragments.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 OgiharaST2024.japanese_ato_matches_datum : Fragments.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.

@cite{ogihara-steinert-threlkeld-2024} §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** (@cite{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 OgiharaST2024.csip_entails_completion {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Semantics.Events.EventPred W Time) (hCSIP : Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P) (w : W) (t : Core.Time.Interval Time) : Semantics.Aspect.Core.IMPF P w t → Semantics.Aspect.Core.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_csip from SubintervalProperty.lean.

theorem OgiharaST2024.non_csip_lacks_completion {W : Type u_1} (w : W) (t₁ t₂ : ℤ) (hlt : t₁ < t₂) : ¬∀ (P : Semantics.Events.EventPred W ℤ), 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 OgiharaST2024.progressive_before_modal_resolution {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P Q : Semantics.Events.EventPred W Time) (alternatives : Semantics.Events.Event Time → Set W) (w : W) (t : Core.Time.Interval Time) (hIMPF : Semantics.Aspect.Core.IMPF P w t) (hContinuation : ∀ (e : Semantics.Events.Event Time), P w e → t.properSubinterval e.τ → ∀ w' ∈ alternatives e, ∃ (e' : Semantics.Events.Event Time), Q w' e') : ∃ (e : Semantics.Events.Event Time), t.properSubinterval e.τ ∧ P w e ∧ ∀ w' ∈ alternatives e, ∃ (e' : Semantics.Events.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 OgiharaST2024.csip_determines_modal_need {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Semantics.Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : (Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P → Semantics.Aspect.Core.IMPF P w t → Semantics.Aspect.Core.PRFV P w t) ∧ (Semantics.Aspect.Core.IMPF P w t → ¬Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P → (¬∀ (t' : Core.Time.Interval Time), t'.subinterval t → ∃ (e : Semantics.Events.Event Time), e.τ = t' ∧ P w e) → ∃ (e : Semantics.Events.Event Time), t.properSubinterval 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 OgiharaST2024.abuts {T : Type u_2} [LinearOrder T] (I₀ I₁ : Core.Time.Interval T) : Prop

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

Equations

• OgiharaST2024.abuts I₀ I₁ = (I₀.finish = I₁.start)

def OgiharaST2024.holdsAtAbutting {T : Type u_2} {E : Type u_3} [LinearOrder T] (runtime : E → Core.Time.Interval T) (e₁ : E) (I₀ : Core.Time.Interval 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

• OgiharaST2024.holdsAtAbutting runtime e₁ I₀ = ((runtime e₁).start ≤ I₀.start ∧ I₀.start ≤ (runtime e₁).finish)

@[reducible, inline]

abbrev OgiharaST2024.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

• OgiharaST2024.SitDenot W T E = Set (W × Core.Time.Interval T × E)

def OgiharaST2024.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₀ : Core.Time.Interval 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

• OgiharaST2024.beforeCase_veridical A B w₀ I₀ e₀ = ((w₀, I₀, e₀) ∈ A ∧ ∃ (I₂ : Core.Time.Interval T), I₀.finish < I₂.start ∧ ∃ (e₄ : E), (w₀, I₂, e₄) ∈ B)

def OgiharaST2024.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₀ : Core.Time.Interval 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

• OgiharaST2024.beforeCase_false A B w₀ I₀ e₀ = ((w₀, I₀, e₀) ∈ A ∧ ∃ (I₂ : Core.Time.Interval T), I₂.finish ≤ I₀.start ∧ ∃ (e₅ : E), (w₀, I₂, e₅) ∈ B)

def OgiharaST2024.beforeCase_modal {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (A B : SitDenot W T E) (runtime : E → Core.Time.Interval T) (alt : W → Core.Time.Interval T → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : Core.Time.Interval 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 OgiharaST2024.OST.before {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (A B : SitDenot W T E) (runtime : E → Core.Time.Interval T) (alt : W → Core.Time.Interval T → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : Core.Time.Interval 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 OgiharaST2024.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₀ : Core.Time.Interval T) (e₀ : E) : beforeCase_veridical A B w₀ I₀ e₀ → ∃ (I : Core.Time.Interval 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 OgiharaST2024.beforeCase_modal_nonveridical : ∃ (A : SitDenot Bool ℤ Unit) (B : SitDenot Bool ℤ Unit) (runtime : Unit → Core.Time.Interval ℤ) (alt : Bool → Core.Time.Interval ℤ → Unit → Set Bool) (cause : Bool → Unit → Unit → Prop) (counterpart : Bool → Unit → Bool → Unit → Prop) (w₀ : Bool) (I₀ : Core.Time.Interval ℤ) (e₀ : Unit), beforeCase_modal A B runtime alt cause counterpart w₀ I₀ e₀ ∧ ¬∃ (I : Core.Time.Interval ℤ) (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 OgiharaST2024.cases_i_ii_exclusive {T : Type u_2} [LinearOrder T] (I₀ I_B : Core.Time.Interval T) (hAfter : I₀.finish < I_B.start) (hBefore : I_B.finish ≤ I₀.start) : 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 OgiharaST2024.mozart_is_case_iii {W : Type u_4} {E : Type u_5} (A B : SitDenot W ℤ E) (runtime : E → Core.Time.Interval ℤ) (alt : W → Core.Time.Interval ℤ → E → Set W) (cause : W → E → E → Prop) (counterpart : W → E → W → E → Prop) (w₀ : W) (I₀ : Core.Time.Interval ℤ) (e₀ : E) (hNoFinish : ¬∃ (I : Core.Time.Interval ℤ) (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

@cite{beaver-condoravdi-2003} @cite{heim-1983} @cite{ogihara-steinert-threlkeld-2024}

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 PrProp 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 OgiharaST2024.VeridicalityBridge.after_veridicality_grounded : Fragments.English.TemporalExpressions.after_.complementVeridical = true ∧ ∀ (A B : Semantics.Tense.TemporalConnectives.SentDenotation ℤ), Semantics.Tense.TemporalConnectives.Anscombe.after A B → ∃ (t : ℤ), t ∈ Semantics.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 OgiharaST2024.VeridicalityBridge.when_veridicality_grounded : Fragments.English.TemporalExpressions.when_conn.complementVeridical = true ∧ ∀ (A B : Semantics.Tense.TemporalConnectives.SentDenotation ℤ), Semantics.Tense.TemporalConnectives.Karttunen.when_ A B → ∃ (t : ℤ), t ∈ Semantics.Tense.TemporalConnectives.timeTrace B

when is veridical: Fragment field matches theory proof.

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

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

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

since is veridical: Fragment field matches theory proof.

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

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

Non-veridical connectives

theorem OgiharaST2024.VeridicalityBridge.before_nonveridicality_grounded : Fragments.English.TemporalExpressions.before_.complementVeridical = false ∧ ∃ (A : Semantics.Tense.TemporalConnectives.SentDenotation ℤ) (B : Semantics.Tense.TemporalConnectives.SentDenotation ℤ), Semantics.Tense.TemporalConnectives.Anscombe.before A B ∧ ¬∃ (t : ℤ), t ∈ Semantics.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 OgiharaST2024.VeridicalityBridge.after_fragment_matches_data : Fragments.English.TemporalExpressions.after_.complementVeridical = after_veridical.complementEntailed

Fragment matches data for after.

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

Fragment matches data for before.

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

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

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

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

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

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

def OgiharaST2024.VeridicalityBridge.connPrProp (complementInstantiated connHolds : Bool) : Core.Presupposition.PrProp Unit

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

Equations

• OgiharaST2024.VeridicalityBridge.connPrProp complementInstantiated connHolds = { presup := fun (x : Unit) => complementInstantiated = true, assertion := fun (x : Unit) => connHolds = true }

theorem OgiharaST2024.VeridicalityBridge.veridical_presupposes_complement : (connPrProp true true).presup () = (true = true)

theorem OgiharaST2024.VeridicalityBridge.nonveridical_no_presupposition : (connPrProp false true).presup () = (false = true)

theorem OgiharaST2024.VeridicalityBridge.negation_preserves_presup : (connPrProp true true).neg.presup () = (true = true)

Negation preserves complement presupposition (projection through negation).

theorem OgiharaST2024.VeridicalityBridge.all_before_readings_nonveridical : Fragments.English.TemporalExpressions.before_.complementVeridical = false

All three readings are compatible with complementVeridical = false.

theorem OgiharaST2024.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.