Cariani (2021): The Modal Future, chapters 5 to 8 and 11

Cariani develops the selection semantics of Cariani and Santorio, on which will selects a world from its modal domain, from the perspective of the world of evaluation, and evaluates its prejacent there. A modal of this kind is necessity along the graph of a function, so it commutes with negation and validates excluded middle, while the hybrid semantics of chapter 5, which adds existential quantification over later times, keeps excluded middle and loses non-contradiction. Chapter 6 replaces the fixed domain with a modal base, the historical partition, which repairs will under epistemic possibility and makes will the identity on contents over a realistic base. Will B and historical might not B are then consistent at a world but accepted together by no information state that respects the partition. Chapter 7 states will in Condoravdi's terms, selecting a world and extending the interval forward, and chapter 8 lets if restrict the modal base, which gives will-conditionals Stalnaker's truth conditions and import–export. Chapter 11 keeps contexts classical and locates the open future in indeterminacy over which context an utterance has, and rejects the convergent thin red line of Belnap and Green.

Main results

• forall_hybrid_or_not_iff, forall_not_hybrid_and_not_iff: the hybrid semantics validates excluded middle where a later time exists and non-contradiction only where at most one does.
• hybrid_tacos: the tacos model, where I will have tacos and I will not have tacos are both true.
• not_diamond_will_fixed, diamond_will_historical: the Oedipus bug of Figure 6.1 and its repair by the modal base of Figure 6.4.
• not_accepts_will_and_might_not: Fact 6.4, no eligible state accepts a historical future-might contradiction, which fmc_point_consistent shows consistent at a world.
• not_will_and_might_not_will, not_not_will_and_might_will, fork_not_will_and_might_will: Kissine's inconsistencies over transitive and Euclidean bases, and the fork model.
• pres_woll_neg_iff, not_pres_WOLL_and_neg: selectional WOLL commutes with negation and Condoravdi's universal WOLL does not.
• pres_woll_iff_of_mem, pres_woll_of_pres_WOLL: over a realistic base selectional WOLL is the prejacent at the world itself, which Condoravdi's WOLL entails.
• willIf_willIf, willIf_univ_eq_selectionConditional: import–export for will-conditionals, and over the universal base they are Stalnaker's conditional.
• not_accepts_willIf_and_mightIf_not: Fact 8.3, the conditional future-might contradiction.
• indeterminate_sat: the lifting argument, Fact 11.1, which needs only the K logic of D.
• not_exists_convergent_centered_trl: convergence and centering of a thin red line are inconsistent on a branching moment (Figure 11.4).

Implementation notes

• A modal base is an accessibility relation, and will along it is SelectionFunction.modal, whose generalized transparency, Fact 6.1, is SelectionFunction.modal_eq_id. The fixed domain H of chapter 5 is the constant relation to H, which is Cariani and Santorio's will.
• An information state is a set of worlds, accepting the propositions that include it.
• Cariani's ext(I), the interval I extended to the future, is the forward interval from the start of I, and the modal base is indexed by that start, as in Condoravdi2002.

TODO

• The counterhistorical restriction of §8.6 and the identity collapse of §8.8 (Fact 8.4).

References

• [Car21]
• [CS18]
• [Kis08]
• [Con02]
• [BG94]

The hybrid semantics

The hybrid semantics of §5.2 (p. 80) evaluates the prejacent of will at the selected world at some later time. It is possibility along an index relation that is serial wherever a later time exists and functional only where at most one does, so it validates excluded middle and loses non-contradiction and Negation Swap (p. 83), the failure of scopelessness for which chapter 7 rejects it (p. 117).

def Cariani2021.hybridRel {W : Type u_1} {T : Type u_2} [LT T] (s : Conditional.SelectionFunction W) (H : Set W) : SetRel (W × T) (W × T)

The index relation of the hybrid semantics relates (w, t) to the world selected from H at each later time.

Equations

• Cariani2021.hybridRel s H = {p : (W × T) × W × T | p.2.1 = s.sel p.1.1 H ∧ p.1.2 < p.2.2}

def Cariani2021.hybrid {W : Type u_1} {T : Type u_2} [LT T] (s : Conditional.SelectionFunction W) (H : Set W) (A : W × T → Prop) : W × T → Prop

Hybrid will, possibility along hybridRel, holds of A at (w, t) when A holds at the world selected from H at some later time.

Equations

• Cariani2021.hybrid s H A = ModalLogic.Diamond (Cariani2021.hybridRel s H) A

