[BC03]: Uniform Analysis with earliest

[BC03] [Tho84]

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.

def BeaverCondoravdi2003.hasEarliest {Time : Type u_1} [LinearOrder Time] (C : Set Time) (p : Time → Prop) : Prop

The EARLIEST definedness presupposition of before^{B&C}: EARLIEST_C is defined for body p iff the set of C-times where p holds has a least element (mathlib's IsLeast).

Equations

• BeaverCondoravdi2003.hasEarliest C p = ∃ (t : Time), IsLeast {t' : Time | t' ∈ C ∧ p t'} t

@[reducible, inline]

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

• BeaverCondoravdi2003.HistAlt W T = (W → T → Set W)

def BeaverCondoravdi2003.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

• BeaverCondoravdi2003.initialBranchPoint alt agree = ∀ (w : W) (t : T), ∀ w' ∈ alt w t, ∀ t' < t, agree t' w w'

def BeaverCondoravdi2003.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

• BeaverCondoravdi2003.altReflexive alt = ∀ (w : W) (t : T), w ∈ alt w t

def BeaverCondoravdi2003.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

• BeaverCondoravdi2003.altMonotone alt = ∀ (w : W) (t t' : T), t ≤ t' → alt w t' ⊆ alt w t

def BeaverCondoravdi2003.histAltOfWorldHistory {W : Type u_1} {T : Type u_2} (h : HistoricalAlternatives W T) : HistAlt W T

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

Equations

• BeaverCondoravdi2003.histAltOfWorldHistory h w t = h { world := w, time := t }

def BeaverCondoravdi2003.worldHistoryOfHistAlt {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : HistoricalAlternatives W T

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

Equations

• BeaverCondoravdi2003.worldHistoryOfHistAlt a s = a s.world s.time

theorem BeaverCondoravdi2003.histAlt_worldHistory_roundtrip {W : Type u_1} {T : Type u_2} (h : HistoricalAlternatives W T) : worldHistoryOfHistAlt (histAltOfWorldHistory h) = h

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

theorem BeaverCondoravdi2003.worldHistory_histAlt_roundtrip {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : histAltOfWorldHistory (worldHistoryOfHistAlt a) = a

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

theorem BeaverCondoravdi2003.altReflexive_iff_reflexive {W : Type u_1} {T : Type u_2} (a : HistAlt W T) : altReflexive a ↔ (worldHistoryOfHistAlt a).reflexive

altReflexive is equivalent to HistoricalAlternatives.reflexive.

theorem BeaverCondoravdi2003.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 HistoricalAlternatives.backwardsClosed.

theorem BeaverCondoravdi2003.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 HistoricalAlternatives.symmetric: if w' ∈ alt(w,t) then w ∈ alt(w',t).

theorem BeaverCondoravdi2003.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 HistoricalAlternatives.transitive: if w' ∈ alt(w,t) and w'' ∈ alt(w',t) then w'' ∈ alt(w,t).

theorem BeaverCondoravdi2003.histAlt_eq_histEquiv {W : Type u_1} {T : Type u_2} [LinearOrder T] (h : HistoricalAlternatives W T) (w : W) (t : T) : histAltOfWorldHistory h w t = {w' : W | h.histEquiv 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 BeaverCondoravdi2003.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

• BeaverCondoravdi2003.instTimes worlds B = {t : T | ∃ w ∈ worlds, (w, t) ∈ B}

def BeaverCondoravdi2003.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 .lt which selects elements dominated by all others on the < ordering — i.e., the minimum / GLB. This is the same operator [Ret20] uses for her MAX₍<₎.

Equations

• BeaverCondoravdi2003.earliestAlt alt B w t = Core.Order.maxOnScale Core.Order.Comparison.lt (BeaverCondoravdi2003.instTimes (alt w t) B)

theorem BeaverCondoravdi2003.mem_earliestAlt_iff_isLeast {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) (B : Set (W × T)) (w : W) (t te : T) : te ∈ earliestAlt alt B w t ↔ IsLeast (instTimes (alt w t) B) te

Membership in earliestAlt is exactly mathlib's IsLeast on the instantiation-times set: B&C's earliest operator is the least element of instTimes, computed via maxOnScale .lt.

theorem BeaverCondoravdi2003.earliestAlt_nonempty_iff_hasEarliest {W : Type u_1} {T : Type u_2} [LinearOrder T] (alt : HistAlt W T) (B : Set (W × T)) (w : W) (t : T) : (earliestAlt alt B w t).Nonempty ↔ hasEarliest Set.univ fun (x : T) => x ∈ instTimes (alt w t) B

B&C's earliest is defined (nonempty) exactly when [Sha14]'s EARLIEST presupposition (hasEarliest, with trivial restrictor) holds of the instantiation times. This is the definedness condition that fails for quantificational pasts on a dense time axis.

def BeaverCondoravdi2003.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

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

def BeaverCondoravdi2003.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

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

def BeaverCondoravdi2003.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

• BeaverCondoravdi2003.Inst B w = ∃ (t : T), (w, t) ∈ B

def BeaverCondoravdi2003.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

• BeaverCondoravdi2003.InstAlt B alt w t = ∃ w' ∈ alt w t, BeaverCondoravdi2003.Inst B w'

inductive BeaverCondoravdi2003.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

@[instance_reducible]

instance BeaverCondoravdi2003.instDecidableEqBeforeReading : DecidableEq BeforeReading

Equations

• BeaverCondoravdi2003.instDecidableEqBeforeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaverCondoravdi2003.instReprBeforeReading.repr : BeforeReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaverCondoravdi2003.instReprBeforeReading : Repr BeforeReading

Equations

• BeaverCondoravdi2003.instReprBeforeReading = { reprPrec := BeaverCondoravdi2003.instReprBeforeReading.repr }

noncomputable def BeaverCondoravdi2003.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 BeaverCondoravdi2003.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 BeaverCondoravdi2003.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.

[OST24] §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 BeaverCondoravdi2003.Counterpart (W : Type u_3) (T : Type u_4) : Type (max u_3 u_4)

Counterpart relation on eventualities across worlds ([OST24], fn. 18): counterpart eventualities share essential properties such as starting time and thematic participants.

Equations

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

def BeaverCondoravdi2003.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₁} ([OST24], 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 ([OST24], def 18a).

def BeaverCondoravdi2003.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) ([OST24], def 18a): alt(w, I, e) ⊆ {w' : w ≃_{I,e} w'}.

Equations

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

def BeaverCondoravdi2003.eventContinuation {W : Type u_1} (alt : Set W) (continues : W → Prop) : Set W

Event continuation condition ([OST24], 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

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

theorem BeaverCondoravdi2003.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 ([OST24], 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 BeaverCondoravdi2003.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 BeaverCondoravdi2003.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).