@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 : BranchingTime.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) : BranchingTime.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 : BranchingTime.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.

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

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 ⋯

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

Equations

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

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

Equations

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

def Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instBEqBeforeReading.beq : BeforeReading → BeforeReading → Bool

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instBEqBeforeReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instBEqBeforeReading : BEq BeforeReading

Equations

• Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instBEqBeforeReading = { beq := Semantics.Tense.TemporalConnectives.BeaverCondoravdi.instBEqBeforeReading.beq }

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.