theorem Cariani2021.exists_hybridRel_iff {W : Type u_1} {T : Type u_2} [LT T] {s : Conditional.SelectionFunction W} {H : Set W} {i : W × T} : (∃ (j : W × T), (i, j) ∈ hybridRel s H) ↔ ∃ (u : T), i.2 < u

theorem Cariani2021.forall_hybrid_or_not_iff {W : Type u_1} {T : Type u_2} [LT T] {s : Conditional.SelectionFunction W} {H : Set W} {i : W × T} : (∀ (A : W × T → Prop), hybrid s H A i ∨ hybrid s H (fun (j : W × T) => ¬A j) i) ↔ ∃ (u : T), i.2 < u

The hybrid semantics validates excluded middle at an index exactly when a later time exists.

theorem Cariani2021.forall_not_hybrid_and_not_iff {W : Type u_1} {T : Type u_2} [LT T] {s : Conditional.SelectionFunction W} {H : Set W} {i : W × T} : (∀ (A : W × T → Prop), ¬(hybrid s H A i ∧ hybrid s H (fun (j : W × T) => ¬A j) i)) ↔ ∀ ⦃u : T⦄, i.2 < u → ∀ ⦃u' : T⦄, i.2 < u' → u = u'

The hybrid semantics validates non-contradiction at an index exactly when at most one later time exists.

theorem Cariani2021.hybrid_tacos (s : Conditional.SelectionFunction Unit) : hybrid s Set.univ (fun (j : Unit × ℕ) => j.2 = 1) ((), 0) ∧ hybrid s Set.univ (fun (j : Unit × ℕ) => ¬j.2 = 1) ((), 0)

In the tacos model of p. 83, with Monday 0, tacos on Tuesday 1 and pasta on Wednesday 2, on Monday I will have tacos and I will not have tacos are both true.

The Oedipus model

In Figure 6.1 (p. 94) the historical possibilities of the context, w0 to w3, agree that Oedipus marries Jocasta, and the epistemic state also admits w4, in which he marries Kate. Over the fixed domain of the historical possibilities, it is possible that Oedipus will avoid incest is false whatever the selection function, since every selection from the domain marries Jocasta (p. 95). Over the modal base of Figure 6.4 (p. 105), which gives w4 its own cell, it is true.

inductive Cariani2021.World : Type

The five worlds of Figure 6.1.

• w0 : World
• w1 : World
• w2 : World
• w3 : World
• w4 : World

@[instance_reducible]

instance Cariani2021.instDecidableEqWorld : DecidableEq World

Equations

• Cariani2021.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cariani2021.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Cariani2021.instReprWorld.repr Cariani2021.World.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cariani2021.World.w0")).group prec✝
• Cariani2021.instReprWorld.repr Cariani2021.World.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cariani2021.World.w1")).group prec✝
• Cariani2021.instReprWorld.repr Cariani2021.World.w2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cariani2021.World.w2")).group prec✝
• Cariani2021.instReprWorld.repr Cariani2021.World.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cariani2021.World.w3")).group prec✝
• Cariani2021.instReprWorld.repr Cariani2021.World.w4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cariani2021.World.w4")).group prec✝

@[instance_reducible]

instance Cariani2021.instReprWorld : Repr World

Equations

• Cariani2021.instReprWorld = { reprPrec := Cariani2021.instReprWorld.repr }

@[instance_reducible]

instance Cariani2021.instFintypeWorld : Fintype World

Equations

• Cariani2021.instFintypeWorld = { elems := { val := ↑Cariani2021.World.enumList, nodup := Cariani2021.World.enumList_nodup }, complete := Cariani2021.instFintypeWorld._proof_1 }

def Cariani2021.avoidIncest : Set World

The proposition that Oedipus avoids incest, marrying Kate.

Equations

• Cariani2021.avoidIncest = {Cariani2021.World.w4}

def Cariani2021.historicalPossibilities : Set World

The historical possibilities of the context, in which Oedipus marries Jocasta.

Equations

• Cariani2021.historicalPossibilities = {Cariani2021.World.w0, Cariani2021.World.w1, Cariani2021.World.w2, Cariani2021.World.w3}

def Cariani2021.epistemic : SetRel World World

The epistemic modal base admits every world.

Equations

• Cariani2021.epistemic = Set.univ

def Cariani2021.historical : SetRel World World

The historical modal base of Figure 6.4 partitions the worlds into the historical possibilities of the context and w4.

Equations

• Cariani2021.historical = {p : Cariani2021.World × Cariani2021.World | p.1 = Cariani2021.World.w4 ↔ p.2 = Cariani2021.World.w4}

instance Cariani2021.instIsReflWorldHistorical : historical.IsRefl

