Historical Alternatives

The historical alternatives of a world at a time are the worlds that perfectly match it in matters of particular fact up to that time ([Lew79b], [CS18]).

Main definitions

• HistoricalAlternatives : the relation between a ⟨world, time⟩ index and the worlds that share its history up to that time;
• isActualHistory, isFutureHistory, isPastHistory, isProspectiveHistory, isMaximalHistory : interval predicates indexing the situation-base slices;
• historicalBase, actualHistoryBase, futureHistoryBase : the temporal slices of the historical modal base;
• histEquiv : historical equivalence ≃_t of [Con02];
• metaphysicalBase : the equivalence class of the evaluation world under ≃_t;
• toTWFrame : a relation with HistoricalProperties, viewed as a Core.Logic.Temporal.TWFrame ([Tho84], [vK97]).

Main results

• upperLimitConstraintModal_implies_value : the Upper Limit Constraint ([Abu97]) is derived from actualHistoryBase membership;
• alternatives_antitone, metaphysicalBase_antitone : the metaphysical base shrinks as time advances;
• settled_not_diverse : settled properties block metaphysical readings;
• toTWFrame_sat_N_atom : the object logic's historical necessity N reduces to truth throughout the metaphysicalBase;
• settled_iff_determined : Condoravdi's settled = object-logic historical determinacy (N P ∨ N ¬P) — settled-whether (bilateral), the analogue of oSettled, not IsInevitable.

