Selectional will-Conditionals

[CS18]

[CS18] §5.3.1 lifts the selectional analysis of will to conditionals via Kratzerian restriction: an if-clause restricts the modal parameter f to its intersection with the antecedent's truth set. The restriction rule is paper eq. (21); eq. (20) is the LF of the example sentence and eq. (23) its informal English gloss.

⟦if A, will B⟧^{w,s,g} = ⟦will B⟧^{w,s,g[f ↦ g(f) ∩ ‖A‖]} = B (s(w, g(f) ∩ ‖A‖))

The semantic rule lives in §5.3.1; §7 then derives the predicted compositional CEM and Negation-Swap-in-Conditionals theorems as consequences of this restriction rule combined with selection single-valuedness.

What's here

• restrict: the Kratzer restriction operation f ∩ ‖A‖ shared by every will-conditional construction in this file.
• willConditional: the restrictor analysis applied to the selectional will. The if-clause intersects the modal parameter.
• compositional_CEM: if A, will B ∨ if A, will ¬B is valid₂ — Compositional CEM for will-conditionals (paper §7). Stalnaker's CEM lifted to the future-modal layer.
• narrow_negation_swap: ¬ (if A, will B) ↔ (if A, will ¬B) — the narrow-scope reading (paper §7). Negation under the if-clause swaps through will by Selectional.negation_swap.
• willConditional_collapse: when w ∈ f and A w, the conditional collapses to its consequent: will B reduces to B w.

def Semantics.Conditionals.WillConditional.restrict {W : Type u_1} (A : W → Prop) (f : Set W) : Set W

Kratzer restriction [CS18] §5.3.1: the if-clause A restricts the modal parameter f to the alternatives that also satisfy A, i.e. f ∩ ‖A‖. Every will-conditional construction in this file feeds the selection function this restricted parameter.

Equations

• Semantics.Conditionals.WillConditional.restrict A f = f ∩ {w' : W | A w'}

