Stalnaker selection-function counterfactuals

@cite{stalnaker-1968} @cite{stalnaker-1975} @cite{stalnaker-1981}

Selection-function-based counterfactual semantics, separated from Conditionals/Basic.lean (which retains material/strict/variably-strict

• counterexamples). All Stalnaker-flavoured machinery — pragmatic constraint, mooded conditional, indicative-vs-subjunctive admissibility, the selection ↔ similarity bridge, and the contextually-mediated material-conditional reduction — lives here.

Selection Functions

@cite{stalnaker-1968}'s selection function approach to counterfactuals:

• A selection function s : W × 𝒫(W) → W selects THE closest antecedent-world
• "If A were, C would be" is true iff C holds at s(w, ⦃A⦄)

Key distinction from @cite{lewis-1973}: Lewis universally quantifies over closest A-worlds; Stalnaker selects a single A-world (with supervaluation for ties — see Conditionals/Counterfactual.lean).

SelectionFunction itself lives in Core/SelectionFunction.lean and is shared with @cite{cariani-santorio-2018}'s selectional will in WillConditional.lean.

Selection ↔ Similarity Bridge (@cite{stalnaker-1981})

A selection function s determines a pairwise preference: w₁ ≤_{w₀} w₂ iff s(w₀, {w₁, w₂}) = w₁. This is reflexive (by success) and total (by definition); transitivity requires s.isCoherent — rationalizability by a total preorder. The coherentSelectionToSimilarity constructor turns a coherent s into a Core.Order.SimilarityOrdering.

Stalnakerian indicative/subjunctive split (@cite{stalnaker-1975})

@cite{stalnaker-1975} argues that the indicative/subjunctive distinction is pragmatic, not semantic: both have the same selection-based truth condition. Indicatives require the selection function to obey the pragmatic constraint (stay inside the context set when possible); subjunctives signal that the constraint is suspended.

The previous identification indicativeConditional := materialImp was inaccurate per @cite{stalnaker-1975} §IV. We now derive the equivalence within an appropriate context (the *_eq_material_within_context theorems below) rather than stipulate it.

Coherent selection ⇒ similarity ordering

def Semantics.Conditionals.coherentSelectionToSimilarity {W : Type u_1} [DecidableEq W] (s : SelectionFunction W) (h_coherent : s.isCoherent) : Core.Order.SimilarityOrdering W

Coherent selection functions induce similarity orderings.

Given a coherent selection function, its pairwise preference relation is a valid SimilarityOrdering: reflexive (from success) and transitive (from coherence).

Equations

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

Selection conditional + Stalnakerian mood machinery

def Semantics.Conditionals.selectionConditional {W : Type u_1} (s : SelectionFunction W) (p q : W → Prop) : W → Prop

Selection-based conditional: "if p, then q" is true at w iff q holds at the world selected by s from the p-worlds. The common semantic core of @cite{stalnaker-1975} indicatives and subjunctives.

Equations

• Semantics.Conditionals.selectionConditional s p q w = q (s.sel w {w' : W | p w'})

@[implicit_reducible]

instance Semantics.Conditionals.selectionConditional_decidable {W : Type u_1} (s : SelectionFunction W) (p q : W → Prop) [DecidablePred q] (w : W) : Decidable (selectionConditional s p q w)

selectionConditional is decidable when its consequent is.

Equations

• Semantics.Conditionals.selectionConditional_decidable s p q w = Semantics.Conditionals.selectionConditional_decidable._aux_1 s p q w

def Semantics.Conditionals.pragmaticConstraint {W : Type u_1} (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) : Prop

Pragmatic constraint on selection (@cite{stalnaker-1975} §III).

If the conditional is being evaluated at a context-set world w, and some antecedent-world is also in the context set, then the selected world must be in the context set. Equivalently: context-set worlds are closer to each other than to non-context-set worlds whenever a context-set option is available.

The central new contribution of @cite{stalnaker-1975}: it makes indicative inference forms behave the way they do, without changing the semantic clause.

Equations

• Semantics.Conditionals.pragmaticConstraint s C = ∀ (w : W) (A : Set W), C w → (∃ w' ∈ A, C w') → C (s.sel w A)

def Semantics.Conditionals.moodedConditional {W : Type u_1} (_m : Core.Mood.GramMood) (s : SelectionFunction W) (p q : W → Prop) : W → Prop

