Cariani and Santorio 2018: will done better

Cariani and Santorio analyse will as a modal that selects rather than quantifies. Its modal parameter is the set of historical alternatives of the context, will A is true at a world when A holds at the world a Stalnaker selection function picks from the parameter, and an if-clause restricts the parameter. Selection makes will a Boolean homomorphism, so it is scopeless with respect to negation, and gives will A the credence of A, where a universal analysis gives an open future credence 0. In their Sports Fan model the cap-conditional has credence 1/3 or 2/3, never its conditional probability 1/2, until contents are taken to be sets of pairs of a world and a selection function.

Main definitions

• will, willIf: selectional will, and if A, will B over the restricted parameter.
• Valid1, Valid2: truth at every context and at every index.
• content2D: the content of a sentence as a set of pairs of a world and a selection function.

Main results

• will_compl, willIf_compl: Negation Swap, unembedded and under an if-clause.
• will_excluded_middle, willIf_excluded_middle: excluded middle is valid₂.
• valid1_materialImp_will, not_valid2_materialImp_will: will A entails A at every context but not at every index.
• will_eq_core, necessity_compl_eq_iff: will is necessity along a selection, and a universal analysis commutes with negation only if it is one.
• will_alternatives_eq: the candidate worlds of a context give will one modal parameter.
• will_inter_self, measure_will: Transparency, so will A has the credence of A.
• measure_necessity_eq_zero: universal will gives an open future credence 0.
• credence_willIf_wearsCap, no_unconditional_one_half: the cap-conditional has credence 2/3 or 1/3, and no proposition of the model has credence 1/2.
• credence2D_willIf_wearsCap: over pairs the cap-conditional has its conditional probability.

Implementation notes

• A sentence is a map from a selection function and a modal parameter to a set of worlds, so an if-clause, rule (21), shifts the parameter.
• At an empty parameter will evaluates the junk selection; the paper restricts its conditional principles to antecedents compatible with the modal base (§7).
• Section and example numbers follow the accepted manuscript (Draft of November 2, 2015).

References

• F. Cariani and P. Santorio, Will done Better: Selection Semantics, Future Credence, and Indeterminacy (2018)
• R. C. Stalnaker, A Theory of Conditionals (1968)
• A. Kratzer, The Notional Category of Modality (1981)
• S. Kaufmann, Conditional Truth and Future Reference (2005)
• A. Hajek, Probabilities of Conditionals — Revisited (1989)

Selectional will

The clause for will is (16) of §5.2, and its collapse at the context is (18).

def CarianiSantorio2018.will {W : Type u_1} (s : Conditional.SelectionFunction W) (f : Set W) : CompleteLatticeHom (Set W) (Set W)

Will over the modal parameter f sends A to the worlds whose selection from f is an A-world, the selectional modal along the constant relation to f.

Equations

• CarianiSantorio2018.will s f = s.modal (SetRel.ofSuccessors fun (x : W) => f)

@[simp]

theorem CarianiSantorio2018.mem_will {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} {w : W} : w ∈ (will s f) A ↔ s.sel w f ∈ A

theorem CarianiSantorio2018.will_eq_core {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} : (will s f) A = (Function.graph fun (w : W) => s.sel w f).core A

Will is necessity along the graph of selection from f, a modal that quantifies over a single world (§5.2).

theorem CarianiSantorio2018.will_compl {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} : (will s f) Aᶜ = ((will s f) A)ᶜ

Will commutes with negation, which is Negation Swap (§7).

theorem CarianiSantorio2018.mem_will_of_mem {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} {w : W} (hw : w ∈ f) : w ∈ (will s f) A ↔ w ∈ A

At a world of the modal parameter, will A is true exactly when A is.

theorem CarianiSantorio2018.will_inter_self {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} : (will s f) A ∩ f = A ∩ f

On the modal parameter will A and A hold at the same worlds, which is Transparency (§8.1).

theorem CarianiSantorio2018.will_eq_selectionConditional {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} (hf : f.Nonempty) : (will s f) A = Conditional.selectionConditional s f A

On a possible modal parameter, will A is the selection conditional of [Sta68] with the modal parameter as antecedent.

Validity

def CarianiSantorio2018.Valid2 {W : Type u_1} (φ : Conditional.SelectionFunction W → Set W → Set W) : Prop

A sentence is valid₂ when it is true at every index, every world under every selection function and modal parameter.

Equations

• CarianiSantorio2018.Valid2 φ = ∀ (s : Conditional.SelectionFunction W) (f : Set W), φ s f = Set.univ