theorem Cariani2021.not_diamond_will_fixed (s : Conditional.SelectionFunction World) : ¬ModalLogic.Diamond epistemic (fun (x : World) => x ∈ (CarianiSantorio2018.will s historicalPossibilities) avoidIncest) World.w0

Over the fixed domain of the historical possibilities, it is possible that Oedipus will avoid incest is false at the actual world, whatever the selection function (p. 95).

theorem Cariani2021.diamond_will_historical (s : Conditional.SelectionFunction World) : ModalLogic.Diamond epistemic (fun (x : World) => x ∈ (s.modal historical) avoidIncest) World.w0

Over the historical modal base, it is possible that Oedipus will avoid incest is true at the actual world, w4 witnessing it (p. 106).

Future-might contradictions

An information state is historically eligible when it cuts through no cell of the historical partition (p. 109). Over a realistic base, will B and historical might not B, (20) of p. 107, are consistent at a world but accepted together by no nonempty eligible state, which classifies them as coordinated-informationally inconsistent, Fact 6.4 (p. 110, proof p. 114).

def Cariani2021.IsEligible {W : Type u_1} (R : SetRel W W) (S : Set W) : Prop

An information state is historically eligible for a modal base when it holds every world the base relates to its own.

Equations

• Cariani2021.IsEligible R S = ∀ w ∈ S, ∀ (v : W), (w, v) ∈ R → v ∈ S

theorem Cariani2021.not_accepts_will_and_might_not {W : Type u_1} {s : Conditional.SelectionFunction W} {R : SetRel W W} [R.IsRefl] {S B : Set W} (hS : IsEligible R S) (hne : S.Nonempty) : ¬(S ⊆ (s.modal R) B ∧ S ⊆ R.preimage Bᶜ)

No nonempty eligible state accepts both will B and historical might not B, Fact 6.4.

theorem Cariani2021.fmc_point_consistent (s : Conditional.SelectionFunction CarianiSantorio2018.W) : CarianiSantorio2018.W.cw ∈ (s.modal (CarianiSantorio2018.frame.alt 0)) CarianiSantorio2018.warriorsCap ∩ (CarianiSantorio2018.frame.alt 0).preimage CarianiSantorio2018.warriorsCapᶜ

Historical future-might contradictions are consistent at a world. In the Sports Fan model of [CS18], at the Warriors-cap world Cynthia will wear a Warriors cap and she might not are both true over today's historical alternatives.

Kissine's argument

Kissine argues against a modal will from the inconsistency of will A and might not will A and of not will A and might will A, (12) and (15), which holds for a quantificational will over a transitive and over a Euclidean base respectively; over a serial base with both properties might will A collapses to will A (ModalLogic.diamond_box_iff). The fork model of footnote 3 (p. 100) is transitive but not Euclidean, and satisfies (15). Selection escapes the argument, which assumes universal force (p. 101).

