Counterfactual Conditionals: Three Theories #
@cite{ramotowska-marty-romoli-santorio-2025} @cite{lewis-1973}
Formalization of three competing theories of counterfactual conditionals.
The Three Theories #
Universal Theory (@cite{lewis-1973}/Kratzer): Universal quantification over closest A-worlds.
- ⦃A □→ B⦄_w = ∀w' ∈ closest(w, A). B(w')
Selectional Theory (Stalnaker): Selection function + supervaluation.
- ⦃A □→ B⦄_w = B(s(w, A)) for all legitimate selection functions s
- Indeterminate when s₁(w,A) ∈ B but s₂(w,A) ∉ B
Homogeneity Theory (von Fintel, Križ): Universal + homogeneity presupposition.
- Presupposes: all closest A-worlds agree on B
- Asserts: they all satisfy B (given the presupposition)
Key Prediction: Quantifier Embedding #
The theories diverge when counterfactuals are embedded under quantifiers in mixed scenarios:
- Selectional: quantifier STRENGTH determines truth values (QUD-independent)
- Homogeneity: QUD × polarity interaction
- Universal: all individual CFs false → strength-independent
Universal Theory #
@cite{ramotowska-marty-romoli-santorio-2025}
The standard possible-worlds analysis: counterfactuals universally quantify over the closest antecedent-worlds.
"If A were, B would" is true at w iff every closest A-world satisfies B.
This predicts:
- "Every student would pass if they studied" is FALSE if even ONE closest study-world for some student doesn't have them passing
Universal counterfactual semantics (@cite{lewis-1973}/Kratzer).
True at w iff all closest A-worlds satisfy B.
Equations
- Semantics.Conditionals.Counterfactual.universalCounterfactual sim A B w = ∀ w' ∈ sim.closestWorlds w (Finset.filter A Finset.univ), B w'
Instances For
Selectional Theory #
Stalnaker's approach with supervaluation over ties:
- A selection function picks THE closest antecedent-world
- When multiple worlds are equally close (ties), supervaluate over all choices
Three-valued semantics:
- True: B holds at s(w, A) for all legitimate selection functions s
- False: B fails at s(w, A) for all legitimate selection functions s
- Indeterminate: B holds for some s but not others
This predicts:
- "Every student would pass if they studied" is INDETERMINATE when some students' closest study-worlds have passing, others don't
Selectional counterfactual semantics (Stalnaker + supervaluation).
Returns a three-valued truth value based on agreement across selection functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
selectionalCounterfactual IS Fine super-truth (Core.Duality.dist)
on the Finset of closest worlds with the consequent as Boolean predicate.
Bridge documenting the equivalence — keeps the bespoke 3-way if-chain body for proof-script compatibility (cem_selectional and many Stalnaker1981 consumers case-split on the structure) while making the canonical-classifier connection explicit.
Conditional Excluded Middle (CEM) holds for selectional semantics.
(A □→ B) ∨ (A □→ ¬B) is always true or gap, never false.
Proof sketch:
- Empty closest: both vacuously true → or = true
- All B: φ = true → or = true
- All ¬B: ψ = true → or = true
- Mixed: both gap → or = gap
Homogeneity Theory #
Universal quantification PLUS a homogeneity presupposition:
- Presupposes: all closest A-worlds agree on B (all true or all false)
- Asserts: they all satisfy B (given the presupposition)
When the presupposition fails (mixed closest worlds), the sentence is neither true nor false (presupposition failure).
This predicts:
- "Every student would pass if they studied" has PRESUPPOSITION FAILURE when students' closest study-worlds are mixed on passing
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Semantics.Conditionals.Counterfactual.instDecidableEqPresupStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Result of evaluating a sentence with presuppositions.
- presupposition : PresupStatus
- assertion : Option Bool
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Homogeneity counterfactual semantics.
Presupposes that all closest A-worlds agree on B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Presupposition Preservation for homogeneity semantics.
If the presupposition is satisfied for (A □→ B), it's also satisfied for (A □→ ¬B). This is because homogeneity for B (all true or all false) implies homogeneity for ¬B.
Negation Swap holds for homogeneity semantics in the non-vacuous case.
When closest worlds are non-empty and presupposition is satisfied: assertion(A □→ B).map (¬·) = assertion(A □→ ¬B)
Grounding Selection Functions in Causal Models #
The selection function s(w, A) can be grounded via causal intervention:
s(w, A) = the world that results from intervening to make A true at w
This connects to @cite{nadathur-lauer-2020}: developDet M (s.extend A true)
gives the counterfactual A-world (or, Pearl-style, (M.intervene A true).developDet s).
Counterfactual dependence (necessity) corresponds to selection-based conditionals.
The intervention-based counterfactual primitive lives in
Core/Causal/V2/SEM/Counterfactual.lean as causallySufficient (which
is exactly "extending with antecedent then developing produces consequent").
The full formalization of @cite{lewis-1973-causation}'s causal dependence
appears as a paper-replication study under Phenomena/Causation/Studies/Lewis1973.lean.
The selectional counterfactual is literally supervaluation (@cite{fine-1975}) over closest worlds. Each closest world is a specification point — a legitimate resolution of the selection-function tie. When all closest worlds agree on B, the counterfactual is definite; when they disagree, it is indefinite.
Now that both `selectionalCounterfactual` and `superTrue` use `Finset`,
the connection is immediate — they are the same `∀/∃` structure over
the same finite set.
Selectional counterfactual = supervaluation over closest worlds.
When the closest-worlds set is non-empty, the selectional semantics
equals superTrue B over the closest worlds as a specification space.
This makes explicit that Stalnaker's "supervaluate over ties" IS
Fine's supervaluation with Spec = W and admissible = closest(w, A).
Now that superTrue takes Prop-valued evaluators directly (post
Bool→Prop substrate migration), the bridge is Iff.rfl-thin on the
underlying ∀ / ∃ checks.
Connection to Aggregation Pushforward #
projectTruthValues delegates directly to Core.Duality.aggregate, so
embeddedSelectional_determinate and strength_determines_pattern (in
QuantifierEmbedding.lean) are thin wrappers around
Duality.aggregate_map_ofBool_ne_indet and Duality.aggregate_map_ofBool_mixed
respectively.
The companion fact aggregate_replicate_indet (also in Duality.lean)
captures the homogeneity theory's architecture: when all inputs are
gaps, both existential and universal aggregation return gap — strength
is invisible.
The selectional theory's strength-effect prediction is an instance of the global aggregation pattern: mixed Bool inputs split duality types.
Might Counterfactuals #
@cite{stalnaker-1981}
The Lewis–Stalnaker debate turns on the analysis of might counterfactuals.
Lewis's definition: "if A, might B" =_df ¬(A □→ ¬B). On this view,
might is an idiom — the negation of the corresponding would not.
Stalnaker's objection: Under CEM, Lewis's definition makes "if A,
might B" equivalent to "if A, would B" — collapsing the might/would
distinction. Stalnaker treats might as a genuine possibility operator
that takes scope over the conditional: ◇(A □→ B).
The three-valued selectional semantics naturally distinguishes them:
would: TRUE iff all closest A-worlds satisfy Bmight: TRUE iff some closest A-world satisfies B (= NOT all satisfy ¬B)
Lewis's might counterfactual: ¬(A □→ ¬B).
Defined as the negation of the universal counterfactual with negated consequent: "it is not the case that if A were, B would not be."
Equations
- Semantics.Conditionals.Counterfactual.lewisMight sim A B w = ¬Semantics.Conditionals.Counterfactual.universalCounterfactual sim A (fun (x : W) => ¬B x) w
Instances For
Equations
Selectional might counterfactual: true on at least one
precisification.
"If A, might B" is true iff the selectional counterfactual is not
determinately false — i.e., at least one legitimate selection function
picks a B-world. This is the existential dual of the universal would.
Derived from selectionalCounterfactual rather than inlining
closestWorlds, making the supervaluation connection structural.
Equations
Instances For
CEM collapses Lewis's might into would.
When the closest-worlds set is a singleton (uniqueness holds), Lewis's
might = ¬(all closest satisfy ¬B) = some closest satisfies B =
all closest satisfy B = would. The uniqueness assumption makes
¬∀¬ equivalent to ∀.
This is the problematic consequence that @cite{stalnaker-1981} argues against: "if A, might B" should be weaker than "if A, would B", but under uniqueness they collapse.
CEM implies Lewis's might = would (the general collapse).
@cite{stalnaker-1981}'s central observation: if CEM holds for the
universal theory at a world (which it does whenever closest worlds
are a singleton, but also in other cases), then Lewis's definition
of might as ¬(would ¬B) collapses into would.
Selectional might is genuinely weaker than would.
There exist worlds where might B holds but would B does not:
when the closest-worlds set is mixed (some satisfy B, some don't),
the existential might is true but the universal would is indeterminate.
Distribution Principle #
@cite{stalnaker-1981}
On Lewis's analysis, conditional antecedents act like necessity operators, quantifying universally over closest A-worlds. The distribution principle
(A □→ (B ∨ C)) ⊃ ((A □→ B) ∨ (A □→ C))
fails for universal semantics (∀ distributes over ∧ but not ∨) but holds trivially for selectional semantics (one world, so B∨C at that world means B or C at that world).
Distribution holds for selectional semantics.
If the selected A-world satisfies B ∨ C, then either it satisfies B (so A □→ B) or it satisfies C (so A □→ C).
Distribution fails for universal semantics.
Counterexample: two closest A-worlds, one satisfying B (not C), the other satisfying C (not B). Then A □→ (B∨C) is true (both satisfy B∨C) but neither A □→ B nor A □→ C is true.
Single-Selection-Function Variant #
@cite{stalnaker-1968}
Stalnaker's original counterfactual analysis used a single Stalnakerian
selection function — picking THE closest A-world — without supervaluation
over ties. This is the same Semantics.Conditionals.SelectionFunction infrastructure that
@cite{cariani-santorio-2018} reuse for will (see
Theories/Semantics/Modality/Selectional.lean); the mechanism is identical,
only the temporal/modal target differs.
The supervaluation variant (selectionalCounterfactual above) generalises
this to handle ties: each "legitimate" selection function corresponds to a
choice point, and we supervaluate over them. The bridge below shows that
when the supervaluation's closest-worlds set is the singleton chosen by a
selection function, the supervaluation analysis (Truth3) reduces to the
single-function analysis (Bool) under Truth3.ofBool.
Stalnaker's single-selection-function counterfactual @cite{stalnaker-1968}.
A □→ B is true at w iff B holds at s(w, ‖A‖). This reuses the
same Semantics.Conditionals.SelectionFunction infrastructure that @cite{cariani-santorio-2018}
apply to will — the mechanism is identical across the two papers.
Equations
- Semantics.Conditionals.Counterfactual.stalnakerCounterfactual s A B w = B (s.sel w {w' : W | A w'})
Instances For
Bridge: Stalnaker = supervaluation when closest is a singleton.
When the supervaluation's closest-worlds set is the singleton
{s.sel w ‖A‖}, the supervaluation analysis (Truth3) reduces
to the single-selection-function analysis (Bool) under
Truth3.ofBool. The supervaluation gap arises only with ties; once
ties are resolved by the selection function, both analyses coincide.
Bridge: Stalnaker counterfactual = will-conditional over the universe #
@cite{cariani-santorio-2018} §5.3.2 + §5.3.1 unify will, would,
will-conditionals, and Stalnaker counterfactuals under a single
Semantics.Conditionals.SelectionFunction substrate. Each operator differs only in its
modal parameter f:
willSem s A f w— bare will with parameterfwillConditional s A B f w— will with parameterf ∩ ‖A‖stalnakerCounterfactual s A B w— would with parameter‖A‖, i.e. the unrestricted parameter is the whole universe
The bridge below makes this explicit: a Stalnaker counterfactual is
exactly a will-conditional whose ambient parameter is Set.univ. The
if-clause then restricts the universe down to the antecedent's truth
set, recovering Stalnaker's s(w, ‖A‖).
Stalnaker counterfactual = will-conditional over the universe.
@cite{cariani-santorio-2018} §5.3.2 + §5.3.1: when the modal parameter
of the will-conditional is taken to be Set.univ, the Kratzer
restriction Set.univ ∩ ‖A‖ = ‖A‖ recovers Stalnaker's selection
target. The Bool-valued stalnakerCounterfactual and the Prop-valued
willConditional thus coincide modulo the · = true reflection.
This is the formal payoff of the unification: bare will (willSem),
will-conditionals (willConditional), Stalnaker counterfactuals, and
would-conditionals (wouldConditional) all derive from one
Semantics.Conditionals.SelectionFunction mechanism, differing only in which modal
parameter the tense morphology supplies.
Stalnaker counterfactual = would-conditional over the universe.
The same identity restated in would-conditional terms, exercising
the morphological identity wouldConditional = willConditional. The
counterfactual is, on the C&S analysis, a past-tense (would-) form,
so the would-conditional reading is the more natural surface gloss.
Truth3 ↔ would-conditional bridge @cite{cariani-santorio-2018}
§5.3.1 + §5.3.2: composing stalnaker_eq_selectional_singleton
(Truth3 ↔ Bool stalnakerCounterfactual under singleton-closest) with
stalnakerCounterfactual_eq_wouldConditional_universe (Bool ↔ Prop
would-conditional under universe parameter) gives a direct bridge
from the supervaluation-valued selectionalCounterfactual to the
Prop-valued would-conditional of WillConditional.
Under the same h_singleton hypothesis that resolves the Truth3
gap (the closest-worlds set is exactly Stalnaker's selected world),
the supervaluation analysis lands at .true iff the would-conditional
holds. The two layers — Truth3 supervaluation over Finset and Prop
selection-function over Set — collapse to the same content.
Stalnaker–Lewis would divergence @cite{cariani-santorio-2018}
§5.3.2 motivation: there exist a world model, a selection function,
a similarity ordering, an antecedent A and a consequent B such
that the Stalnakerian would (single-selection-function reading)
is true while the Lewisian would (universal over closest
A-worlds) is false.
Construction: three worlds with everyone equally close (closer ≡
true), antecedent A = {1, 2}, consequent B = {1}. Lewis's
closestWorlds for A is the whole of A = {1, 2}, and the
universal ∀ w ∈ {1, 2}. B w fails at w = 2. Stalnaker's
selection (divergeSel) picks 1, where B holds. The same
structural source — single-valuedness of selection vs. universal
quantification over a non-trivial closest set — drives the C&S
will / universalWill split in
Semantics.Modality.Selectional.