@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 Phenomena.TenseAspect.Studies.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

instance Phenomena.TenseAspect.Studies.OgiharaST2024.instReprVeridicalityDatum : Repr VeridicalityDatum

Equations

• Phenomena.TenseAspect.Studies.OgiharaST2024.instReprVeridicalityDatum = { reprPrec := Phenomena.TenseAspect.Studies.OgiharaST2024.instReprVeridicalityDatum.repr }

def Phenomena.TenseAspect.Studies.OgiharaST2024.instReprVeridicalityDatum.repr : VeridicalityDatum → ℕ → Std.Format

Equations

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

def Phenomena.TenseAspect.Studies.OgiharaST2024.after_veridical : VeridicalityDatum

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

Equations

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

def Phenomena.TenseAspect.Studies.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

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

def Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.after_veridical_2 : VeridicalityDatum

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

Equations

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

def Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.instReprLogicalPropertyDatum.repr : LogicalPropertyDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.OgiharaST2024.instReprLogicalPropertyDatum : Repr LogicalPropertyDatum

Equations

• Phenomena.TenseAspect.Studies.OgiharaST2024.instReprLogicalPropertyDatum = { reprPrec := Phenomena.TenseAspect.Studies.OgiharaST2024.instReprLogicalPropertyDatum.repr }

def Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.BCCounterexampleDatum : Type

A datum recording an empirical problem for B&C's branching-time analysis. These are cases where before is used with complement events that are in the past, which B&C's forward-branching alt(w,t) cannot handle.

• sentence : String

  The example sentence

• reading : String

  Which reading of before is involved?

• problem : String

  Why B&C's analysis fails

def Phenomena.TenseAspect.Studies.OgiharaST2024.instReprBCCounterexampleDatum.repr : BCCounterexampleDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.OgiharaST2024.instReprBCCounterexampleDatum : Repr BCCounterexampleDatum

Equations

• Phenomena.TenseAspect.Studies.OgiharaST2024.instReprBCCounterexampleDatum = { reprPrec := Phenomena.TenseAspect.Studies.OgiharaST2024.instReprBCCounterexampleDatum.repr }

def Phenomena.TenseAspect.Studies.OgiharaST2024.ost_counterexample_ohtani : BCCounterexampleDatum

"Shohei Ohtani was named the 2023 AL MVP before the 2023 MLB season ended." The complement event (season ending) is in the PAST relative to the naming event but also temporally precedes it. B&C's alt(w,t) at the naming time cannot branch to alternatives where the season doesn't end, because the season ending is already in the past. (O&@cite{ogihara-steinert-threlkeld-2024}, §5.1)

Equations

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

def Phenomena.TenseAspect.Studies.OgiharaST2024.ost_counterexample_snow : BCCounterexampleDatum

"It snowed a lot in 2020 before the pandemic hit." Both events are in the past. B&C's analysis requires alt(w,t) at the snow time to include alternatives where the pandemic doesn't hit, but the pandemic is also in the past. (O&@cite{ogihara-steinert-threlkeld-2024}, §5.1)

Equations

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

def Phenomena.TenseAspect.Studies.OgiharaST2024.ost_counterexample_nostradamus : BCCounterexampleDatum

"Nostradamus predicted many things before they happened." The complement events (predictions coming true) are in the past relative to utterance time. B&C would need alternatives where the predicted events never happen, but these events are already settled. (O&@cite{ogihara-steinert-threlkeld-2024}, §5.1)

Equations

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

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

Equations

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

instance Phenomena.TenseAspect.Studies.OgiharaST2024.instReprNonCommittalDatum : Repr NonCommittalDatum

Equations

• Phenomena.TenseAspect.Studies.OgiharaST2024.instReprNonCommittalDatum = { reprPrec := Phenomena.TenseAspect.Studies.OgiharaST2024.instReprNonCommittalDatum.repr }

def Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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?

def Phenomena.TenseAspect.Studies.OgiharaST2024.instReprCrossLinguisticDatum.repr : CrossLinguisticDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.Studies.OgiharaST2024.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

• Phenomena.TenseAspect.Studies.OgiharaST2024.instReprCrossLinguisticDatum = { reprPrec := Phenomena.TenseAspect.Studies.OgiharaST2024.instReprCrossLinguisticDatum.repr }

def Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.after_data_veridical : after_veridical.complementEntailed = true ∧ after_veridical_2.complementEntailed = true

After is uniformly veridical across examples.

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

The asymmetry: after and before differ on complement entailment.

theorem Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.after_veridicality_derived (P Q : Semantics.Events.EvPred ℤ) : Semantics.Tense.TemporalConnectives.OST.after P Q → ∃ (e : Semantics.Events.Ev ℤ), 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 Phenomena.TenseAspect.Studies.OgiharaST2024.before_nonveridicality_derived : ∃ (P : Semantics.Events.EvPred ℤ) (Q : Semantics.Events.EvPred ℤ), Semantics.Tense.TemporalConnectives.OST.before P Q ∧ ¬∃ (e : Semantics.Events.Ev ℤ), 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 Phenomena.TenseAspect.Studies.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.OST.after (fun (x : Semantics.Events.Ev ℤ) => x = leave) fun (x : Semantics.Events.Ev ℤ) => 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 Phenomena.TenseAspect.Studies.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.OST.before (fun (x : Semantics.Events.Ev ℤ) => x = leave) fun (x : Semantics.Events.Ev ℤ) => 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 Phenomena.TenseAspect.Studies.OgiharaST2024.scenario_before_counterfactual : have explode := { runtime := { start := 5, finish := 5, valid := ⋯ }, sort := Semantics.Events.EventSort.action }; Semantics.Tense.TemporalConnectives.OST.before (fun (x : Semantics.Events.Ev ℤ) => x = explode) fun (x : Semantics.Events.Ev ℤ) => False

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

theorem Phenomena.TenseAspect.Studies.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.Ev ℤ) => x = leave) (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Ev ℤ) => x = arrive)

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

theorem Phenomena.TenseAspect.Studies.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.Ev ℤ) => x = leave) (Semantics.Tense.TemporalConnectives.eventDenotation fun (x : Semantics.Events.Ev ℤ) => 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 Phenomena.TenseAspect.Studies.OgiharaST2024.before_antisymmetric_scenario : Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_cleo_b✝) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_david_b✝) ∧ ¬Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_david_b✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.after_not_antisymmetric_scenario : Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_cleo_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_david_a✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_david_a✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.before_transitive_scenario : Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_delores_t✝) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_ginger_t✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_ginger_t✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_fred_t✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.before (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_delores_t✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.OgiharaST2024.after_not_transitive_scenario : Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_fred_a✝) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_ginger_a✝) ∧ Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_ginger_a✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_delores_a✝) ∧ ¬Semantics.Tense.TemporalConnectives.Anscombe.after (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.OgiharaST2024.i_fred_a✝¹) (Semantics.Tense.TemporalConnectives.stativeDenotation Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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 Phenomena.TenseAspect.Studies.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.