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, Lewis's notion, which Cariani and Santorio take as the modal base of will. A HistoricalAlternatives relation sends a world–time index to a set of worlds; restricted to times from, up to, or strictly after the index's own, it gives Condoravdi's historical base and Klecha's doxastic and circumstantial bases. A T × W frame determines its alternatives, the classes of its historical equivalence.

Main definitions

• HistoricalAlternatives, metaphysicalBase: the relation and its curried modal base.
• orientedBase: the alternatives at the times a tense cell admits, with historicalBase, actualHistoryBase and futureHistoryBase its nonpast, nonfuture and future instances.
• Temporal.TWFrame.alternatives: the historical alternatives of a T × W frame.
• settled, diverse: settledness over a common ground, and Condoravdi's diversity condition.

Main results

• time_le_of_mem_actualHistoryBase: Abusch's Upper Limit Constraint for the doxastic base.
• compare_mem_of_mem_orientedBase: an oriented base admits only its cell's orientations.
• actualHistoryBase_union_futureHistoryBase: the actual and future bases together hold the alternatives at all times.
• Temporal.TWFrame.alternatives_eq_of_mem: the alternatives of an alternative are the same.
• settled_not_diverse: a settled property is not diverse.
• settled_alternatives_iff: over a frame, settledness is historical necessity of the property or its negation.

References

• D. Lewis, Counterfactual dependence and time's arrow (1979)
• F. Cariani and P. Santorio, Will done better: selection semantics, future credence, and indeterminacy (2018)
• C. Condoravdi, Temporal interpretation of modals: modals for the present and for the past (2002)
• P. Klecha, Modality and embedded temporal operators (2016)
• D. Abusch, Sequence of tense and temporal de re (1997)
• R. H. Thomason, Combinations of tense and modality (1984)
• F. von Kutschera, T × W completeness (1997)

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

The historical alternatives of a world–time index are the worlds that agree with its world up to its time.

Equations

• HistoricalAlternatives W T = (Reference.Index W T → Set W)

@[reducible, inline]

abbrev HistoricalAlternatives.metaphysicalBase {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) : W → T → Set W

The metaphysical modal base of [Con02] is the relation curried, giving at a world and time the worlds that share the world's history up to that time.

Equations

• history.metaphysicalBase = Function.curry history

Bases oriented by a tense cell

A modal over historical alternatives evaluates its prejacent at the alternatives of its index and at times oriented to the index's time by a tense cell, Condoravdi's temporal orientation of a modal relative to its perspective. The historical base is oriented to the nonpast, and Klecha's doxastic and circumstantial bases to the nonfuture and the future.

def HistoricalAlternatives.orientedBase {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (s : Reference.Index W T) [LT T] (C : Finset Ordering) : Set (Reference.Index W T)

The base of the alternatives oriented by a tense cell C pairs the alternatives of an index with the times standing to the index's time in a position of C.

Equations

• history.orientedBase s C = history s ×ˢ {t : T | (s.time, t) ∈ Tense.toSetRel C}

@[reducible, inline]

abbrev HistoricalAlternatives.historicalBase {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (s : Reference.Index W T) [LT T] : Set (Reference.Index W T)

The historical modal base, the alternatives at times at or after the index's own, the past fixed and the future branching ([Tho84], [Con02]).

Equations

• history.historicalBase s = history.orientedBase s Tense.nonpast

@[reducible, inline]

abbrev HistoricalAlternatives.actualHistoryBase {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (s : Reference.Index W T) [LT T] : Set (Reference.Index W T)

The actual-history base, [Kle16]'s doxastic base, the alternatives at times at or before the index's own.

Equations

• history.actualHistoryBase s = history.orientedBase s (Semantics.Denotes.denote Tense.future)ᶜ

@[reducible, inline]

abbrev HistoricalAlternatives.futureHistoryBase {W : Type u_1} {T : Type u_2} (history : HistoricalAlternatives W T) (s : Reference.Index W T) [LT T] : Set (Reference.Index W T)

The future-history base, [Kle16]'s circumstantial base, the alternatives at times strictly after the index's own.

Equations

• history.futureHistoryBase s = history.orientedBase s (Semantics.Denotes.denote Tense.future)

theorem HistoricalAlternatives.mem_orientedBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} {C : Finset Ordering} [LT T] : s' ∈ history.orientedBase s C ↔ s'.world ∈ history s ∧ (s.time, s'.time) ∈ Tense.toSetRel C

theorem HistoricalAlternatives.compare_mem_of_mem_orientedBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} {C : Finset Ordering} [LinearOrder T] (h : s' ∈ history.orientedBase s C) : compare s'.time s.time ∈ C

On linear time the time of a situation in an oriented base stands to the index's time in a position of the cell.

theorem HistoricalAlternatives.mem_historicalBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} [PartialOrder T] : s' ∈ history.historicalBase s ↔ s'.world ∈ history s ∧ s.time ≤ s'.time

theorem HistoricalAlternatives.mem_actualHistoryBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} [PartialOrder T] : s' ∈ history.actualHistoryBase s ↔ s'.world ∈ history s ∧ s'.time ≤ s.time

theorem HistoricalAlternatives.mem_futureHistoryBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} [Preorder T] : s' ∈ history.futureHistoryBase s ↔ s'.world ∈ history s ∧ s.time < s'.time

