Selectional Semantics for will

@cite{cariani-santorio-2018}

A selectional treatment of the future modal will: rather than quantifying universally or existentially over a modal base of historical alternatives, will applies its prejacent at a single selected world picked out by a Stalnaker-style selection function indexed by a modal parameter f.

⟦will_f A⟧^{w,s,g} = 1 iff ⟦A⟧^{s(w, g(f)), s, g} = 1

where s : SelectionFunction W is a contextually supplied selection function and g(f) is the relevant set of historical alternatives.

Three constraints @cite{cariani-santorio-2018}

@cite{cariani-santorio-2018} argue that an adequate theory of will must satisfy three constraints:

1. Modal character: will takes scope, interacts with negation and quantifiers, and embeds under attitudes — so it cannot be a pure present-tense or pure future-tense reference operator.
2. Scopelessness: under negation in matrix uses, will ¬A and ¬will A are equivalent (Negation Swap, negation_swap). Universal quantification over a non-trivial modal base cannot deliver this (universal_negation_swap_fails).
3. Cognitive role: a sincere assertion of will A is licensed by ordinary, non-extreme credence in A, not credence 1 (cognitive_role). A homogeneity / domain-width condition that requires uniform truth across the modal base would make assertion conditions too strong (universalWill collapses credence to 0/1).

What's here

• willSem, willSem_def: the selectional truth-condition.
• negation_swap, will_excluded_middle, unembedded_collapse: the three core scopelessness/CEM/factivity-on-base theorems.
• will_eq_A_on_modalParam: content transparency §8.1 footnote 30. As Set W, ‖will A‖ and ‖A‖ agree on every world in the modal parameter f. This is the substantive transparency claim from which the cognitive-role prediction follows.
• Valid2: validity₂ from paper §6 (truth at every ⟨s, f, w⟩, not just at the context). valid2_will_excluded_middle and valid2_negation_swap recast the matrix theorems in this stronger validity notion.
• willHistorical: will over the metaphysical modal base from Core/Modality/HistoricalAlternatives.lean — the bridge to the branching-time substrate.
• universalWill: the universal-quantifier reading used as a foil in @cite{cariani-santorio-2018}'s arguments. Shown to violate Negation Swap (universal_negation_swap_fails).
• cognitive_role: under any credence supported on the modal parameter, μ(‖will A‖) = μ(‖A‖) — the §8.1 prediction that decisively distinguishes selectional from universal accounts.

§1. The selectional truth-condition