theorem Cariani2021.not_will_and_might_not_will {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [R.IsTrans] : ¬(ModalLogic.Box R p w ∧ ModalLogic.Diamond R (fun (v : W) => ¬ModalLogic.Box R p v) w)

Over a transitive base will A and might not will A is inconsistent for a quantificational will.

theorem Cariani2021.not_not_will_and_might_will {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [ModalLogic.IsEuclidean R] : ¬(¬ModalLogic.Box R p w ∧ ModalLogic.Diamond R (ModalLogic.Box R p) w)

Over a Euclidean base not will A and might will A is inconsistent for a quantificational will.

def Cariani2021.fork : SetRel (Fin 3) (Fin 3)

The fork model relates 0 to 1 and 2 and each of these to itself.

Equations

• Cariani2021.fork = {p : Fin 3 × Fin 3 | p.1 = 0 ∧ p.2 ≠ 0 ∨ p.1 ≠ 0 ∧ p.2 = p.1}

@[instance_reducible]

instance Cariani2021.instDecidablePredProdFinOfNatNatMemSetRelFork : DecidablePred fun (x : Fin 3 × Fin 3) => x ∈ fork

Equations

• Cariani2021.instDecidablePredProdFinOfNatNatMemSetRelFork p = { decide := decide (p.1 = 0 ∧ p.2 ≠ 0) || decide (p.1 ≠ 0 ∧ p.2 = p.1), reflects_decide := ⋯ }

instance Cariani2021.instIsTransFinOfNatNatFork : fork.IsTrans

theorem Cariani2021.not_isEuclidean_fork : ¬ModalLogic.IsEuclidean fork

theorem Cariani2021.fork_not_will_and_might_will : ¬ModalLogic.Box fork (fun (x : Fin 3) => x = 1) 0 ∧ ModalLogic.Diamond fork (ModalLogic.Box fork fun (x : Fin 3) => x = 1) 0

In the fork model, with A true at 1 and false at 2, not will A and might will A is true at 0.

Selection semantics, Condoravdi style

Chapter 7 states will in Condoravdi's framework: WOLL selects a world out of the historical modal base and extends the interval of evaluation forward to the end of time, and the present locates the interval at now (p. 126). Neither contribution quantifies, so will and not commute (p. 127), where Condoravdi's universal WOLL does not. Over a realistic base selectional WOLL is the prejacent at the world itself, the limited collapse Condoravdi's diversity condition is designed to avoid (p. 128).

def Cariani2021.woll {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (s : Conditional.SelectionFunction W) (MB : W → T → Set W) (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

Selectional WOLL instantiates the property throughout the forward interval from the start of the reference interval at the world selected from the modal base there (p. 126).

Equations

• Cariani2021.woll s MB Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => ∃ (t₀ : T), IsLeast ↑t ↑t₀ ∧ Aspect.At (Interval.Ici ↑t₀) (s.sel w (MB w t₀)) Q

def Cariani2021.neg {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

Negation of a sorted property, true at an interval where the property is not instantiated (p. 126).

Equations

• Cariani2021.neg Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => ¬Aspect.At t w Q

@[simp]

theorem Cariani2021.pres_woll_iff {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {s : Conditional.SelectionFunction W} {MB : W → T → Set W} {Q : Aspect.SortedProperty W E T} {w : W} {now : T} : Condoravdi2002.PRES now (woll s MB Q) w ↔ Aspect.At (Interval.Ici ↑now) (s.sel w (MB w now)) Q

At the present, selectional WOLL holds when the world selected from the base at the present has the property throughout the forward interval.

theorem Cariani2021.pres_woll_neg_iff {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {s : Conditional.SelectionFunction W} {MB : W → T → Set W} {Q : Aspect.SortedProperty W E T} {w : W} {now : T} : Condoravdi2002.PRES now (woll s MB (neg Q)) w ↔ ¬Condoravdi2002.PRES now (woll s MB Q) w

Will not A and not will A have complementary truth conditions (p. 127).

theorem Cariani2021.not_pres_WOLL_and_neg {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {MB : W → T → Set W} {Q : Aspect.SortedProperty W E T} {w : W} {now : T} {w₁ w₂ : W} (h₁ : w₁ ∈ MB w now) (h₂ : w₂ ∈ MB w now) (hQ₁ : Aspect.At (Interval.Ici ↑now) w₁ Q) (hQ₂ : ¬Aspect.At (Interval.Ici ↑now) w₂ Q) : ¬Condoravdi2002.PRES now (Condoravdi2002.WOLL MB Q) w ∧ ¬Condoravdi2002.PRES now (Condoravdi2002.WOLL MB (neg Q)) w

Condoravdi's universal WOLL does not commute with negation, since over a base whose worlds disagree on the property neither will A nor will not A holds.

theorem Cariani2021.pres_woll_iff_of_mem {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {s : Conditional.SelectionFunction W} {MB : W → T → Set W} {Q : Aspect.SortedProperty W E T} {w : W} {now : T} (h : w ∈ MB w now) : Condoravdi2002.PRES now (woll s MB Q) w ↔ Aspect.At (Interval.Ici ↑now) w Q

Over a realistic base selectional WOLL at the present is the prejacent at the world itself throughout the forward interval (p. 128).

theorem Cariani2021.pres_woll_of_pres_WOLL {W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {s : Conditional.SelectionFunction W} {MB : W → T → Set W} {Q : Aspect.SortedProperty W E T} {w : W} {now : T} (h : w ∈ MB w now) (hW : Condoravdi2002.PRES now (Condoravdi2002.WOLL MB Q) w) : Condoravdi2002.PRES now (woll s MB Q) w

Over a realistic base Condoravdi's universal WOLL entails selectional WOLL.

Will-conditionals

An if-clause restricts the modal base of the modal in its scope to the antecedent-worlds, f + A (Definition 8.1, p. 137), and will contributes the selection, so if A, will B holds where the world selected from the base restricted to A is a B-world, Stalnaker's conditional with a modal base (p. 133). Restricting twice is restricting once by the conjunction, so will-conditionals validate import–export (p. 140), and over a realistic base the conditional future-might contradiction is accepted by no eligible state, Fact 8.3 (p. 142, proof p. 152).

def Cariani2021.willIf {W : Type u_1} (s : Conditional.SelectionFunction W) (R : SetRel W W) (A : Set W) : CompleteLatticeHom (Set W) (Set W)

If A, will B, selectional will along the base restricted to the A-worlds.

Equations

• Cariani2021.willIf s R A = s.modal (R ∩ Set.univ ×ˢ A)

theorem Cariani2021.willIf_willIf {W : Type u_1} {s : Conditional.SelectionFunction W} {R : SetRel W W} {A B : Set W} (C : Set W) : (willIf s (R ∩ Set.univ ×ˢ A) B) C = (willIf s R (A ∩ B)) C

Import–export for will-conditionals, if A, if B, will C is if A and B, will C (p. 140).

theorem Cariani2021.willIf_univ_eq_selectionConditional {W : Type u_1} {s : Conditional.SelectionFunction W} {A : Set W} (hA : A.Nonempty) (B : Set W) : (willIf s Set.univ A) B = Conditional.selectionConditional s A B

Over the universal base, a will-conditional with a possible antecedent is Stalnaker's conditional (p. 133).

theorem Cariani2021.diamond_of_diamond_inter {W : Type u_1} {R : SetRel W W} {A : Set W} {w : W} {p : W → Prop} (h : ModalLogic.Diamond (R ∩ Set.univ ×ˢ A) p w) : ModalLogic.Diamond R (fun (v : W) => v ∈ A ∧ p v) w

If A, might B alone entails might (A and B), so semi-closure, Fact 8.2 (p. 142), holds for the restrictor analysis of if.

theorem Cariani2021.not_accepts_willIf_and_mightIf_not {W : Type u_1} {s : Conditional.SelectionFunction W} {R : SetRel W W} {A B : Set W} [R.IsRefl] {S : Set W} (hS : IsEligible R S) (hne : S.Nonempty) : ¬(S ⊆ (willIf s R A) B ∧ S ⊆ (R ∩ Set.univ ×ˢ A).preimage Bᶜ)

No nonempty eligible state accepts both if A, will B and if A, might not B, Fact 8.3.

Indeterminacy and the thin red line

Chapter 11 keeps every context classical, fixing a world, and reads the open future as indeterminacy over which of the contexts of a cloud an utterance has. A bare prediction has one content across the cloud, generalized transparency, and its truth there is indeterminate, so the normative status of asserting it is indeterminate too, the lifting argument of Fact 11.1 (p. 211, proof pp. 222-223). The determinacy operator D is necessity along a relation between contexts, and its indeterminacy I φ is ¬ D φ ∧ ¬ D ¬φ (p. 211). Against a flexible thin red line, convergence, that moments on one history share a thin red line, and centering, that the thin red line at a moment passes through it, are inconsistent once two branches leave a moment (Figure 11.4, p. 217).

def Cariani2021.Indeterminate {C : Type u_1} (R : SetRel C C) (φ : C → Prop) (c : C) : Prop

Indeterminacy along the determinacy relation R, ¬ D φ ∧ ¬ D ¬φ (p. 211).

Equations

• Cariani2021.Indeterminate R φ c = (¬ModalLogic.Box R φ c ∧ ¬ModalLogic.Box R (fun (c' : C) => ¬φ c') c)

theorem Cariani2021.indeterminate_sat {C : Type u_1} {R : SetRel C C} (cloud : Set C) {cu : C} {holds asserts sat : C → Prop} (hind : Indeterminate R holds cu) (hbridge : (∀ c ∈ cloud, asserts c) → ModalLogic.Box R asserts cu) (hcontent : ∀ c ∈ cloud, asserts c) (hnorm : ModalLogic.Box R (fun (c : C) => sat c ↔ asserts c → holds c) cu) : Indeterminate R sat cu

The lifting argument, Fact 11.1. If the truth of A in the context of the utterance is indeterminate, every context of the cloud has the speaker assert A, this is then determinate, and the truth norm determinately ties satisfaction of the norm to the truth of what is asserted, then whether the norm is satisfied is indeterminate. The argument uses only the K logic of D, though the book assumes S5 (p. 210).

theorem Cariani2021.not_exists_convergent_centered_trl {M : Type u_2} [PartialOrder M] [IsLeftLinear M] {m₁ m₂ m₃ : M} (h₂ : m₁ ≤ m₂) (h₃ : m₁ ≤ m₃) (h₂₃ : ¬(m₂ ≤ m₃ ∨ m₃ ≤ m₂)) : ¬∃ (trl : M → Flag M), (∀ (m : M), m ∈ trl m) ∧ ∀ (m m' : M) (h : Flag M), m ∈ h → m' ∈ h → trl m = trl m'

A thin red line assigning each moment a history cannot be both convergent and centered once two incomparable moments follow a common one (Figure 11.4).