@cite{beaver-condoravdi-2003}: Uniform Analysis with earliest

@cite{beaver-condoravdi-2003} @cite{thomason-1984}

A uniform semantics for before and after: both connectives use the same earliest operator, with the veridicality asymmetry derived from branching time and historical alternatives rather than quantificational asymmetry.

Core Architecture

B&C define temporal connective truth conditions over world–time pairs (situations) with access to historical alternatives:

• A after B true at w iff ∃t : ⟨w,t⟩ ∈ A, t > earliest_{alt(w,t)}(B)
• A before B true at w iff ∃t : ⟨w,t⟩ ∈ A, t < earliest_{alt(w,t)}(B)

Where alt(w,t) is the set of worlds historically accessible from w at t (worlds sharing w's history up to t).

Veridicality from Branching

The veridicality asymmetry falls out from the initial branch point condition:

• After: A happens after the earliest B. Since B is in the past of A and alt(w,t) only branches in the future of t, B must be on the actual branch. So after is always veridical.

• Before: A happens before the earliest B. B could be on a different branch (a historical alternative), so B might not be instantiated in w. Three readings arise from context: veridical (all context worlds have B), counterfactual (no context world has B), non-committal (some do, some don't).

Level

Level 4 (intensional): operates on sets of world–time pairs. The earliest operator is MAX on the < scale (same as Rett's MAX₍<₎), applied across historical alternatives.

@[reducible, inline]

abbrev Semantics.Tense.TemporalConnectives.BeaverCondoravdi.HistAlt (W : Type u_3) (T : Type u_4) : Type (max u_3 u_4)

Historical alternatives: for each world w and time t, the set of worlds sharing w's history up to t but potentially diverging afterwards.

alt(w,t) satisfies the initial branch point condition: all worlds in alt(w,t) agree with w on all events at times ≤ t.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.HistAlt W T = (W → T → Set W)

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.initialBranchPoint {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) (agree : T → W → W → Prop) : Prop

Initial branch point condition: worlds in alt(w,t) agree with w on all events at times before t.

agree t' w w' means "w and w' are indistinguishable at time t'".

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.initialBranchPoint alt agree = ∀ (w : W) (t : T), ∀ w' ∈ alt w t, ∀ t' < t, agree t' w w'

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altReflexive {W : Type u_1} {T : Type u_2} (alt : HistAlt W T) : Prop

The actual world is always a historical alternative of itself.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altReflexive alt = ∀ (w : W) (t : T), w ∈ alt w t

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altMonotone {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) : Prop

Monotonicity of alternatives: later times have fewer alternatives, since more shared history constrains the set of compatible worlds. alt(w,t') ⊆ alt(w,t) when t ≤ t'.

Intuitively: if w' shares w's history up to t', it also shares w's history up to any earlier t ≤ t'.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altMonotone alt = ∀ (w : W) (t t' : T), t ≤ t' → alt w t' ⊆ alt w t

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.histAltOfWorldHistory {W : Type u_1} {T : Type u_2} (h : Core.Modality.HistoricalAlternatives.WorldHistory W T) : HistAlt W T

Convert a WorldHistory (situation-indexed) to curried HistAlt form.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.histAltOfWorldHistory h w t = h { world := w, time := t }

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.worldHistoryOfHistAlt {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : Core.Modality.HistoricalAlternatives.WorldHistory W T

Convert curried HistAlt to WorldHistory (situation-indexed) form.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.worldHistoryOfHistAlt a s = a s.world s.time

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.histAlt_worldHistory_roundtrip {W : Type u_1} {T : Type u_2} (h : Core.Modality.HistoricalAlternatives.WorldHistory W T) : worldHistoryOfHistAlt (histAltOfWorldHistory h) = h

Round-trip: WorldHistory → HistAlt → WorldHistory is identity.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.worldHistory_histAlt_roundtrip {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : histAltOfWorldHistory (worldHistoryOfHistAlt a) = a

Round-trip: HistAlt → WorldHistory → HistAlt is identity.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altReflexive_iff_reflexive {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : altReflexive a ↔ (worldHistoryOfHistAlt a).reflexive

altReflexive is equivalent to WorldHistory.reflexive.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altMonotone_iff_backwardsClosed {W : Type u_1} {T : Type u_2} [LinearOrder T] (a : HistAlt W T) : altMonotone a ↔ (worldHistoryOfHistAlt a).backwardsClosed

altMonotone is equivalent to WorldHistory.backwardsClosed.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altSymmetric_iff_symmetric {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : (∀ (w : W) (t : T), ∀ w' ∈ a w t, w ∈ a w' t) ↔ (worldHistoryOfHistAlt a).symmetric

HistAlt symmetry is equivalent to WorldHistory.symmetric: if w' ∈ alt(w,t) then w ∈ alt(w',t).

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altTransitive_iff_transitive {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : (∀ (w : W) (t : T), ∀ w' ∈ a w t, ∀ w'' ∈ a w' t, w'' ∈ a w t) ↔ (worldHistoryOfHistAlt a).transitive

HistAlt transitivity is equivalent to WorldHistory.transitive: if w' ∈ alt(w,t) and w'' ∈ alt(w',t) then w'' ∈ alt(w,t).

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.histAlt_eq_histEquiv {W : Type u_1} {T : Type u_2} [LinearOrder T] (h : Core.Modality.HistoricalAlternatives.WorldHistory W T) (w : W) (t : T) : histAltOfWorldHistory h w t = {w' : W | Core.Modality.HistoricalAlternatives.histEquiv h t w w'}

B&C's alt(w,t) is exactly the histEquiv equivalence class: w' ∈ alt(w,t) iff histEquiv history t w w'.

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instTimes {W : Type u_1} {T : Type u_2} (worlds : Set W) (B : Set (W × T)) : Set T

The set of times at which B is instantiated in some world of a world set. instTimes worlds B = { t | ∃ w ∈ worlds, ⟨w,t⟩ ∈ B }.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instTimes worlds B = {t : T | ∃ w ∈ worlds, (w, t) ∈ B}

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.earliestAlt {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) (B : Set (W × T)) (w : W) (t : T) : Set T

earliest across alternatives: the earliest time at which B is instantiated in any world of alt(w,t).

Uses maxOnScale (· < ·) which selects elements dominated by all others on the < ordering — i.e., the minimum / GLB. This is the same operator @cite{rett-2020} uses for her MAX₍<₎.

Equations

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

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.after {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistAlt W T) (w : W) : Prop

B&C's after: ∃t : ⟨w,t⟩ ∈ A, t > earliest_{alt(w,t)}(B).

"There is a time at which A is true in w, and that time is later than the earliest time at which B is true in any historical alternative."

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.after A B alt w = ∃ (t : T), (w, t) ∈ A ∧ ∃ te ∈ Semantics.Tense.TemporalConnectives.BeaverCondoravdi.earliestAlt alt B w t, t > te

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.before {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistAlt W T) (w : W) : Prop

B&C's before: ∃t : ⟨w,t⟩ ∈ A, t < earliest_{alt(w,t)}(B).

"There is a time at which A is true in w, and that time is earlier than the earliest time at which B is true in any historical alternative."

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.before A B alt w = ∃ (t : T), (w, t) ∈ A ∧ ∃ te ∈ Semantics.Tense.TemporalConnectives.BeaverCondoravdi.earliestAlt alt B w t, t < te

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.Inst {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (w : W) : Prop

B is instantiated in world w: ∃t, ⟨w,t⟩ ∈ B.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.Inst B w = ∃ (t : T), (w, t) ∈ B

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.InstAlt {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (alt : HistAlt W T) (w : W) (t : T) : Prop

B is instantiated in some alternative of w at t.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.InstAlt B alt w t = ∃ w' ∈ alt w t, Semantics.Tense.TemporalConnectives.BeaverCondoravdi.Inst B w'

inductive Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BeforeReading : Type

The three contextual readings of before (B&C §5).

Since before quantifies over historical alternatives, the reading depends on whether B is instantiated in the actual world:

• Veridical: B happens in the actual world and in alternatives
• Counterfactual: B doesn't happen in the actual world but does in some alternative (the "barely prevented" reading)
• NonCommittal: context is compatible with both

• veridical : BeforeReading
• counterfactual : BeforeReading
• nonCommittal : BeforeReading

@[implicit_reducible]

instance Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instDecidableEqBeforeReading : DecidableEq BeforeReading

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instDecidableEqBeforeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instReprBeforeReading.repr : BeforeReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instReprBeforeReading : Repr BeforeReading

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instReprBeforeReading = { reprPrec := Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instReprBeforeReading.repr }

noncomputable def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.classifyBeforeReading {W : Type u_1} {T : Type u_2} [(p : Prop) → Decidable p] (B : Set (W × T)) (_w : W) (contextWorlds : Set W) : BeforeReading

Classify a before sentence into its reading based on whether B is instantiated in the actual world w.

Uses classical decidability since the underlying propositions involve arbitrary set membership.

Equations

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

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.after_veridical {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistAlt W T) (agree : T → W → W → Prop) (hIBP : initialBranchPoint alt agree) (eventLocal : ∀ (w w' : W) (t : T), agree t w w' → (w', t) ∈ B → (w, t) ∈ B) (w : W) : after A B alt w → Inst B w

After is veridical under the initial branch point condition: if after(A,B) holds at w, then B is instantiated in w.

The key reasoning (B&C §4): A is at ⟨w,t_A⟩ and B is at ⟨w',t_B⟩ for some w' ∈ alt(w,t_A). Since t_B < t_A (earliest before A), and alt(w,t_A) branches only after t_A, w and w' agree at t_B. So if ⟨w',t_B⟩ ∈ B, the "same event" exists at ⟨w,t_B⟩.

We formalize this with eventLocal: if w' agrees with w at t_B and ⟨w',t_B⟩ ∈ B, then ⟨w,t_B⟩ ∈ B.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.BC.uniform_structure {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistAlt W T) (w : W) : (before A B alt w ↔ ∃ (t : T), (w, t) ∈ A ∧ ∃ te ∈ earliestAlt alt B w t, t < te) ∧ (after A B alt w ↔ ∃ (t : T), (w, t) ∈ A ∧ ∃ te ∈ earliestAlt alt B w t, t > te)

B&C's key claim: before and after use the same earliestAlt operator. The only difference is the comparison direction (< vs >). This is the "uniform analysis" — the veridicality asymmetry is not lexical but structural, following from branching time.

@cite{ogihara-steinert-threlkeld-2024} §4 propose revising B&C's equivalence relation to be sensitive to both an interval I and an eventuality e. The key idea: alternative worlds must contain a counterpart of e that co-occurs with e throughout the interval [START_w(e₁), START(I)), and worlds must be identical at all earlier intervals.

This allows w₂ to become distinct from w₁ before I as long as they contain
events that start simultaneously, share the same set of participants, and
run up until I (not necessarily including I). 

@[reducible, inline]

abbrev Semantics.Tense.TemporalConnectives.BeaverCondoravdi.Counterpart (W : Type u_3) (T : Type u_4) : Type (max u_3 u_4)

Counterpart relation on eventualities across worlds (@cite{ogihara-steinert-threlkeld-2024}, fn. 18): counterpart eventualities share essential properties such as starting time and thematic participants.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.Counterpart W T = (W → T → W → T → Prop)

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.equivIE {W : Type u_1} {T : Type u_2} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (agree : T → W → W → Prop) (w₁ w₂ : W) (startI e₁_start : T) : Prop

Event-relative equivalence ≃_{I,e₁} (@cite{ogihara-steinert-threlkeld-2024}, def 17).

For worlds w₁, w₂ ∈ W, interval I, and eventuality e₁ in w₁, w₁ ≃_{I,e₁} w₂ iff:

(i) there is an eventuality e₂ in w₂ understood as e₁'s counterpart; (ii) e₁ and e₂ co-occur throughout [START_{w₁}(e₁), START(I)); (iii) at all intervals I₁ < START_{w₁}(e₁), w₁ and w₂ are identical.

The coOccur parameter models condition (ii): both eventualities occur throughout the interval [start_e, start_I). The agree parameter models condition (iii): world identity at earlier intervals.

Equations

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

The revised alt(w, I, e) uses the eventuality-relative equivalence (@cite{ogihara-steinert-threlkeld-2024}, def 18a).

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.altIE {W : Type u_1} {T : Type u_2} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (agree : T → W → W → Prop) (w : W) (startI e_start : T) : Set W

Event-relative alternatives alt(w, I, e) (@cite{ogihara-steinert-threlkeld-2024}, def 18a): alt(w, I, e) ⊆ {w' : w ≃_{I,e} w'}.

Equations

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

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.eventContinuation {W : Type u_1} (alt : Set W) (continues : W → Prop) : Set W

Event continuation condition (@cite{ogihara-steinert-threlkeld-2024}, def 18b): alt(w, I, e) contains only those worlds w' in which the counterpart eventuality of e develops beyond I, as long as this is reasonable. Modeled as a predicate on the alternative set.

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.eventContinuation alt continues = {w' : W | w' ∈ alt ∧ continues w'}

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.equivIE_downward_closed {W : Type u_1} {T : Type u_2} [LinearOrder T] (counterpart : Counterpart W T) (coOccur : W → T → W → T → T → T → Prop) (coOccur_mono : ∀ (w₁ : W) (e₁ : T) (w₂ : W) (e₂ s₁ s₂ s₂' : T), s₂' ≤ s₂ → coOccur w₁ e₁ w₂ e₂ s₁ s₂ → coOccur w₁ e₁ w₂ e₂ s₁ s₂') (agree : T → W → W → Prop) (w₁ w₂ : W) (startI startI' e_start : T) (hle : startI' ≤ startI) (h : equivIE counterpart coOccur agree w₁ w₂ startI e_start) : equivIE counterpart coOccur agree w₁ w₂ startI' e_start

Downward closure (@cite{ogihara-steinert-threlkeld-2024}, def 18c): If w ≃{I,e} w' and I' < I, then w ≃{I',e} w'. Earlier equivalence classes are supersets.

O&ST's eventuality-relative equivalence ≃_{I,e} is a strict generalization of B&C's initial branch point condition. Under trivial counterpart and co-occurrence relations (always true), equivIE reduces to condition (iii) alone: identity at all times before the eventuality's start — which is exactly B&C's initialBranchPoint restricted to a single world pair.

This shows that the O&ST framework subsumes B&C: any `HistAlt` satisfying
`initialBranchPoint` can be recovered as an `altIE` with trivial parameters. 

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

Under trivial counterpart (always holds) and trivial co-occurrence (always holds), equivIE reduces to B&C's condition (iii): agreement at all earlier times. This is the per-world-pair content of initialBranchPoint.

theorem Semantics.Tense.TemporalConnectives.BeaverCondoravdi.histAlt_subset_altIE_trivial {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) (agree : T → W → W → Prop) (hIBP : initialBranchPoint alt agree) (w : W) (t : T) : alt w t ⊆ altIE (fun (x : W) (x_1 : T) (x_2 : W) (x_3 : T) => True) (fun (x : W) (x_1 : T) (x_2 : W) (x_3 x_4 x_5 : T) => True) agree w t t

B&C's alt(w,t) under initialBranchPoint is a subset of altIE with trivial counterpart/co-occurrence, when the eventuality starts at t. That is: any world sharing w's history up to t (B&C-style) also satisfies the trivial ≃_{I,e} (O&ST-style).