def CarianiSantorio2018.Valid1 {W : Type u_1} (φ : Conditional.SelectionFunction W → Set W → Set W) : Prop

A sentence is valid₁ when it is true at every context, an index whose world lies in the modal parameter.

Equations

• CarianiSantorio2018.Valid1 φ = ∀ (s : Conditional.SelectionFunction W) (f : Set W), f ⊆ φ s f

theorem CarianiSantorio2018.Valid2.valid1 {W : Type u_1} {φ : Conditional.SelectionFunction W → Set W → Set W} (h : Valid2 φ) : Valid1 φ

theorem CarianiSantorio2018.will_excluded_middle {W : Type u_1} {A : Set W} : Valid2 fun (s : Conditional.SelectionFunction W) (f : Set W) => (will s f) A ∪ (will s f) Aᶜ

Will Excluded Middle is valid₂ (§7).

theorem CarianiSantorio2018.valid1_materialImp_will {W : Type u_1} {A : Set W} : Valid1 fun (s : Conditional.SelectionFunction W) (f : Set W) => Conditional.materialImp ((will s f) A) A

Every context at which will A is true verifies A.

If-clauses

An if-clause restricts the modal parameter of will to the antecedent-worlds, by rule (21) of §5.3.1.

def CarianiSantorio2018.willIf {W : Type u_1} (s : Conditional.SelectionFunction W) (f A : Set W) : CompleteLatticeHom (Set W) (Set W)

If A, will B is will B over the modal parameter restricted to the A-worlds.

Equations

• CarianiSantorio2018.willIf s f A = CarianiSantorio2018.will s (f ∩ A)

theorem CarianiSantorio2018.willIf_compl {W : Type u_1} (s : Conditional.SelectionFunction W) {f A B : Set W} : (willIf s f A) Bᶜ = ((willIf s f A) B)ᶜ

Will commutes with negation under an if-clause, which is Negation Swap in conditionals (§7). Since the if-clause only shifts the parameter, the narrow and the wide form are this one equation.

theorem CarianiSantorio2018.willIf_excluded_middle {W : Type u_1} {A B : Set W} : Valid2 fun (s : Conditional.SelectionFunction W) (f : Set W) => (willIf s f A) B ∪ (willIf s f A) Bᶜ

Conditional Excluded Middle for will-conditionals is valid₂ (§7).

theorem CarianiSantorio2018.willIf_inter {W : Type u_1} (s : Conditional.SelectionFunction W) {f A B C : Set W} : (willIf s f A) B ∩ (willIf s f A) C = (willIf s f A) (B ∩ C)

Under modal subordination, If A, will B. Will C with the second will coindexed with the restricted parameter is if A, will (B and C), (24) of §5.3.1.

theorem CarianiSantorio2018.willIf_eq_selectionConditional {W : Type u_1} (s : Conditional.SelectionFunction W) {f A B : Set W} (h : (f ∩ A).Nonempty) : (willIf s f A) B = Conditional.selectionConditional s (f ∩ A) B

When the restricted parameter is possible, if A, will B is the selection conditional with the restricted parameter as antecedent.

Contexts

At a context the modal parameter of will is the set of historical alternatives of the context's world at its time (§3, §5.1).

theorem CarianiSantorio2018.mem_will_alternatives_iff {W : Type u_1} (s : Conditional.SelectionFunction W) {A : Set W} {w : W} {T : Type u_2} [Preorder T] {F : Temporal.TWFrame W T} {t : T} : w ∈ (will s (F.alternatives (w, t))) A ↔ w ∈ A

At a context will A is true exactly when A is, the collapse (18).

theorem CarianiSantorio2018.will_alternatives_eq {W : Type u_1} (s : Conditional.SelectionFunction W) {w : W} {T : Type u_2} [Preorder T] {F : Temporal.TWFrame W T} {t : T} {v : W} (hv : v ∈ F.alternatives (w, t)) : will s (F.alternatives (v, t)) = will s (F.alternatives (w, t))

Every candidate world of a context has the same historical alternatives, so the modal parameter of will, and with it the content of will A, is fixed even when it is indeterminate which context an utterance takes place in (§3).

Cognitive role

theorem CarianiSantorio2018.measure_will {W : Type u_1} (s : Conditional.SelectionFunction W) {f A : Set W} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (h : μ fᶜ = 0) : μ ((will s f) A) = μ A

Under a credence concentrated on the modal parameter, the content of will A has the credence of A (§8.1).