def Semantics.Modality.Selectional.willSem {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : Prop

Selectional truth-condition for will @cite{cariani-santorio-2018}.

willSem s A f w is true iff the prejacent A holds at the world selected by s from the modal parameter f at w.

Reading: "will A" at w says A holds at the unique selected historical alternative s.sel w f.

Equations

• Semantics.Modality.Selectional.willSem s A f w = A (s.sel w f)

@[simp]

theorem Semantics.Modality.Selectional.willSem_def {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : willSem s A f w ↔ A (s.sel w f)

@[implicit_reducible]

instance Semantics.Modality.Selectional.willSem_decidable {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) [DecidablePred A] (f : Set W) (w : W) : Decidable (willSem s A f w)

willSem is decidable when its prejacent is.

Equations

• Semantics.Modality.Selectional.willSem_decidable s A f w = Semantics.Modality.Selectional.willSem_decidable._aux_1 s A f w

§2. Scopelessness, CEM, and unembedded collapse

theorem Semantics.Modality.Selectional.negation_swap {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : willSem s (fun (w' : W) => ¬A w') f w ↔ ¬willSem s A f w

Negation Swap @cite{cariani-santorio-2018}: under selectional semantics, will commutes with negation. will ¬A ↔ ¬ will A.

Derived from Semantics.Conditionals.SelectionFunction.sel_neg_swap — the structural origin is single-valuedness of selection: the selected world either satisfies A or it doesn't.

theorem Semantics.Modality.Selectional.will_excluded_middle {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : willSem s A f w ∨ willSem s (fun (w' : W) => ¬A w') f w

Will Excluded Middle @cite{cariani-santorio-2018}: will A ∨ will ¬A holds at every point of evaluation.

Derived from Semantics.Conditionals.SelectionFunction.sel_em — the disjunction holds because s.sel w f is a single world, on which A is either true or false. This is the selectional analogue of Conditional Excluded Middle for Stalnaker counterfactuals; both share the same structural origin in sel_em.

theorem Semantics.Modality.Selectional.unembedded_collapse {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) (hw : w ∈ f) : willSem s A f w ↔ A w

Unembedded collapse @cite{cariani-santorio-2018} eq. (17): when the evaluation world is itself in the modal parameter, Centering forces the selected world to be w, so will A reduces to A w.

This explains the apparent factivity of unembedded will-claims when the speaker presupposes that the actual world is among the historical alternatives.

§3. Content transparency

The substantive transparency claim of @cite{cariani-santorio-2018} §8.1 footnote 30: as a proposition (set of worlds), ‖will A‖ is not just ‖A‖ — they may diverge outside the modal parameter. But restricted to the modal parameter, they agree. This is the content-level fact from which the cognitive-role prediction follows.

theorem Semantics.Modality.Selectional.will_eq_A_on_modalParam {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : w ∈ f → (willSem s A f w ↔ A w)

Content transparency @cite{cariani-santorio-2018} §8.1: on the modal parameter f, the truth set of will A coincides with the truth set of A. Pointwise consequence of Centering.

theorem Semantics.Modality.Selectional.will_and_eq_will_and_will_on_modalParam {W : Type u_1} (s : Conditionals.SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : w ∈ f → (willSem s (fun (w' : W) => A w' ∧ B w') f w ↔ willSem s A f w ∧ willSem s B f w)

Conjunction transparency: on f, will (A ∧ B) and will A ∧ will B coincide pointwise.

theorem Semantics.Modality.Selectional.will_or_eq_will_or_will_on_modalParam {W : Type u_1} (s : Conditionals.SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : w ∈ f → (willSem s (fun (w' : W) => A w' ∨ B w') f w ↔ willSem s A f w ∨ willSem s B f w)

Disjunction transparency: on f, will (A ∨ B) and will A ∨ will B coincide pointwise.

theorem Semantics.Modality.Selectional.will_inter_modalParam_eq {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) : {w : W | willSem s A f w} ∩ f = {w : W | A w} ∩ f

Set-level Content Transparency @cite{cariani-santorio-2018} §8.1: as propositions (sets of worlds), ‖will_f A‖ and ‖A‖ coincide on the modal parameter f. The cognitive-role argument (paper §8.1) hinges on this set equality, not just on pointwise truth: it is the equality of truth-sets — restricted to f — that underwrites cognitive_role.

theorem Semantics.Modality.Selectional.will_and_inter_modalParam_eq {W : Type u_1} (s : Conditionals.SelectionFunction W) (A B : W → Prop) (f : Set W) : {w : W | willSem s (fun (w' : W) => A w' ∧ B w') f w} ∩ f = {w : W | willSem s A f w} ∩ {w : W | willSem s B f w} ∩ f

Conjunction transparency at the set level @cite{cariani-santorio-2018} §8.1: on f, the truth-set of will (A ∧ B) coincides with the intersection of the truth-sets of will A and will B. Equivalently: ‖will (A ∧ B)‖_f = ‖will A‖_f ∩ ‖will B‖_f. Follows from single-valuedness of selection: at each world, all three propositions are evaluated at the same point s.sel w f.

theorem Semantics.Modality.Selectional.will_or_union_modalParam_eq {W : Type u_1} (s : Conditionals.SelectionFunction W) (A B : W → Prop) (f : Set W) : {w : W | willSem s (fun (w' : W) => A w' ∨ B w') f w} ∩ f = ({w : W | willSem s A f w} ∪ {w : W | willSem s B f w}) ∩ f

Disjunction transparency at the set level @cite{cariani-santorio-2018} §8.1: on f, the truth-set of will (A ∨ B) coincides with the union of the truth-sets of will A and will B. Selectional will distributes over disjunction at the set level — a substantively stronger claim than the universal account, which over-distributes.

§4. Validity₂ (paper §6)

@cite{cariani-santorio-2018} distinguish validity₁ (truth at the context of utterance) from validity₂ (truth at every index ⟨w, s, g⟩). The matrix scopelessness theorems are validity₁ claims; the more interesting ones are validity₂.

def Semantics.Modality.Selectional.Valid2 {W : Type u_1} (φ : Conditionals.SelectionFunction W → Set W → W → Prop) : Prop

Validity₂: a propositional schema is valid₂ when it holds at every ⟨selection function, modal parameter, world⟩ triple.

Equations

• Semantics.Modality.Selectional.Valid2 φ = ∀ (s : Semantics.Conditionals.SelectionFunction W) (f : Set W) (w : W), φ s f w

@[reducible]

def Semantics.Modality.Selectional.Valid1 {W : Type u_1} (φ : Conditionals.SelectionFunction W → Set W → W → Prop) (sCtx : Conditionals.SelectionFunction W) (fCtx : Set W) (wCtx : W) : Prop

Validity₁ (paper §6): a propositional schema is valid₁ at a given context — fixed selection function sCtx, modal parameter fCtx, and world wCtx determined by the utterance — when it holds at that index.

This is the weaker of the two validity notions @cite{cariani-santorio-2018} distinguish in §6. The postsemantic indeterminacy phenomena live here: a schema can be valid₁ at every context without being valid₂.

Marked @[reducible] so it unfolds automatically at use sites: Valid1 φ sCtx fCtx wCtx is just φ sCtx fCtx wCtx, and treating it as a wrapper would force every downstream user to unfold Valid1.

Equations

• Semantics.Modality.Selectional.Valid1 φ sCtx fCtx wCtx = φ sCtx fCtx wCtx

theorem Semantics.Modality.Selectional.valid2_implies_valid1 {W : Type u_1} {φ : Conditionals.SelectionFunction W → Set W → W → Prop} (h : Valid2 φ) (sCtx : Conditionals.SelectionFunction W) (fCtx : Set W) (wCtx : W) : Valid1 φ sCtx fCtx wCtx

Validity₂ implies Validity₁ at every context (paper §6): if a schema holds at every index, it holds in particular at the contextually-determined index. The converse fails — postsemantic indeterminacy is precisely the gap between the two.

theorem Semantics.Modality.Selectional.valid2_negation_swap {W : Type u_1} (A : W → Prop) : Valid2 fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s (fun (w' : W) => ¬A w') f w ↔ ¬willSem s A f w

Negation Swap is valid₂ (paper §6).

theorem Semantics.Modality.Selectional.valid2_will_excluded_middle {W : Type u_1} (A : W → Prop) : Valid2 fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s A f w ∨ willSem s (fun (w' : W) => ¬A w') f w

Will Excluded Middle is valid₂ (paper §6, §7).

theorem Semantics.Modality.Selectional.postsemantic_will_excluded_middle {W : Type u_1} (A : W → Prop) (sCtx : Conditionals.SelectionFunction W) (fCtx : Set W) (wCtx : W) : Valid1 (fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s A f w ∨ willSem s (fun (w' : W) => ¬A w') f w) sCtx fCtx wCtx

Postsemantic Will Excluded Middle (paper §7): the disjunction will A ∨ will ¬A holds at the context of utterance, derived as a Validity₁ specialization of valid2_will_excluded_middle. The paper distinguishes Postsemantic CEM (Validity₁) from Compositional CEM (Validity₂); under a single contextually-fixed selection function, the former follows from the latter.

§5. Bridge to historical alternatives

Selectional will parameterized by the metaphysical modal base of @cite{condoravdi-2002} — the historical-alternatives substrate from Core/Modality/HistoricalAlternatives.lean.

def Semantics.Modality.Selectional.willHistorical {W : Type u_1} {Time : Type u_2} (s : Conditionals.SelectionFunction W) (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (A : W → Prop) (w : W) (t : Time) : Prop

Selectional will over historical alternatives. Evaluates the prejacent at the world selected from the metaphysical modal base at ⟨w, t⟩.

Equations

• Semantics.Modality.Selectional.willHistorical s history A w t = Semantics.Modality.Selectional.willSem s A (Core.Modality.HistoricalAlternatives.metaphysicalBase history w t) w

theorem Semantics.Modality.Selectional.willHistorical_reflexive_collapse {W : Type u_1} {Time : Type u_2} (s : Conditionals.SelectionFunction W) {history : Core.Modality.HistoricalAlternatives.WorldHistory W Time} (hRefl : history.reflexive) (A : W → Prop) (w : W) (t : Time) : willHistorical s history A w t ↔ A w

When the world-history relation is reflexive (the standard case @cite{condoravdi-2002} §4.1 condition (i)), willHistorical collapses to its prejacent: will_t A at w reduces to A w.

§6. The universal-quantifier foil

The universal-quantifier reading is what @cite{cariani-santorio-2018} argue against. Section 8.1's cognitive-role argument is decisive because the selectional account validates μ(‖will A‖) = μ(A) while the universal account collapses credence into a 0/1 step function.

def Semantics.Modality.Selectional.universalWill {W : Type u_1} (A : W → Prop) (f : Set W) (_w : W) : Prop

The universal-quantifier reading of will: true at w iff A holds at every world in the modal parameter. The world w itself is not used — universal will is index-independent.

Equations

• Semantics.Modality.Selectional.universalWill A f _w = ∀ w' ∈ f, A w'

theorem Semantics.Modality.Selectional.universal_negation_swap_fails {W : Type u_1} {A : W → Prop} {f : Set W} {w : W} (h : ∃ w₁ ∈ f, ∃ w₂ ∈ f, A w₁ ∧ ¬A w₂) : ¬(universalWill (fun (w' : W) => ¬A w') f w ↔ ¬universalWill A f w)

Negation Swap fails for universal will. When the modal parameter contains both an A-world and a ¬A-world, the universal-quantifier reading violates ¬∀ ↔ ∀¬.

Witness: ∀A is false (some w₂ ∉ A), but ∀¬A is also false (some w₁ ∈ A). So the biconditional is false ↔ true.

§7. Cognitive role (paper §8.1)

The selectional analysis predicts μ(‖will A‖_f) = μ(‖A‖_f) whenever the credence μ is supported on the modal parameter f. This matches the empirically attested gradedness of will-credences and distinguishes selectional from universal accounts.

The single cognitive_role theorem subsumes the conjunction, disjunction, and negation variants of earlier drafts: those are just this theorem applied to A ∩ B, A ∪ B, and Aᶜ — the Bool connectives are encoding set algebra.

theorem Semantics.Modality.Selectional.cognitive_role {W : Type u_1} (s : Conditionals.SelectionFunction W) (A f : Set W) (μ : PMF W) (h_supp : μ.support ⊆ f) : μ.probOfSet {w : W | s.sel w f ∈ A} = μ.probOfSet A

Cognitive role @cite{cariani-santorio-2018} §8.1: under any credence μ whose support lies within the modal parameter f, the measure of ‖will A‖ (the worlds whose selected world is in A) equals the measure of ‖A‖.

Reading: assertion of will A is licensed by ordinary, non-extreme credence in A. The universal-quantifier reading instead forces μ(‖∀ A‖) ∈ {0, 1} (collapsing into a step function on whether f ⊆ A), which is empirically wrong.

Proof: on the support, Centering forces s.sel w f = w, so the two sets agree on the support, and PMF.toOuterMeasure_apply_eq_of_inter_support_eq closes the goal.

§9. Multi-premise validity (paper §6)

@cite{cariani-santorio-2018} §6 distinguishes Validity₁ (truth at the context) from Validity₂ (truth at every index). Both notions extend to multi-premise consequence: an argument H₁, …, Hₙ ⊨ C is valid₂ when every index that satisfies all premises also satisfies the conclusion.

def Semantics.Modality.Selectional.Valid2Arg {W : Type u_1} (premises : List (Conditionals.SelectionFunction W → Set W → W → Prop)) (conclusion : Conditionals.SelectionFunction W → Set W → W → Prop) : Prop

Multi-premise validity₂: an argument premises ⊨ conclusion holds at every ⟨s, f, w⟩ — if all premises are true at the index, the conclusion is too.

Equations

• Semantics.Modality.Selectional.Valid2Arg premises conclusion = ∀ (s : Semantics.Conditionals.SelectionFunction W) (f : Set W) (w : W), (∀ φ ∈ premises, φ s f w) → conclusion s f w

@[reducible]

def Semantics.Modality.Selectional.Valid1Arg {W : Type u_1} (premises : List (Conditionals.SelectionFunction W → Set W → W → Prop)) (conclusion : Conditionals.SelectionFunction W → Set W → W → Prop) (sCtx : Conditionals.SelectionFunction W) (fCtx : Set W) (wCtx : W) : Prop

Multi-premise validity₁ at a context: at the contextually-fixed ⟨sCtx, fCtx, wCtx⟩, if all premises hold then so does the conclusion.

Equations

• Semantics.Modality.Selectional.Valid1Arg premises conclusion sCtx fCtx wCtx = ((∀ φ ∈ premises, φ sCtx fCtx wCtx) → conclusion sCtx fCtx wCtx)

theorem Semantics.Modality.Selectional.valid2Arg_implies_valid1Arg {W : Type u_1} {premises : List (Conditionals.SelectionFunction W → Set W → W → Prop)} {conclusion : Conditionals.SelectionFunction W → Set W → W → Prop} (h : Valid2Arg premises conclusion) (sCtx : Conditionals.SelectionFunction W) (fCtx : Set W) (wCtx : W) : Valid1Arg premises conclusion sCtx fCtx wCtx

Validity₂Arg implies Validity₁Arg at every context: if an argument is valid₂, it is valid₁ at the context of utterance.

theorem Semantics.Modality.Selectional.valid2_will_modus_ponens {W : Type u_1} (A B : W → Prop) : Valid2Arg [fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s A f w ↔ willSem s B f w, fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s A f w] fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => willSem s B f w

Modus ponens for selectional will is valid₂: from will A ↔ will B and will A, conclude will B. A trivial illustration of the multi-premise architecture.

§8. Would as past-tense morphological derivative of will

@cite{cariani-santorio-2018} §5.3.2

@cite{cariani-santorio-2018} §5.3.2 argues that would is not a separate modal operator but the past-tense morphological form of will. Both share the same selectional truth-condition; they differ only in the modal parameter f made available by tense — present will parameterises f to the historical alternatives at the speech time; past would parameterises f to a counterfactual base, typically supplied by an if-clause.

The shared truth-condition means every theorem about will lifts automatically to would: Negation Swap, Will Excluded Middle, the collapse-on-membership theorem, the cognitive-role prediction. This is the formal payoff of analysing would as a tense form of will rather than as an independent operator: the entire §2–§7 architecture is reused unchanged.

def Semantics.Modality.Selectional.wouldSem {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : Prop

Selectional would @cite{cariani-santorio-2018} §5.3.2: definitionally identical to willSem. The morphological past-tense distinction does not change the semantic clause; it only changes which modal parameter is supplied by context.

Equations

• Semantics.Modality.Selectional.wouldSem s A f w = Semantics.Modality.Selectional.willSem s A f w

@[simp]

theorem Semantics.Modality.Selectional.wouldSem_def {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : wouldSem s A f w ↔ A (s.sel w f)

theorem Semantics.Modality.Selectional.wouldSem_eq_willSem {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : wouldSem s A f w = willSem s A f w

Past-tense morphology = parameter shift, not semantic shift @cite{cariani-santorio-2018} §5.3.2: would and will have the same selectional truth-condition. The difference is purely in the modal parameter f supplied by the tense morpheme.

theorem Semantics.Modality.Selectional.would_excluded_middle {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : wouldSem s A f w ∨ wouldSem s (fun (w' : W) => ¬A w') f w

Would Excluded Middle, lifted from will_excluded_middle via the morphological identity.

theorem Semantics.Modality.Selectional.would_negation_swap {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : wouldSem s (fun (w' : W) => ¬A w') f w ↔ ¬wouldSem s A f w

Would Negation Swap, lifted from negation_swap.

theorem Semantics.Modality.Selectional.would_unembedded_collapse {W : Type u_1} (s : Conditionals.SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) (hw : w ∈ f) : wouldSem s A f w ↔ A w

Would-Centering / unembedded collapse for would: when w is in the modal parameter, would A collapses to A w, lifted from unembedded_collapse.

theorem Semantics.Modality.Selectional.valid2_would_excluded_middle {W : Type u_1} (A : W → Prop) : Valid2 fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => wouldSem s A f w ∨ wouldSem s (fun (w' : W) => ¬A w') f w

Would Excluded Middle is valid₂, by the same argument as valid2_will_excluded_middle.

theorem Semantics.Modality.Selectional.valid2_would_negation_swap {W : Type u_1} (A : W → Prop) : Valid2 fun (s : Conditionals.SelectionFunction W) (f : Set W) (w : W) => wouldSem s (fun (w' : W) => ¬A w') f w ↔ ¬wouldSem s A f w

Would Negation Swap is valid₂.