Stalnaker selection-function counterfactuals #
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 #
[Sta68]'s selection function approach to counterfactuals:
- A selection function
s : W × 𝒫(W) → Wselects THE closest antecedent-world - "If A were, C would be" is true iff C holds at s(w, ⦃A⦄)
Key distinction from [Lew73b]: 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
Semantics/Conditionals/SelectionFunction.lean and is shared with
[CS18]'s selectional will (Semantics/Modality/Selectional.lean)
and will-conditionals (Semantics/Conditionals/WillConditional.lean).
Selection ↔ Similarity Bridge ([Sta81]) #
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 ([Sta75]) #
[Sta75] 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 [Sta75] §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 #
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.
Instances For
Stalnakerian mood machinery #
The bare selection-conditional clause selectionConditional and its
decidability instance now live in SelectionFunction.lean — the
[Sta68] substrate shared with the counterfactual reading
(Counterfactual.stalnakerCounterfactual). This section adds the
[Sta75] indicative refinements on top of that shared clause.
Pragmatic constraint on selection ([Sta75] §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 [Sta75]: 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)
Instances For
Mooded conditional ([Sta75]): 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
Instances For
moodedConditional is decidable when its consequent is.
Equations
Mood-indexed admissibility on selection functions ([Sta75]).
Stalnaker's mood distinction lives here, not in the truth-conditional clause:
.indicativerequires the selection function to obeypragmaticConstrainton the context — the central [Sta75] contribution..subjunctiveimposes 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
Instances For
Indicative admissibility unfolds to the pragmatic constraint.
Subjunctive admissibility imposes no constraint.
Mood is irrelevant to the truth-conditional clause ([Sta75]). For any grammatical mood, the mooded conditional reduces to the bare selection conditional.
Selection conditional ≡ material within an appropriate context ([Sta75] §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:wis in the context set;h_open_p: some context-set world satisfiesp(antecedent is open);h_constraint:sobeys the pragmatic constraint relative toC;h_C_imp: in the context, the material conditional holds.
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.