def Semantics.Conditionals.WillConditional.willConditional {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : Prop

Selectional will-conditional [CS18] §5.3.1: the if-clause A Kratzer-restricts the modal parameter f to f ∩ ‖A‖ before evaluating the will-prejacent B. The restriction rule is paper eq. (21); eq. (23) is its informal English gloss.

Equations

• Semantics.Conditionals.WillConditional.willConditional s A B f w = Semantics.Modality.Selectional.willSem s B (Semantics.Conditionals.WillConditional.restrict A f) w

@[simp]

theorem Semantics.Conditionals.WillConditional.willConditional_def {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : willConditional s A B f w ↔ B (s.sel w (f ∩ {w' : W | A w'}))

theorem Semantics.Conditionals.WillConditional.compositional_CEM {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : willConditional s A B f w ∨ willConditional s A (fun (w' : W) => ¬B w') f w

Compositional CEM [CS18] §7: for the selectional will-conditional, the disjunction (if A, will B) ∨ (if A, will ¬B) holds at every point.

Derived from Semantics.Conditionals.SelectionFunction.sel_em applied at the restricted parameter f ∩ ‖A‖. Will Excluded Middle and Compositional CEM share this single structural origin: the selected world is single-valued no matter which proposition restricts the modal parameter.

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

Compositional CEM is valid₂ (paper §7): holds at every ⟨s, f, w⟩ index.

theorem Semantics.Conditionals.WillConditional.narrow_negation_swap {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : willConditional s A (fun (w' : W) => ¬B w') f w ↔ ¬willConditional s A B f w

Narrow Negation Swap in Conditionals [CS18] §7: under the narrow reading where negation scopes under the if-clause, ¬ (if A, will B) ↔ (if A, will ¬B). Derived from Semantics.Conditionals.SelectionFunction.sel_neg_swap at the restricted parameter f ∩ ‖A‖; the conditional analogue of the matrix Negation Swap, lifted by restrictor-style restriction of the modal parameter.

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

Narrow Negation Swap is valid₂.

theorem Semantics.Conditionals.WillConditional.wide_negation_swap {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : ¬willConditional s A B f w ↔ willConditional s A (fun (w' : W) => ¬B w') f w

Wide Negation Swap in Conditionals [CS18] §7: under the wide reading where negation scopes over the entire conditional, ¬ (if A, will B) ↔ (if A, will ¬B). In the selectional setting this is definitionally the converse of narrow_negation_swap: selection-function single-valuedness reduces both LF positions to the same truth condition ¬ B (s.sel w (f ∩ ‖A‖)), so C&S derive Wide Negation Swap from Narrow plus the matrix Negation Swap (paper §7). The wide/narrow collapse is internal to the selectional analysis.

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

Wide Negation Swap is valid₂.

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

Postsemantic CEM for will-conditionals [CS18] §7: Compositional CEM specialized to the context of utterance — (if A, will B) ∨ (if A, will ¬B) holds at the contextually-fixed ⟨sCtx, fCtx, wCtx⟩. Under a single selection function the postsemantic and compositional readings coincide; the paper distinguishes them because the supervaluational generalization separates Validity₁ from Validity₂.

theorem Semantics.Conditionals.WillConditional.willConditional_collapse {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) (hw_f : w ∈ f) (hw_A : A w) : willConditional s A B f w ↔ B w

Conditional collapse: when the evaluation world w is in the restricted modal parameter f ∩ ‖A‖ (i.e., both in the original base and an A-world itself), the conditional collapses to its consequent B w by Centering.

theorem Semantics.Conditionals.WillConditional.willConditional_redundant {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) (h_subset : ∀ w' ∈ f, A w') : willConditional s A B f w ↔ Modality.Selectional.willSem s B f w

Restriction is idempotent under satisfaction: if f ⊆ ‖A‖, restricting by A is a no-op, so will A → will A and if A, will B ↔ will B.

The universal-base foil for will-conditionals

The Lewis-style universal-quantifier reading lifts to conditionals the same way the selectional one does — by Kratzer-restricting the modal parameter — but evaluates the prejacent universally over the restricted parameter instead of at the single selected world. This is the conditional image of [CS18]'s matrix foil Selectional.universalWill. It is the natural-language analogue of [Lew73b]'s counterfactual semantics, and it falsifies Compositional CEM: when the restricted parameter contains both a B-world and a ¬B-world, neither (if A, will B) nor (if A, will ¬B) is universally true. The concrete refutation is CarianiSantorio2018's universal_will_conditional_cem_fails, the will-conditional analogue of Stalnaker1981.bizet_cem_fails_universal.

def Semantics.Conditionals.WillConditional.universalWillConditional {W : Type u_1} (A B : W → Prop) (f : Set W) (w : W) : Prop

Universal-base will-conditional (the foil): the if-clause Kratzer-restricts the parameter to f ∩ ‖A‖, then will B is read as universal quantification over that restricted parameter. Unlike willConditional, this validates neither Compositional CEM nor Negation Swap.

Equations

• Semantics.Conditionals.WillConditional.universalWillConditional A B f w = Semantics.Modality.Selectional.universalWill B (Semantics.Conditionals.WillConditional.restrict A f) w

Would-conditionals — the past-tense morphological derivative

[CS18] §5.3.2 identifies would with the past tense form of will. The conditional analogue follows: a would- conditional is just the selectional restrictor applied to would, which by wouldSem_eq_willSem is identical to a will-conditional. The morphology shifts the modal parameter; the semantic clause is unchanged.

def Semantics.Conditionals.WillConditional.wouldConditional {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : Prop

Selectional would-conditional [CS18] §5.3.2 + §5.3.1: the would-conditional is the selectional restrictor applied to would, which by the morphological identity wouldSem = willSem collapses to willConditional.

Equations

• Semantics.Conditionals.WillConditional.wouldConditional s A B f w = Semantics.Conditionals.WillConditional.willConditional s A B f w

@[simp]

theorem Semantics.Conditionals.WillConditional.wouldConditional_eq_willConditional {W : Type u_1} (s : SelectionFunction W) (A B : W → Prop) (f : Set W) (w : W) : wouldConditional s A B f w = willConditional s A B f w

Past-tense morphology = parameter shift for conditionals: would-conditionals and will-conditionals share their semantic clause (the conditional analogue of wouldSem_eq_willSem). Tagged @[simp] so wouldConditional reduces to the canonical willConditional normal form.

Modal subordination

[CS18] §5.3.1 models modal subordination in a discourse "If A, will B. Will C." by coindexing the second sentence's will to the same restricted modal-base variable the if-clause introduces, so both wills are interpreted under the antecedent's supposition f ∩ ‖A‖ rather than the second starting fresh from f. C&S treat the coindexing as a discourse assumption (following Klecha), not as something the semantics forces. Under that coindexing the selection function picks the same world for both prejacents, because s.sel w (f ∩ ‖A‖) is single-valued — the discourse analogue of the single-valuedness behind compositional_CEM and narrow_negation_swap.

def Semantics.Conditionals.WillConditional.subordinatedWillDiscourse {W : Type u_1} (s : SelectionFunction W) (A B C : W → Prop) (f : Set W) (w : W) : Prop

Modally-subordinated will-discourse [CS18] §5.3.1: the minimal two-will instance of C&S's coindexing analysis — "If A, will B. Will C." with the second will's modal base coindexed to the if-clause's restricted parameter f ∩ ‖A‖. Holds iff both prejacents hold at the Stalnaker-selected world from the restricted parameter.

Equations

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

theorem Semantics.Conditionals.WillConditional.subordinatedWillDiscourse_eq_conj {W : Type u_1} (s : SelectionFunction W) (A B C : W → Prop) (f : Set W) (w : W) : subordinatedWillDiscourse s A B C f w ↔ B (s.sel w (f ∩ {w' : W | A w'})) ∧ C (s.sel w (f ∩ {w' : W | A w'}))

Modal subordination = shared selected world: the subordinated discourse picks the same world for both prejacents, because s.sel w (f ∩ ‖A‖) is single-valued. The discourse therefore reduces to a single conjunction B w' ∧ C w' evaluated at that world w'.

theorem Semantics.Conditionals.WillConditional.subordinated_eq_unrestricted_of_no_shift {W : Type u_1} (s : SelectionFunction W) (A B C : W → Prop) (f : Set W) (w : W) (h_no_shift : s.sel w f = s.sel w (restrict A f)) : subordinatedWillDiscourse s A B C f w ↔ willConditional s A B f w ∧ Modality.Selectional.willSem s C f w

Subordination coincides with an unrestricted continuation exactly when the if-clause does not shift the selected world. The modally-subordinated reading evaluates the continuation will C at the restricted parameter f ∩ ‖A‖, whereas a fresh, non-subordinated will C would evaluate it at f. The two readings agree precisely when restricting by A leaves the selected world fixed (s.sel w f = s.sel w (f ∩ ‖A‖)); in general they diverge.