theorem HistoricalAlternatives.time_le_of_mem_actualHistoryBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} [PartialOrder T] (h : s' ∈ history.actualHistoryBase s) : s'.time ≤ s.time

A situation in the actual-history base is no later than the index, the Upper Limit Constraint of [Abu97] as [Kle16] derives it from the doxastic base.

theorem HistoricalAlternatives.time_lt_of_mem_futureHistoryBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s s' : Reference.Index W T} [Preorder T] (h : s' ∈ history.futureHistoryBase s) : s.time < s'.time

theorem HistoricalAlternatives.orientedBase_sup {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s : Reference.Index W T} [LT T] (C D : Finset Ordering) : history.orientedBase s (C ⊔ D) = history.orientedBase s C ∪ history.orientedBase s D

Bases oriented by the join of two cells are the union of the bases.

theorem HistoricalAlternatives.actualHistoryBase_union_futureHistoryBase {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {s : Reference.Index W T} [LinearOrder T] : history.actualHistoryBase s ∪ history.futureHistoryBase s = history s ×ˢ Set.univ

On linear time the actual and future bases together hold the alternatives at all times.

The alternatives of a T × W frame

The historical alternatives of a T × W frame are its classes of historical equivalence, so a world is an alternative to itself and the alternatives of an alternative are the same.

def Temporal.TWFrame.alternatives {W : Type u_1} {T : Type u_2} [Preorder T] (F : TWFrame W T) : HistoricalAlternatives W T

The historical alternatives of a frame, at an index the worlds historically equivalent to its world at its time.

Equations

• F.alternatives i = {v : W | (F.sim i.time) i.world v}

@[simp]

theorem Temporal.TWFrame.mem_alternatives {W : Type u_1} {T : Type u_2} [Preorder T] {F : TWFrame W T} {w v : W} {t : T} : v ∈ F.alternatives (w, t) ↔ (F.sim t) w v

theorem Temporal.TWFrame.mem_alternatives_self {W : Type u_1} {T : Type u_2} [Preorder T] {F : TWFrame W T} {w : W} {t : T} : w ∈ F.alternatives (w, t)

theorem Temporal.TWFrame.alternatives_eq_of_mem {W : Type u_1} {T : Type u_2} [Preorder T] {F : TWFrame W T} {w v : W} {t : T} (h : v ∈ F.alternatives (w, t)) : F.alternatives (v, t) = F.alternatives (w, t)

Historical equivalence partitions the worlds, so an alternative of a world has the same alternatives as the world.

Settledness and diversity

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

A property is settled at a time over a common ground when the historical alternatives of each of its worlds agree on it ([Con02]). Past and present issues are settled, and future ones need not be.

Equations

• history.settled cg t P = ∀ w ∈ cg, ∀ w' ∈ history (w, t), P w ↔ P w'

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

A modal base meets the diversity condition of [Con02] for a property when some common-ground world sees worlds disagreeing on it.

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} {T : Type u_2} {history : HistoricalAlternatives W T} {MB : W → T → Set W} {cg : Set W} {t : T} {P : W → Prop} (hMB : ∀ w ∈ cg, MB w t ⊆ history (w, t)) (h : history.settled cg t P) : ¬diverse MB cg t P

A settled property is not diverse over a modal base within the metaphysical one, so metaphysical readings of possibility modals are blocked for settled properties.

theorem HistoricalAlternatives.settled_alternatives_iff {W : Type u_1} {T : Type u_2} [Preorder T] {F : Temporal.TWFrame W T} {cg : Set W} {t : T} {P : W → Prop} : F.alternatives.settled cg t P ↔ ∀ w ∈ cg, ModalLogic.Box (F.alt t) P w ∨ ModalLogic.Box (F.alt t) (fun (v : W) => ¬P v) w

Over the alternatives of a T × W frame, a property is settled at a time over a common ground exactly when, at every common-ground world, it or its negation is historically necessary.