Historical Alternatives

@cite{condoravdi-2002} @cite{thomason-1984} @cite{cariani-santorio-2018} @cite{klecha-2016} @cite{abusch-1997}

Framework-agnostic relational structure on worlds: 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 (@cite{lewis-1979}, @cite{cariani-santorio-2018}). This is the substrate of the historical modal base used by metaphysical and future-oriented modality.

Key Concepts

1. Partial history time predicates — isActualHistory, isFutureHistory, etc. The framework-neutral interval predicates over LE Time / LT Time that index the situation-base slices. Named for @cite{klecha-2016} Definition 3.
2. World history function — the relation between a ⟨world, time⟩ point and the worlds that share its history up to that time.
3. Historical/actual/future bases — the three temporal slices of the historical modal base, defined as situations whose time component satisfies one of the partial-history predicates.
4. Klecha 2016 ULC derivation — the Upper Limit Constraint (@cite{abusch-1997}) is derived from actualHistoryBase membership by .2 projection, rather than stipulated.
5. Historical equivalence — the equivalence relation ≃_t of @cite{condoravdi-2002} §4.1.
6. Metaphysical modal base — the equivalence class of the evaluation world under ≃_t.

What's not here

This file is foundational: it commits to no specific modal theory (Kratzer, Stalnaker selection, etc.). It defines the relational substrate that any modal theory referring to "historical alternatives" can use. The selectional semantics for will (@cite{cariani-santorio-2018}) lives in Theories/Semantics/Modality/Selectional.lean.

Partial History Taxonomy

@cite{klecha-2016} Definition 3 defines five kinds of partial history, distinguished 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 are used in the core DOX/CIR mechanism, but the full taxonomy is needed for extensions (e.g., prospective is the temporal component of historicalBase below).

These are framework-neutral interval predicates over LE Time / LT Time; the @cite{klecha-2016} citation is for the terminology, not the mathematical content (which is just ≤, <, >, ≥).

def Core.Modality.HistoricalAlternatives.isMaximalHistory {Time : Type u_1} (_evalTime _historyTime : Time) : Prop

Maximal history: unrestricted temporal extent. @cite{klecha-2016} Definition 3(v): Ω_t = all histories.

Equations

• Core.Modality.HistoricalAlternatives.isMaximalHistory _evalTime _historyTime = True

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

Actual history: temporal component ends at or before t. @cite{klecha-2016} Definition 3(vi): 𝒜_t = {i : τ(i) = (-∞, t]}.

Equations

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

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

Past history: temporal component ends strictly before t. @cite{klecha-2016} Definition 3(viii): 𝒫_t = {i : τ(i) = (-∞, t)}. Distinct from actual: past excludes t itself.

Equations

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

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

Future history: temporal component starts strictly after t. @cite{klecha-2016} Definition 3(vii): ℱ_t = {j : τ(j) = (t, ∞)}.

Equations

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

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

Prospective history: temporal component starts at or after t. @cite{klecha-2016} Definition 3(ix): ℙ_t = {j : τ(j) = [t, ∞)}. This is exactly the temporal component of historicalBase below: s'.time ≥ s.time.

Equations

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