def HistoricalAlternatives (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Historical-alternatives relation: given a ⟨world, time⟩ index, returns the worlds that agree with that world up to that time. This is the basis for the "historical" or "open future" modal base used in future-oriented modality.

Equations

• HistoricalAlternatives W Time = (Intensional.WorldTimeIndex W Time → Set W)

Partial History Taxonomy

[Kle16] distinguishes five kinds of partial history by the temporal component of the world-time pair relative to a reference time t. We formalize all five as predicates on time pairs. Only actual and future drive the core DOX/CIR mechanism, but the full taxonomy is needed for extensions (prospective is the temporal component of historicalBase below).

These are framework-neutral interval predicates over LE Time / LT Time; the [Kle16] citation is for the terminology, not the mathematical content (which is just ≤, <, >, ≥).

def HistoricalAlternatives.isMaximalHistory {Time : Type u_2} (_evalTime _historyTime : Time) : Prop

Maximal history: unrestricted temporal extent (Ω_t = all histories).

Equations

• HistoricalAlternatives.isMaximalHistory _evalTime _historyTime = True

def HistoricalAlternatives.isActualHistory {Time : Type u_2} [LE Time] (evalTime historyTime : Time) : Prop

Actual history: temporal component ends at or before t (𝒜_t).

Equations

• HistoricalAlternatives.isActualHistory evalTime historyTime = (historyTime ≤ evalTime)

def HistoricalAlternatives.isPastHistory {Time : Type u_2} [LT Time] (evalTime historyTime : Time) : Prop

Past history: temporal component ends strictly before t (𝒫_t). Distinct from actual: past excludes t itself.

Equations

• HistoricalAlternatives.isPastHistory evalTime historyTime = (historyTime < evalTime)

def HistoricalAlternatives.isFutureHistory {Time : Type u_2} [LT Time] (evalTime historyTime : Time) : Prop

Future history: temporal component starts strictly after t (ℱ_t).

Equations

• HistoricalAlternatives.isFutureHistory evalTime historyTime = (historyTime > evalTime)

def HistoricalAlternatives.isProspectiveHistory {Time : Type u_2} [LE Time] (evalTime historyTime : Time) : Prop

Prospective history: temporal component starts at or after t (ℙ_t). This is exactly the temporal component of historicalBase.

Equations

• HistoricalAlternatives.isProspectiveHistory evalTime historyTime = (historyTime ≥ evalTime)

theorem HistoricalAlternatives.actual_future_complementary {Time : Type u_2} [LinearOrder Time] (evalTime historyTime : Time) : isActualHistory evalTime historyTime ∨ isFutureHistory evalTime historyTime

Actual and future histories are complementary: every time is either ≤ t (actual) or > t (future).

theorem HistoricalAlternatives.past_prospective_complementary {Time : Type u_2} [LinearOrder Time] (evalTime historyTime : Time) : isPastHistory evalTime historyTime ∨ isProspectiveHistory evalTime historyTime

Past and prospective histories are complementary: every time is either < t (past) or ≥ t (prospective).

theorem HistoricalAlternatives.past_implies_actual {Time : Type u_2} [Preorder Time] (evalTime historyTime : Time) (h : isPastHistory evalTime historyTime) : isActualHistory evalTime historyTime

Past ⊂ actual: strict past implies actual.

theorem HistoricalAlternatives.future_implies_prospective {Time : Type u_2} [Preorder Time] (evalTime historyTime : Time) (h : isFutureHistory evalTime historyTime) : isProspectiveHistory evalTime historyTime

Future ⊂ prospective: strict future implies prospective.

theorem HistoricalAlternatives.actual_and_prospective_iff_simultaneous {Time : Type u_2} [PartialOrder Time] (evalTime historyTime : Time) : isActualHistory evalTime historyTime ∧ isProspectiveHistory evalTime historyTime ↔ historyTime = evalTime

Actual ∩ prospective = simultaneous: a time that is both actual and prospective is exactly the evaluation time.

theorem HistoricalAlternatives.past_future_disjoint {Time : Type u_2} [Preorder Time] (evalTime historyTime : Time) : ¬(isPastHistory evalTime historyTime ∧ isFutureHistory evalTime historyTime)

Past and future are disjoint: no time is both < t and > t.

Situation Bases

def HistoricalAlternatives.historicalBase {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s : Intensional.WorldTimeIndex W Time) : Set (Intensional.WorldTimeIndex W Time)

Historical modal base: situations whose worlds agree with s up to τ(s), and whose times are at or after τ(s). Past is fixed, the future branches ([Tho84], [Con02]).

Equations

• history.historicalBase s = {s' : Intensional.WorldTimeIndex W Time | s'.world ∈ history s ∧ HistoricalAlternatives.isProspectiveHistory s.time s'.time}

def HistoricalAlternatives.actualHistoryBase {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s : Intensional.WorldTimeIndex W Time) : Set (Intensional.WorldTimeIndex W Time)

Actual history base ([Kle16] DOX): situations whose worlds agree with s and whose times are at or before τ(s) — the temporal mirror of historicalBase.

Equations

• history.actualHistoryBase s = {s' : Intensional.WorldTimeIndex W Time | s'.world ∈ history s ∧ HistoricalAlternatives.isActualHistory s.time s'.time}

def HistoricalAlternatives.futureHistoryBase {W : Type u_1} {Time : Type u_2} [LT Time] (history : HistoricalAlternatives W Time) (s : Intensional.WorldTimeIndex W Time) : Set (Intensional.WorldTimeIndex W Time)

Future history base ([Kle16] CIR): situations whose worlds agree with s and whose times are strictly after τ(s).

Equations

• history.futureHistoryBase s = {s' : Intensional.WorldTimeIndex W Time | s'.world ∈ history s ∧ HistoricalAlternatives.isFutureHistory s.time s'.time}

def HistoricalAlternatives.reflexive {W : Type u_1} {Time : Type u_2} (h : HistoricalAlternatives W Time) : Prop

A historical-alternatives relation is reflexive if every world agrees with itself.

Equations

• h.reflexive = ∀ (s : Intensional.WorldTimeIndex W Time), s.world ∈ h s

def HistoricalAlternatives.symmetric {W : Type u_1} {Time : Type u_2} (h : HistoricalAlternatives W Time) : Prop

A historical-alternatives relation is symmetric: if w' agrees with w up to t, then w agrees with w' up to t. Part of ≃_t being an equivalence relation ([Con02]).

Equations

• h.symmetric = ∀ (w w' : W) (t : Time), w' ∈ h { world := w, time := t } → w ∈ h { world := w', time := t }

def HistoricalAlternatives.transitive {W : Type u_1} {Time : Type u_2} (h : HistoricalAlternatives W Time) : Prop

A historical-alternatives relation is transitive: if w' agrees with w up to t and w'' agrees with w' up to t, then w'' agrees with w up to t.

Equations

• h.transitive = ∀ (w w' w'' : W) (t : Time), w' ∈ h { world := w, time := t } → w'' ∈ h { world := w', time := t } → w'' ∈ h { world := w, time := t }

def HistoricalAlternatives.backwardsClosed {W : Type u_1} {Time : Type u_2} [LE Time] (h : HistoricalAlternatives W Time) : Prop

A historical-alternatives relation is backwards-closed: if w' agrees with w up to t and t' ≤ t, then w' agrees with w up to t' ([Con02]).

Equations

• h.backwardsClosed = ∀ (w w' : W) (t t' : Time), t' ≤ t → w' ∈ h { world := w, time := t } → w' ∈ h { world := w, time := t' }

structure HistoricalAlternatives.HistoricalProperties {W : Type u_1} {Time : Type u_2} [LE Time] (h : HistoricalAlternatives W Time) : Prop

Standard historical modal base properties: ≃_t is an equivalence relation that is monotone in time ([Con02]).

• refl : h.reflexive

  Every world agrees with itself

• symm : h.symmetric

  Historical agreement is symmetric

• trans : h.transitive

  Historical agreement is transitive

• backwards : h.backwardsClosed

  Agreement is preserved for earlier times

@[reducible, inline]

abbrev HistoricalAlternatives.TProp (W : Type u_3) (Time : Type u_4) : Type (max u_4 u_3)

A temporal proposition: true or false at each situation. The situation-semantic analog of Prop' W.

Equations

• HistoricalAlternatives.TProp W Time = (Intensional.WorldTimeIndex W Time → Prop)

def HistoricalAlternatives.liftProp {W : Type u_1} {Time : Type u_2} (p : W → Prop) : TProp W Time

Lift a world proposition to a temporal proposition, true at situation s iff the original holds at s.world.

Equations

• HistoricalAlternatives.liftProp p s = p s.world

def HistoricalAlternatives.holdsAt {W : Type u_1} {Time : Type u_2} (p : TProp W Time) (w : W) (t : Time) : Prop

A proposition holds at time t in world w.

Equations

• HistoricalAlternatives.holdsAt p w t = p { world := w, time := t }

Klecha 2016: ULC derived from history structure

The Upper Limit Constraint — embedded RT under a doxastic attitude must be ≤ matrix EvalT — was stated by [Abu97] ("the now of an epistemic alternative is an upper limit for the denotation of tenses"), with the presuppositional construal due to [Hei94a]. [Kle16] derives the same constraint from the temporal character of the doxastic modal base: DOX returns actual histories 𝒜_t, and membership entails RT ≤ t by .2 projection through the situation-base definition. Symmetrically, CIR returns ℱ_t and membership entails RT > t. The theorems below make the projection kernel-checked.

This is what distinguishes [Kle16]'s account from [Abu97]'s: both rely on the branching-futures motivation, but Klecha derives ULC from history structure while Abusch states it as a constraint on tense-node denotation. The Klecha-namespace dispatch on ModalBaseKind lives in Semantics/Modality/TemporalConstraint.lean. The modal-alternative quantification in Abusch's formulation is captured here at the substrate level by HistoricalAlternatives membership; the value-level projection s'.time ≤ s.time recovers Abusch's bare-≤ form.

theorem HistoricalAlternatives.historicalBase_time_prospective {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (h : s' ∈ history.historicalBase s) : isProspectiveHistory s.time s'.time

A situation in historicalBase has prospective time.

theorem HistoricalAlternatives.actualHistoryBase_time_actual {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (h : s' ∈ history.actualHistoryBase s) : isActualHistory s.time s'.time

A situation in actualHistoryBase has actual time.

def HistoricalAlternatives.upperLimitConstraintModal {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (matrixSituation embeddedSituation : Intensional.WorldTimeIndex W Time) : Prop

Modal-layer Upper Limit Constraint: an embedded situation s' satisfies it relative to a matrix situation s and doxastic accessibility history iff s' lies in s's actual-history base. See the section note for how this recovers [Abu97]'s alternative-quantifying formulation.

Equations

• history.upperLimitConstraintModal matrixSituation embeddedSituation = (embeddedSituation ∈ history.actualHistoryBase matrixSituation)

theorem HistoricalAlternatives.upperLimitConstraintModal_implies_value {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (h : history.upperLimitConstraintModal s s') : s'.time ≤ s.time

The modal-layer Upper Limit Constraint implies the value-level one (embeddedSituation.time ≤ matrixSituation.time), by .2 projection through actualHistoryBase.

theorem HistoricalAlternatives.futureHistoryBase_time_future {W : Type u_1} {Time : Type u_2} [LT Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (h : s' ∈ history.futureHistoryBase s) : isFutureHistory s.time s'.time

A situation in futureHistoryBase has future time.

theorem HistoricalAlternatives.futureHistoryBase_subset_historicalBase {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : HistoricalAlternatives W Time) (s : Intensional.WorldTimeIndex W Time) : history.futureHistoryBase s ⊆ history.historicalBase s

futureHistoryBase ⊆ historicalBase: future situations are prospective. The situation-semantic instantiation of future_implies_prospective.

theorem HistoricalAlternatives.actualBase_inter_historicalBase_simultaneous {W : Type u_1} {Time : Type u_2} [PartialOrder Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (hActual : s' ∈ history.actualHistoryBase s) (hHist : s' ∈ history.historicalBase s) : s'.time = s.time

actualHistoryBase ∩ historicalBase contains only simultaneous situations. The situation-semantic instantiation of actual_and_prospective_iff_simultaneous.

theorem HistoricalAlternatives.actualBase_futureBase_disjoint {W : Type u_1} {Time : Type u_2} [Preorder Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) : ¬(s' ∈ history.actualHistoryBase s ∧ s' ∈ history.futureHistoryBase s)

Actual and future history bases are disjoint on the time component. The situation-semantic instantiation of past_future_disjoint.

theorem HistoricalAlternatives.actualBase_futureBase_complementary {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (hw : s'.world ∈ history s) : s' ∈ history.actualHistoryBase s ∨ s' ∈ history.futureHistoryBase s

Every situation is in actualHistoryBase ∪ futureHistoryBase on the time component. The situation-semantic instantiation of actual_future_complementary.

theorem HistoricalAlternatives.prospective_time_mem_historicalBase {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isProspectiveHistory s.time s'.time) : s' ∈ history.historicalBase s

Converse: prospective time + world agreement → membership in historicalBase.

theorem HistoricalAlternatives.actual_time_mem_actualHistoryBase {W : Type u_1} {Time : Type u_2} [LE Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isActualHistory s.time s'.time) : s' ∈ history.actualHistoryBase s

Converse: actual time + world agreement → membership in actualHistoryBase.

theorem HistoricalAlternatives.future_time_mem_futureHistoryBase {W : Type u_1} {Time : Type u_2} [LT Time] (history : HistoricalAlternatives W Time) (s s' : Intensional.WorldTimeIndex W Time) (hw : s'.world ∈ history s) (ht : isFutureHistory s.time s'.time) : s' ∈ history.futureHistoryBase s

Converse: future time + world agreement → membership in futureHistoryBase.

Historical Equivalence

[Con02]: historical equivalence ≃_t groups worlds that share the same history up to time t. The equivalence classes are the "ways things might have gone" — worlds that agree on the past but may diverge in the future.

def HistoricalAlternatives.histEquiv {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) (t : Time) (w w' : W) : Prop

Historical equivalence: w' agrees with w up to time t. w ≃_t w' iff w' ∈ history(w, t).

Equations

• history.histEquiv t w w' = (w' ∈ history { world := w, time := t })

def HistoricalAlternatives.histEquiv_equivalence {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (hSymm : history.symmetric) (hTrans : history.transitive) (t : Time) : Equivalence (history.histEquiv t)

histEquiv history t is an equivalence relation when history satisfies the standard properties ([Con02]).

Equations

• ⋯ = ⋯

def HistoricalAlternatives.histSetoid {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (hSymm : history.symmetric) (hTrans : history.transitive) (t : Time) : Setoid W

The Setoid induced by historical equivalence at time t.

Equations

• HistoricalAlternatives.histSetoid hRefl hSymm hTrans t = { r := history.histEquiv t, iseqv := ⋯ }

def HistoricalAlternatives.histEquiv_equivalence' {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} [LE Time] (hp : history.HistoricalProperties) (t : Time) : Equivalence (history.histEquiv t)

histEquiv_equivalence from bundled HistoricalProperties.

Equations

• ⋯ = ⋯

def HistoricalAlternatives.histSetoid' {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} [LE Time] (hp : history.HistoricalProperties) (t : Time) : Setoid W

histSetoid from bundled HistoricalProperties.

Equations

• HistoricalAlternatives.histSetoid' hp t = HistoricalAlternatives.histSetoid ⋯ ⋯ ⋯ t

theorem HistoricalAlternatives.histEquiv_refl {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} (hRefl : history.reflexive) (t : Time) (w : W) : history.histEquiv t w w

Historical equivalence is reflexive (from reflexive).

theorem HistoricalAlternatives.histEquiv_symm {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} (hSymm : history.symmetric) (t : Time) {w w' : W} (h : history.histEquiv t w w') : history.histEquiv t w' w

Historical equivalence is symmetric (from symmetric).

theorem HistoricalAlternatives.histEquiv_trans {W : Type u_1} {Time : Type u_2} {history : HistoricalAlternatives W Time} (hTrans : history.transitive) (t : Time) {w w' w'' : W} (h₁ : history.histEquiv t w w') (h₂ : history.histEquiv t w' w'') : history.histEquiv t w w''

Historical equivalence is transitive (from transitive).

theorem HistoricalAlternatives.histEquiv_mono {W : Type u_1} {Time : Type u_2} [LE Time] {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) {t t' : Time} (w w' : W) (hle : t' ≤ t) (h : history.histEquiv t w w') : history.histEquiv t' w w'

Historical equivalence is monotone in time: agreement up to a later time implies agreement up to an earlier time (from backwardsClosed).

theorem HistoricalAlternatives.alternatives_antitone {W : Type u_1} {Time : Type u_2} [LE Time] {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) (w : W) {t t' : Time} (hle : t ≤ t') : {w' : W | history.histEquiv t' w w'} ⊆ {w' : W | history.histEquiv t w w'}

The set of metaphysical alternatives shrinks as time advances ([Con02]): t ↦ { w' | w ≃_t w' } is antitone.

Metaphysical Modal Base

[Con02]: for modals expressing metaphysical modality, the modal base consists of historical alternatives MB(w,t) = {w' | w ≃_t w'} — the maximal modal base compatible with the world's history up to t.

def HistoricalAlternatives.metaphysicalBase {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) : W → Time → Set W

The metaphysical modal base: at world w and time t, the set of all worlds sharing w's history up to t.

Equations

• history.metaphysicalBase w t = {w' : W | history.histEquiv t w w'}

theorem HistoricalAlternatives.metaphysicalBase_antitone {W : Type u_1} {Time : Type u_2} [LE Time] {history : HistoricalAlternatives W Time} (hBC : history.backwardsClosed) (w : W) {t t' : Time} (hle : t ≤ t') : history.metaphysicalBase w t' ⊆ history.metaphysicalBase w t

The metaphysical modal base is antitone in time: later times yield smaller accessible sets.

Settledness and Diversity

[Con02]: an issue is settled at time t₀ when all historically equivalent worlds agree on its resolution; past and present issues are always settled, future issues may not be. The diversity condition is the felicity condition for associating a metaphysical modal base with a possibility modal: the base must contain worlds that disagree on the property.

def HistoricalAlternatives.settled {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) (cg : Set W) (t₀ : Time) (P : W → Prop) : Prop

Settledness: within each common-ground equivalence class, the property P is resolved uniformly — all historically equivalent worlds agree on P.

Equations

• history.settled cg t₀ P = ∀ w ∈ cg, ∀ (w' : W), history.histEquiv t₀ w w' → (P w ↔ P w')

def HistoricalAlternatives.diverse {W : Type u_1} {Time : Type u_2} (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) : Prop

Diversity condition: there is a common-ground world whose modal base contains worlds disagreeing on P. The felicity condition for pairing a metaphysical modal base with a possibility modal ([Con02]).

Equations

• HistoricalAlternatives.diverse MB cg t P = ∃ w ∈ cg, ∃ w' ∈ MB w t, ∃ w'' ∈ MB w t, P w' ∧ ¬P w''

theorem HistoricalAlternatives.settled_not_diverse {W : Type u_1} {Time : Type u_2} (history : HistoricalAlternatives W Time) (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) (hMB : ∀ w ∈ cg, ∀ w' ∈ MB w t, history.histEquiv t w w') (hSettled : history.settled cg t P) : ¬diverse MB cg t P

When MB(w,t) ⊆ {w' | w ≃_t w'} (the metaphysical case) and P is settled, diversity fails: all worlds in the modal base agree on P, so no pair can witness disagreement. The key theorem blocking metaphysical readings for settled properties.

theorem HistoricalAlternatives.diverse_of_witnesses {W : Type u_1} {Time : Type u_2} (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) (w : W) (hwcg : w ∈ cg) (w' w'' : W) (hw' : w' ∈ MB w t) (hw'' : w'' ∈ MB w t) (hP : P w') (hnP : ¬P w'') : diverse MB cg t P

Diversity is witnessed by the common ground: if P holds for some world in cg and fails for another, both accessible from some w via MB, then diversity holds.

Grounding in the T × W object logic

A historical-alternatives relation with HistoricalProperties satisfies exactly the axioms of a Core.Logic.Temporal.TWFrame — per-time equivalence (via histEquiv_equivalence') and backward closure — so it is a T × W frame. The object logic's historical necessity N then reduces to quantification over metaphysicalBase, making the denotational base and the object-language modality the same operator ([Tho84], [vK97]).

def HistoricalAlternatives.toTWFrame {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) : Core.Logic.Temporal.TWFrame Time W

A historical-alternatives relation with HistoricalProperties, viewed as a TWFrame: sim is histEquiv, reusing histEquiv_equivalence' for the equivalence axiom and backwards for backward closure.

Equations

• history.toTWFrame hp = { sim := history.histEquiv, sim_equiv := ⋯, sim_backward := ⋯ }

@[simp]

theorem HistoricalAlternatives.toTWFrame_sim {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (t : Time) (w w' : W) : (history.toTWFrame hp).sim t w w' ↔ w' ∈ history.metaphysicalBase w t

theorem HistoricalAlternatives.toTWFrame_sat_N_atom {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {Atom : Type u_3} (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (V : Atom → Time → W → Prop) (p : Atom) (t : Time) (w : W) : (history.toTWFrame hp).sat V (Core.Logic.Temporal.OForm.atom p).N t w ↔ ∀ w' ∈ history.metaphysicalBase w t, V p t w'

Historical necessity N in the object logic = truth throughout the metaphysical base.

theorem HistoricalAlternatives.toTWFrame_sat_box_atom {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {Atom : Type u_3} (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (V : Atom → Time → W → Prop) (p : Atom) (t : Time) (w : W) : (history.toTWFrame hp).sat V (Core.Logic.Temporal.OForm.atom p).box t w ↔ ∀ (w' : W), V p t w'

The all-worlds modality box = truth in every world (the unrestricted base).

theorem HistoricalAlternatives.mem_metaphysicalBase_self {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (t : Time) (w : W) : w ∈ history.metaphysicalBase w t

The evaluation world is always a metaphysical alternative to itself.

theorem HistoricalAlternatives.toTWFrame_N_or_N_neg_iff {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {Atom : Type u_3} (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (V : Atom → Time → W → Prop) (a : Core.Logic.Temporal.OForm Atom) (t : Time) (w : W) : (history.toTWFrame hp).sat V a.N t w ∨ (history.toTWFrame hp).sat V a.neg.N t w ↔ ∀ w' ∈ history.metaphysicalBase w t, (history.toTWFrame hp).sat V a t w' ↔ (history.toTWFrame hp).sat V a t w

A formula is historically determined at (t, w) — the object logic decides it, N a ∨ N ¬a — iff it is constant across the metaphysical base. The single-world, formula-general core of settledness.

theorem HistoricalAlternatives.settled_iff_determined {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : HistoricalAlternatives W Time) (hp : history.HistoricalProperties) (cg : Set W) (P : W → Prop) (t : Time) : history.settled cg t P ↔ ∀ w ∈ cg, (history.toTWFrame hp).sat (fun (x : Unit) (x_1 : Time) (w' : W) => P w') (Core.Logic.Temporal.OForm.atom ()).N t w ∨ (history.toTWFrame hp).sat (fun (x : Unit) (x_1 : Time) (w' : W) => P w') (Core.Logic.Temporal.OForm.atom ()).neg.N t w

Condoravdi's settled over a common ground is object-logic historical determinacy at every cg-world: N P ∨ N ¬P for the lifted valuation. This is settled-whether (bilateral, history-blind — the analogue of oSettled/IsSettledWhether, not the unilateral IsInevitable). P is the already-forward-instantiated world proposition (Condoravdi's AT([t₀,_), ·, P); the AT-wrapper is discharged by the caller). Cf. [klecha-2016]'s futureHistoryBase — the slice on which determinacy can fail.