Mooded conditional (@cite{stalnaker-1975}): the truth-conditional clause is selectionConditional regardless of grammatical mood. The mood index m is metadata at the call site; the semantic mood difference is captured by which selection functions are admissible (see admissibleSelection).

Single source of truth: indicative and subjunctive conditionals do not have distinct semantic clauses.

Equations

• Semantics.Conditionals.moodedConditional _m s p q = Semantics.Conditionals.selectionConditional s p q

@[implicit_reducible]

instance Semantics.Conditionals.moodedConditional_decidable {W : Type u_1} (m : Core.Mood.GramMood) (s : SelectionFunction W) (p q : W → Prop) [DecidablePred q] (w : W) : Decidable (moodedConditional m s p q w)

moodedConditional is decidable when its consequent is.

Equations

• Semantics.Conditionals.moodedConditional_decidable m s p q w = Semantics.Conditionals.moodedConditional_decidable._aux_1 m s p q w

def Semantics.Conditionals.Mood.admissibleSelection {W : Type u_1} (m : Core.Mood.GramMood) (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) : Prop

Mood-indexed admissibility on selection functions (@cite{stalnaker-1975}).

Stalnaker's mood distinction lives here, not in the truth-conditional clause:

• .indicative requires the selection function to obey pragmaticConstraint on the context — the central @cite{stalnaker-1975} contribution.
• .subjunctive imposes no such constraint; the selection function may reach outside the context set, which is precisely what subjunctive mood signals.

This makes "indicative vs subjunctive" a property of the selection-function / context pairing, not a separate semantic operator.

Equations

• Semantics.Conditionals.Mood.admissibleSelection Core.Mood.GramMood.indicative s C = Semantics.Conditionals.pragmaticConstraint s C
• Semantics.Conditionals.Mood.admissibleSelection Core.Mood.GramMood.subjunctive s C = True

theorem Semantics.Conditionals.admissibleSelection_indicative {W : Type u_1} (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) : Mood.admissibleSelection Core.Mood.GramMood.indicative s C = pragmaticConstraint s C

Indicative admissibility unfolds to the pragmatic constraint.

theorem Semantics.Conditionals.admissibleSelection_subjunctive {W : Type u_1} (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) : Mood.admissibleSelection Core.Mood.GramMood.subjunctive s C = True

Subjunctive admissibility imposes no constraint.

theorem Semantics.Conditionals.moodedConditional_eq_selectionConditional {W : Type u_1} (m : Core.Mood.GramMood) (s : SelectionFunction W) (p q : W → Prop) : moodedConditional m s p q = selectionConditional s p q

Mood is irrelevant to the truth-conditional clause (@cite{stalnaker-1975}). For any grammatical mood, the mooded conditional reduces to the bare selection conditional.

theorem Semantics.Conditionals.selectionConditional_eq_material_within_context {W : Type u_1} (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) (p q : W → Prop) (w : W) (hC_w : C w) (h_open_p : ∃ w' ∈ {w' : W | p w'}, C w') (h_constraint : pragmaticConstraint s C) (h_C_imp : ∀ (w' : W), C w' → p w' → q w') : selectionConditional s p q w

Selection conditional ≡ material within an appropriate context (@cite{stalnaker-1975} §IV).

In any context C evaluated at a context-set world w, given that the antecedent is open in C, the selection function obeys the pragmatic constraint, and the material conditional holds throughout C, the selection conditional is true. The contextually-mediated equivalence Stalnaker defends in place of the semantic identification.

Specialised to .indicative mood, this is the Stalnakerian claim that indicative conditionals reduce to the material conditional within an appropriate context.

Hypotheses encode the "appropriate context" conditions:

• hC_w: w is in the context set;
• h_open_p: some context-set world satisfies p (antecedent is open);
• h_constraint: s obeys the pragmatic constraint relative to C;
• h_C_imp: in the context, the material conditional holds.

theorem Semantics.Conditionals.moodedConditional_indicative_eq_material_within_context {W : Type u_1} (s : SelectionFunction W) (C : Core.CommonGround.ContextSet W) (p q : W → Prop) (w : W) (hC_w : C w) (h_open_p : ∃ w' ∈ {w' : W | p w'}, C w') (h_admissible : Mood.admissibleSelection Core.Mood.GramMood.indicative s C) (h_C_imp : ∀ (w' : W), C w' → p w' → q w') : moodedConditional Core.Mood.GramMood.indicative s p q w

Indicative-mood specialisation: when the mood is indicative and the selection function is admissible, the mooded conditional reduces to the material conditional within the context.