theorem Core.Modality.HistoricalAlternatives.actual_future_complementary {Time : Type u_1} [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 Core.Modality.HistoricalAlternatives.past_prospective_complementary {Time : Type u_1} [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 Core.Modality.HistoricalAlternatives.past_implies_actual {Time : Type u_1} [Preorder Time] (evalTime historyTime : Time) (h : isPastHistory evalTime historyTime) : isActualHistory evalTime historyTime

Past ⊂ actual: strict past implies actual.

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

Future ⊂ prospective: strict future implies prospective.

theorem Core.Modality.HistoricalAlternatives.actual_and_prospective_iff_simultaneous {Time : Type u_1} [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 Core.Modality.HistoricalAlternatives.past_future_disjoint {Time : Type u_1} [Preorder Time] (evalTime historyTime : Time) : ¬(isPastHistory evalTime historyTime ∧ isFutureHistory evalTime historyTime)

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

World History Functions and Situation Bases

def Core.Modality.HistoricalAlternatives.WorldHistory (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

World history function: given a world and time, returns 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.

Intuition: At time t in world w, multiple futures are possible. The historical alternatives are all worlds that share the same past with w up to t.

Equations

• Core.Modality.HistoricalAlternatives.WorldHistory W Time = (Core.WorldTimeIndex W Time → Set W)

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

Historical modal base: situations whose worlds agree with s up to τ(s), and whose times are at or after τ(s).

Following @cite{thomason-1984} and @cite{condoravdi-2002}:

• Past is fixed (determined)
• Future branches (open)

hist(s) = {s' : w_{s'} ∈ H(wₛ, τ(s)) ∧ τ(s') ≥ τ(s)}

Equations

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

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

Actual history base (@cite{klecha-2016} DOX): situations whose worlds agree with s and whose times are at or before τ(s).

This is the temporal mirror of historicalBase (which uses ≥). DOX returns actual histories — world-time pairs where the temporal component ends at the evaluation time: 𝒜_t = {i : τ(i) = (-∞, t]}.

Equations

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

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

Future history base (@cite{klecha-2016} CIR): situations whose worlds agree with s and whose times are strictly after τ(s).

CIR returns future histories — world-time pairs where the temporal component departs from the evaluation time: ℱ_t = {j : τ(j) = (t, ∞)}.

Equations

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

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

A world history is reflexive if every world agrees with itself.

Equations

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

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

A world history is symmetric: if w' agrees with w up to t, then w agrees with w' up to t.

@cite{condoravdi-2002} §4.1, condition (i): ≃_t is an equivalence relation for all t. Symmetry ensures historical equivalence is bidirectional — "sharing a history" is a mutual relationship.

Equations

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

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

A world history 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 Core.Modality.HistoricalAlternatives.WorldHistory.backwardsClosed {W : Type u_1} {Time : Type u_2} [LE Time] (h : WorldHistory W Time) : Prop

A world history is backwards-closed: if w' agrees with w up to t, and t' ≤ t, then w' agrees with w up to t'.

"If two worlds agree up to time t, they also agree up to any earlier time." @cite{condoravdi-2002} §4.1, condition (ii).

Equations

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

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

Standard historical modal base properties. @cite{condoravdi-2002} §4.1: ≃_t is an equivalence relation (i) that is monotone in time (ii).

• 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 Core.Modality.HistoricalAlternatives.TProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

A temporal proposition: true or false at each situation.

This is the situation-semantic analog of Prop' W.

Equations

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

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

Lift a world proposition to a temporal proposition.

The lifted proposition is true at situation s iff the original proposition is true at s.world.

Equations

• Core.Modality.HistoricalAlternatives.liftProp p s = p s.world

def Core.Modality.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

• Core.Modality.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 @cite{abusch-1997} §7 ("the now of an epistemic alternative is an upper limit for the denotation of tenses"), with the presuppositional construal due to @cite{heim-1994-comments} and endorsed by Abusch 1997 fn 20. @cite{klecha-2016} §4.2 derives the same constraint from the temporal character of the doxastic modal base: DOX returns actual histories 𝒜_t (Klecha eq 35a); membership in 𝒜_t 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 @cite{klecha-2016}'s account from @cite{abusch-1997}'s ("identical in spirit, if not in implementation" per Klecha §4.2): 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 Theories/Semantics/Modality/TemporalConstraint.lean.

Note: the modal-alternative quantification in Abusch's formulation ("the now of an epistemic alternative") is captured here at the substrate level by WorldHistory membership; the value-level projection s'.time ≤ s.time recovers Abusch's bare-≤ form.

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

A situation in historicalBase has prospective time: s' ∈ historicalBase h s → isProspectiveHistory s.time s'.time.

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

A situation in actualHistoryBase has actual time: s' ∈ actualHistoryBase h s → isActualHistory s.time s'.time.

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

Modal-layer Upper Limit Constraint (@cite{abusch-1997}'s formulation that quantifies over doxastic alternatives, NOT just times). An embedded situation s' satisfies the modal-layer ULC relative to a matrix situation s and a doxastic accessibility history iff s' is a member of s's actual-history base (i.e., s' agrees with s on world history up to s.time, and s'.time ≤ s.time).

The value-level Theories/Semantics/Tense/Basic.lean.upperLimitConstraint is the .2-projection of this modal-layer formulation; the world component of the conjunction is what carries the doxastic-alternative quantification Abusch's original prose statement requires.

Equations

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

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

The modal-layer Upper Limit Constraint implies the value-level one (embeddedSituation.time ≤ matrixSituation.time). The proof is .2 projection through the actualHistoryBase definition. This is the structural soundness lemma justifying the value-level Theories/Semantics/Tense/Basic.lean.upperLimitConstraint as a faithful reduction of @cite{abusch-1997}'s modal formulation.

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

A situation in futureHistoryBase has future time: s' ∈ futureHistoryBase h s → isFutureHistory s.time s'.time.

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

futureHistoryBase ⊆ historicalBase: future situations are prospective. This is the situation-semantic instantiation of future_implies_prospective.

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

actualHistoryBase ∩ historicalBase contains only simultaneous situations: if s'.time ≤ s.time and s'.time ≥ s.time, then s'.time = s.time. This is the situation-semantic instantiation of actual_and_prospective_iff_simultaneous.

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

Actual and future history bases are disjoint on the time component: no situation can have time both ≤ t and > t. This is the situation-semantic instantiation of past_future_disjoint (actual ∩ future = ∅ since actual ⊃ past).

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

Every situation is in actualHistoryBase ∪ futureHistoryBase (on the time component): for any s', either s'.time ≤ s.time or s'.time > s.time. This is the situation-semantic instantiation of actual_future_complementary.

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

Converse: prospective time + world agreement → membership in historicalBase. The time predicate fully characterizes the temporal component of the base.

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

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

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

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

Historical Equivalence

@cite{condoravdi-2002} §4.1: 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 Core.Modality.HistoricalAlternatives.histEquiv {W : Type u_1} {Time : Type u_2} (history : WorldHistory 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

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

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

histEquiv history t is an equivalence relation when history satisfies the standard properties. This is the content of @cite{condoravdi-2002} §4.1, condition (i).

Equations

• ⋯ = ⋯

def Core.Modality.HistoricalAlternatives.histSetoid {W : Type u_1} {Time : Type u_2} {history : WorldHistory 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

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

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

histEquiv_equivalence from bundled HistoricalProperties.

Equations

• ⋯ = ⋯

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

histSetoid from bundled HistoricalProperties.

Equations

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

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

Historical equivalence is reflexive (from WorldHistory.reflexive).

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

Historical equivalence is symmetric (from WorldHistory.symmetric).

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

Historical equivalence is transitive (from WorldHistory.transitive).

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

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

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

@cite{condoravdi-2002} §4.1: "as time advances the set of metaphysical alternatives to any given world decreases."

The function t ↦ { w' | w ≃_t w' } is antitone: later times yield smaller (or equal) equivalence classes.

Metaphysical Modal Base

@cite{condoravdi-2002} §4.1: for modals expressing metaphysical modality, the modal base consists of historical alternatives: MB(w,t) = {w' | w ≃_t w'}. This is the maximal modal base compatible with the world's history up to t.

def Core.Modality.HistoricalAlternatives.metaphysicalBase {W : Type u_1} {Time : Type u_2} (history : WorldHistory 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

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

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

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

Settledness and Diversity

@cite{condoravdi-2002} §4.1: 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** [45] is the felicity condition for
associating a metaphysical modal base with a possibility modal:
the modal base must contain worlds that disagree on the property. 

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

Settledness [44]: within each equivalence class of the common ground, the property P is resolved uniformly — all historically equivalent worlds agree on whether P holds.

@cite{condoravdi-2002}: "the past and the present are settled."

Equations

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

def Core.Modality.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 [45]: there exists a world in the common ground whose modal base contains worlds that disagree on P.

This is the felicity condition for associating a metaphysical modal base with a possibility modal applying to property P. Without diversity, the modal assertion would be equivalent to a non-modal assertion, violating the distinctness requirement.

Equations

• Core.Modality.HistoricalAlternatives.diverse MB cg t P = ∃ (w : W), w ∈ cg ∧ ∃ (w' : W), w' ∈ MB w t ∧ ∃ (w'' : W), w'' ∈ MB w t ∧ P w' ∧ ¬P w''

theorem Core.Modality.HistoricalAlternatives.settled_not_diverse {W : Type u_1} {Time : Type u_2} (history : WorldHistory W Time) (MB : W → Time → Set W) (cg : Set W) (t : Time) (P : W → Prop) (hMB : ∀ (w : W), w ∈ cg → ∀ (w' : W), w' ∈ MB w t → histEquiv history t w w') (hSettled : settled history 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.

This is the key theorem blocking metaphysical readings for settled properties.

theorem Core.Modality.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, and both are accessible from some w via MB, then diversity holds.