Universal will

The modal analyses the paper argues against make will necessity over the best open worlds, the necessity f g of [Kra81b] with the open worlds as modal base, such as the most likely open worlds of [Kau05b]. They differ in the ordering source g (§2.4, (14)).

theorem CarianiSantorio2018.necessity_compl_eq_iff {W : Type u_1} {f g : Modality.Background W} : (∀ (p : W → Prop), Modality.necessity f g pᶜ = (Modality.necessity f g p)ᶜ) ↔ ∃ (σ : W → W), ∀ (p : W → Prop), Modality.necessity f g p = p ∘ σ

A universal analysis commutes with negation for every prejacent exactly when it is truth at a selected world, so the scopelessness of §2.2 leaves no quantificational analysis but selection (§2.4).

theorem CarianiSantorio2018.not_necessity_or_necessity_compl {W : Type u_1} {A : Set W} {w : W} {f g : Modality.Background W} {v v' : W} (hv : v ∈ Modality.bestWorlds f g w) (hv' : v' ∈ Modality.bestWorlds f g w) (hA : v ∈ A) (hA' : v' ∉ A) : ¬(Modality.necessity f g (fun (x : W) => x ∈ A) w ∨ Modality.necessity f g (fun (x : W) => x ∈ Aᶜ) w)

On a parameter whose best worlds hold an A-world and a non-A-world, universal will verifies neither will A nor will not A, so its scope with negation matters (§2.4).

theorem CarianiSantorio2018.measure_necessity_eq_zero {W : Type u_1} {A : Set W} [MeasurableSpace W] (μ : MeasureTheory.Measure W) {f g : Modality.Background W} (h : ∀ᵐ (w : W) ∂μ, ¬Modality.bestWorlds f g w ⊆ A) : μ {w : W | Modality.necessity f g (fun (x : W) => x ∈ A) w} = 0

A credence certain that the best worlds hold a non-A-world gives universal will A credence 0, whatever the ordering source (§2.4).

Two-dimensional content

Uncertainty about the selection function joins uncertainty about the world when contents are sets of pairs of a world and a selection function (§8.2).

def CarianiSantorio2018.content2D {W : Type u_1} (φ : Conditional.SelectionFunction W → Set W → Set W) (f : Set W) : Set (W × Conditional.SelectionFunction W)

The 2D content of a sentence at a modal parameter is the set of pairs of a world and a selection function at which the sentence is true.

Equations

• CarianiSantorio2018.content2D φ f = {p : W × Conditional.SelectionFunction W | p.1 ∈ φ p.2 f}

@[simp]

theorem CarianiSantorio2018.mem_content2D {W : Type u_1} {f : Set W} {φ : Conditional.SelectionFunction W → Set W → Set W} {p : W × Conditional.SelectionFunction W} : p ∈ content2D φ f ↔ p.1 ∈ φ p.2 f

The Sports Fan model

inductive CarianiSantorio2018.W : Type

The three worlds of the Sports Fan scenario (§2.3), in which Cynthia wears a Warriors cap, a Giants cap, or no cap.

• cw : W
• cg : W
• cn : W

@[instance_reducible]

instance CarianiSantorio2018.instDecidableEqW : DecidableEq W

Equations

• CarianiSantorio2018.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CarianiSantorio2018.instReprW.repr : W → ℕ → Std.Format

Equations

• CarianiSantorio2018.instReprW.repr CarianiSantorio2018.W.cw prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CarianiSantorio2018.W.cw")).group prec✝
• CarianiSantorio2018.instReprW.repr CarianiSantorio2018.W.cg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CarianiSantorio2018.W.cg")).group prec✝
• CarianiSantorio2018.instReprW.repr CarianiSantorio2018.W.cn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CarianiSantorio2018.W.cn")).group prec✝

@[instance_reducible]

instance CarianiSantorio2018.instReprW : Repr W

Equations

• CarianiSantorio2018.instReprW = { reprPrec := CarianiSantorio2018.instReprW.repr }

@[instance_reducible]

instance CarianiSantorio2018.instFintypeW : Fintype W

Equations

• CarianiSantorio2018.instFintypeW = { elems := { val := ↑CarianiSantorio2018.W.enumList, nodup := CarianiSantorio2018.W.enumList_nodup }, complete := CarianiSantorio2018.instFintypeW._proof_1 }

def CarianiSantorio2018.frame : Temporal.TWFrame W ℕ

Cynthia's cap choice is the one matter of particular fact, dated tomorrow at time 1, so two worlds are historical alternatives up to a time when they agree on it or it is not yet dated.

Equations

• CarianiSantorio2018.frame = Temporal.TWFrame.ofDatedFacts (fun (x : CarianiSantorio2018.W) => 1) fun (x1 x2 : CarianiSantorio2018.W) => x1 = x2

@[simp]

theorem CarianiSantorio2018.alternatives_today (w : W) : frame.alternatives (w, 0) = Set.univ

Today, at time 0, nothing is settled, and every world is a historical alternative to every other.

def CarianiSantorio2018.warriorsCap : Set W

The proposition that Cynthia wears a Warriors cap.

Equations

• CarianiSantorio2018.warriorsCap = {CarianiSantorio2018.W.cw}

def CarianiSantorio2018.wearsCap : Set W

The proposition that Cynthia wears some cap, Warriors or Giants.

Equations

• CarianiSantorio2018.wearsCap = {CarianiSantorio2018.W.cw, CarianiSantorio2018.W.cg}

theorem CarianiSantorio2018.will_warriorsCap_indeterminate (s : Conditional.SelectionFunction W) : W.cw ∈ (will s (frame.alternatives (W.cw, 0))) warriorsCap ∧ W.cg ∉ (will s (frame.alternatives (W.cg, 0))) warriorsCap

Whatever the selection function, Cynthia will wear a Warriors cap is true at the context whose world is the Warriors-cap world and false at the one whose world is the Giants-cap world, so while the future is open its truth value is indeterminate (§3, §6).

theorem CarianiSantorio2018.not_valid2_materialImp_will : ¬Valid2 fun (s : Conditional.SelectionFunction W) (f : Set W) => Conditional.materialImp ((will s f) {W.cn}) {W.cn}

Will A does not valid₂-entail A. At the Warriors-cap world, with the no-cap world as the only modal parameter, Cynthia will wear no cap is true and its prejacent false.

@[instance_reducible]

instance CarianiSantorio2018.instMeasurableSpaceW : MeasurableSpace W

Equations

• CarianiSantorio2018.instMeasurableSpaceW = ⊤

instance CarianiSantorio2018.instDiscreteMeasurableSpaceW : DiscreteMeasurableSpace W

noncomputable def CarianiSantorio2018.cynthiaCredence : MeasureTheory.Measure W

The agent's credence is uniform, each cap choice getting 1/3.

Equations

• CarianiSantorio2018.cynthiaCredence = ProbabilityTheory.uniformOn Set.univ

theorem CarianiSantorio2018.credence_will_warriorsCap (s : Conditional.SelectionFunction W) (w : W) : cynthiaCredence.real ((will s (frame.alternatives (w, 0))) warriorsCap) = 1 / 3

Whatever the selection function and the world of the context, Cynthia will wear a Warriors cap has credence 1/3, that of its prejacent (§8.1).

def CarianiSantorio2018.histBase : Modality.Background W

The historical modal base, the background of the relation to today's historical alternatives.

Equations

• CarianiSantorio2018.histBase = Modality.Background.ofRel (SetRel.ofSuccessors fun (w : CarianiSantorio2018.W) => CarianiSantorio2018.frame.alternatives (w, 0))

@[simp]

theorem CarianiSantorio2018.accessibleWorlds_histBase (w : W) : histBase.accessibleWorlds w = Set.univ

theorem CarianiSantorio2018.credence_necessity_warriorsCap : cynthiaCredence {w : W | Modality.necessity histBase ⊥ (fun (x : W) => x ∈ warriorsCap) w} = 0

On the universal reading over the historical modal base, Cynthia will wear a Warriors cap has credence 0 (§2.3).

theorem CarianiSantorio2018.not_necessity_warriorsCap_or_compl (w : W) : ¬(Modality.necessity histBase ⊥ (fun (x : W) => x ∈ warriorsCap) w ∨ Modality.necessity histBase ⊥ (fun (x : W) => x ∈ warriorsCapᶜ) w)

On the universal reading will not and not will come apart, since at every world Cynthia will wear a Warriors cap and Cynthia will not wear a Warriors cap are both false (§2.4).

theorem CarianiSantorio2018.not_conditionalNecessity_wearsCap_or_compl (w : W) : ¬(Conditional.Restrictor.conditionalNecessity histBase ⊥ (fun (x : W) => x ∈ wearsCap) (fun (x : W) => x ∈ warriorsCap) w ∨ Conditional.Restrictor.conditionalNecessity histBase ⊥ (fun (x : W) => x ∈ wearsCap) (fun (x : W) => x ∈ warriorsCapᶜ) w)

The universal reading of if Cynthia wears a cap, she will wear a Warriors cap is the restrictor conditional, and it refutes Conditional Excluded Middle, since the restricted base holds both cap worlds.

The cap-conditional

The cap-conditional is (31) of §8.2.

theorem CarianiSantorio2018.mem_willIf_wearsCap_warriorsCap (s : Conditional.SelectionFunction W) (w v : W) : v ∈ (willIf s (frame.alternatives (w, 0)) wearsCap) warriorsCap ↔ v = W.cw ∨ v = W.cn ∧ s.sel W.cn wearsCap = W.cw

Under any selection function, if Cynthia wears a cap, she will wear a Warriors cap is true at the Warriors-cap world, false at the Giants-cap world, and true at the no-cap world exactly when that world selects the Warriors-cap world (footnote 32).

theorem CarianiSantorio2018.credence_willIf_wearsCap (s : Conditional.SelectionFunction W) (w : W) : cynthiaCredence.real ((willIf s (frame.alternatives (w, 0)) wearsCap) warriorsCap) = if s.sel W.cn wearsCap = W.cw then 2 / 3 else 1 / 3

The content of the cap-conditional has credence 2/3 when the no-cap world selects the Warriors-cap world and 1/3 otherwise (footnote 32).

theorem CarianiSantorio2018.cond_wearsCap_warriorsCap : cynthiaCredence[|wearsCap].real warriorsCap = 1 / 2

The probability of a Warriors cap conditional on some cap is 1/2.

theorem CarianiSantorio2018.no_unconditional_one_half (S : Set W) : cynthiaCredence.real S ≠ 1 / 2

No proposition over the Sports Fan model has credence 1/2, since every credence is a multiple of 1/3, so no reading of the cap-conditional has its conditional probability. It is an instance of the point of [Haj89] that conditional probabilities outnumber unconditional ones.

The two-dimensional cap-conditional

Which world the no-cap world selects for the cap antecedent is open, so the agent is uncertain between two selection functions, sw selecting the Warriors-cap world and sv the Giants-cap world (§8.2).

noncomputable def CarianiSantorio2018.candidate (v : W) (hv : v ∈ wearsCap) : Conditional.SelectionFunction W

A selection function selecting the cap world v for the no-cap world and the cap antecedent.

Equations

• CarianiSantorio2018.candidate v hv = ⋯.choose

theorem CarianiSantorio2018.candidate_sel {v : W} (hv : v ∈ wearsCap) : (candidate v hv).sel W.cn wearsCap = v

noncomputable def CarianiSantorio2018.sw : Conditional.SelectionFunction W

The candidate selecting the Warriors-cap world.

Equations

• CarianiSantorio2018.sw = CarianiSantorio2018.candidate CarianiSantorio2018.W.cw CarianiSantorio2018.sw._proof_1

noncomputable def CarianiSantorio2018.sv : Conditional.SelectionFunction W

The candidate selecting the Giants-cap world.

Equations

• CarianiSantorio2018.sv = CarianiSantorio2018.candidate CarianiSantorio2018.W.cg CarianiSantorio2018.sv._proof_1

theorem CarianiSantorio2018.sw_ne_sv : sw ≠ sv

def CarianiSantorio2018.pairs : Set (W × Conditional.SelectionFunction W)

The six pairs of a world and a candidate selection function.

Equations

• CarianiSantorio2018.pairs = Set.univ ×ˢ {CarianiSantorio2018.sw, CarianiSantorio2018.sv}

@[instance_reducible]

instance CarianiSantorio2018.instMeasurableSpaceSelectionFunctionW : MeasurableSpace (Conditional.SelectionFunction W)

Equations

• CarianiSantorio2018.instMeasurableSpaceSelectionFunctionW = ⊤

instance CarianiSantorio2018.instDiscreteMeasurableSpaceSelectionFunctionW : DiscreteMeasurableSpace (Conditional.SelectionFunction W)

theorem CarianiSantorio2018.credence2D_willIf_wearsCap (w : W) : (ProbabilityTheory.uniformOn pairs).real (content2D (fun (s : Conditional.SelectionFunction W) (f : Set W) => (willIf s f wearsCap) warriorsCap) (frame.alternatives (w, 0))) = cynthiaCredence[|wearsCap].real warriorsCap

The uniform credence over the six pairs gives the 2D content of the cap-conditional its conditional probability 1/2 (§8.2).