Counterfactual conditionals: three theories

This file defines three theories of counterfactuals, all stated over the closest antecedent-worlds of a similarity ordering. On the universal theory of Lewis and Kratzer if p, would q is true when every closest p-world is a q-world. On the selectional theory of Stalnaker a selection function picks one closest p-world and ties are resolved by supervaluation over the completions of the ordering, so the counterfactual is true when every closest p-world is a q-world, false when none is, and indeterminate otherwise. On the homogeneity theory of von Fintel and Križ the universal assertion carries the presupposition that the closest p-worlds agree on q. The three agree whenever the closest antecedent-worlds agree on the consequent, and part under embedding.

Main definitions

• selectionalCounterfactual: the selectional counterfactual, super-truth over the closest antecedent-worlds.
• superCounterfactual: Stalnaker's supervaluation over completions.
• homogeneityCounterfactual: the homogeneity counterfactual, a trivalent proposition.
• selectionalMight: the selectional might.

Main results

• homogeneityCounterfactual_eq_selectionalCounterfactual: unembedded, the homogeneity counterfactual is the selectional one.
• superCounterfactual_eq_selectionalCounterfactual: on a finite, strongly centered ordering the supervaluation over completions is the selectional counterfactual.

References

• S. Ramotowska, P. Marty, J. Romoli and P. Santorio, Counterfactuals and quantificational force: Experimental evidence for selectional semantics (2025)
• D. Lewis, Counterfactuals (1973)
• A. Kratzer, Modals and Conditionals (2012)
• R. C. Stalnaker, A Theory of Conditionals (1968)
• R. C. Stalnaker, A Defense of Conditional Excluded Middle (1981)
• K. von Fintel, Bare Plurals, Bare Conditionals, and Only (1997)
• M. Križ, Aspects of Homogeneity in the Semantics of Natural Language (2015)

The homogeneity theory

The homogeneity counterfactual is a trivalent proposition. Unembedded it is the selectional counterfactual, and the two theories part only under embedding, where [RMRS25] test them.

noncomputable def Conditional.homogeneityCounterfactual {W : Type u_1} (ord : W → Preorder W) (p q : Set W) : W → SignType

The homogeneity counterfactual, which asserts that every closest p-world is a q-world and presupposes that the closest p-worlds agree on q.

Equations

• Conditional.homogeneityCounterfactual ord p q = (Conditional.closestImp ord p q ∪ Conditional.closestImp ord p qᶜ).indicator fun (v : W) => SignType.ofProp (v ∈ Conditional.closestImp ord p q)

@[simp]

theorem Conditional.homogeneityCounterfactual_eq_one_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} : homogeneityCounterfactual ord p q w = 1 ↔ w ∈ closestImp ord p q

@[simp]

theorem Conditional.homogeneityCounterfactual_eq_neg_one_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} : homogeneityCounterfactual ord p q w = -1 ↔ w ∉ closestImp ord p q ∧ w ∈ closestImp ord p qᶜ

@[simp]

theorem Conditional.homogeneityCounterfactual_eq_zero_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} : homogeneityCounterfactual ord p q w = 0 ↔ w ∉ closestImp ord p q ∧ w ∉ closestImp ord p qᶜ

theorem Conditional.support_homogeneityCounterfactual_compl {W : Type u_1} {ord : W → Preorder W} {p q : Set W} : Function.support (homogeneityCounterfactual ord p qᶜ) = Function.support (homogeneityCounterfactual ord p q)

The presupposition is symmetric in the consequent and its negation.

theorem Conditional.homogeneityCounterfactual_compl {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} (h : ((ord w).minimals p).Nonempty) : homogeneityCounterfactual ord p qᶜ w = -homogeneityCounterfactual ord p q w

With closest antecedent-worlds, negating the consequent negates the verdict.

The selectional theory

The selectional counterfactual is super-truth over the closest antecedent-worlds, each of them one resolution of the selection function's tie.

def Conditional.selectionalCounterfactual {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : SignType

The selectional counterfactual, true when every closest p-world is a q-world, false when every one is a qᶜ-world, and indeterminate otherwise.

Equations

• Conditional.selectionalCounterfactual ord p q w = SignType.supervaluation ((ord w).minimals p).toFinset fun (x : W) => x ∈ q

theorem Conditional.selectionalCounterfactual_eq_one_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : selectionalCounterfactual ord p q w = 1 ↔ w ∈ closestImp ord p q

theorem Conditional.selectionalCounterfactual_eq_neg_one_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : selectionalCounterfactual ord p q w = -1 ↔ w ∉ closestImp ord p q ∧ w ∈ closestImp ord p qᶜ

theorem Conditional.selectionalCounterfactual_eq_zero_iff {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : selectionalCounterfactual ord p q w = 0 ↔ w ∉ closestImp ord p q ∧ w ∉ closestImp ord p qᶜ

theorem Conditional.selectionalCounterfactual_compl {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] (h : ((ord w).minimals p).Nonempty) : selectionalCounterfactual ord p qᶜ w = -selectionalCounterfactual ord p q w

With closest antecedent-worlds, negating the consequent negates the verdict.

theorem Conditional.cem_selectional {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : max (selectionalCounterfactual ord p q w) (selectionalCounterfactual ord p qᶜ w) ≠ -1

The selectional disjunction of if p, q and if p, not q is never false.

theorem Conditional.homogeneityCounterfactual_eq_selectionalCounterfactual {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : homogeneityCounterfactual ord p q w = selectionalCounterfactual ord p q w

Unembedded, the homogeneity counterfactual is the selectional counterfactual.

Might counterfactuals

[Lew73b] defines if p, might q as not (if p, would not q). Together with Conditional Excluded Middle that definition makes might equivalent to would, which Lewis counts against a semantics validating it. [Sta81] rejects the definition instead, reading might as a possibility operator over the whole conditional.

def Conditional.selectionalMight {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : Prop

The selectional might holds when the selectional counterfactual is not false.

Equations

• Conditional.selectionalMight ord p q w = (Conditional.selectionalCounterfactual ord p q w ≠ -1)

@[instance_reducible]

instance Conditional.instDecidableSelectionalMight {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] : Decidable (selectionalMight ord p q w)

Equations

• Conditional.instDecidableSelectionalMight ord p q w = { decide := !decide (Conditional.selectionalCounterfactual ord p q w = -1), reflects_decide := ⋯ }

theorem Conditional.selectional_might_weaker : ∃ (ord : Fin 3 → Preorder (Fin 3)) (x : (w : Fin 3) → DecidableRel LE.le) (p : Set (Fin 3)) (q : Set (Fin 3)) (x_1 : DecidablePred fun (x : Fin 3) => x ∈ p) (x_2 : DecidablePred fun (x : Fin 3) => x ∈ q) (w : Fin 3), selectionalMight ord p q w ∧ selectionalCounterfactual ord p q w = 0

The selectional might is weaker than would, since with mixed closest worlds might holds while would is indeterminate.

Distribution

Distribution of a counterfactual over a disjunctive consequent fails for the universal theory, which quantifies over every closest world, and holds for the selectional theory when there is at most one closest world ([Sta81]).

theorem Conditional.distribution_selectional {W : Type u_1} (ord : W → Preorder W) (p q r : Set W) (w : W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] [DecidablePred fun (x : W) => x ∈ r] (h_unique : ((ord w).minimals p).Subsingleton) (h : selectionalCounterfactual ord p (q ∪ r) w = 1) : selectionalCounterfactual ord p q w = 1 ∨ selectionalCounterfactual ord p r w = 1

With at most one closest world, the selectional counterfactual distributes over a disjunctive consequent.

theorem Conditional.distribution_fails_universal : ∃ (ord : Fin 3 → Preorder (Fin 3)) (p : Set (Fin 3)) (q : Set (Fin 3)) (r : Set (Fin 3)), ∃ w ∈ closestImp ord p (q ∪ r), w ∉ closestImp ord p q ∧ w ∉ closestImp ord p r

The conditional of the closest worlds does not distribute over a disjunctive consequent when one closest world is a q-world and another an r-world.

The selectional theory as supervaluation

[Sta81] supervaluates the [Sta68] selection conditional over the completions of a similarity ordering. A conditional is true when every completion makes it true, false when every one makes it false, and indeterminate otherwise (superCounterfactual), which for a single conditional on a finite, strongly centered ordering is the selectional counterfactual.

noncomputable def Conditional.superCounterfactual {W : Type u_1} (ord : W → Preorder W) (p q : Set W) (w : W) : SignType

The supervaluation of the selection conditional over the completions of a family of preorders, true when every compatible selection function makes if p, q true, false when every one makes it false, and indeterminate otherwise.

Equations

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

theorem Conditional.selectionalCounterfactual_eq_one_iff_forall_compatible {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] (hc : IsCentered ord) : selectionalCounterfactual ord p q w = 1 ↔ ∀ (s : SelectionFunction W), s.Compatible ord → w ∈ selectionConditional s p q

The selectional counterfactual is true iff the selection conditional is true on every completion.

theorem Conditional.selectionalCounterfactual_eq_neg_one_iff_forall_compatible {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] (hc : IsCentered ord) : selectionalCounterfactual ord p q w = -1 ↔ ∀ (s : SelectionFunction W), s.Compatible ord → w ∉ selectionConditional s p q

The selectional counterfactual is false iff the selection conditional is false on every completion.

theorem Conditional.superCounterfactual_eq_selectionalCounterfactual {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] (hc : IsCentered ord) : superCounterfactual ord p q w = selectionalCounterfactual ord p q w

On a finite, strongly centered family of preorders the supervaluation over completions is the selectional counterfactual.

theorem Conditional.selectionalCounterfactual_eq_ofProp {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] {s : SelectionFunction W} (hs : s.Compatible ord) (hu : ((ord w).minimals p).Subsingleton) (hp : p.Nonempty) : selectionalCounterfactual ord p q w = SignType.ofProp (s.sel w p ∈ q)

Under the uniqueness assumption of [Sta81], at most one closest antecedent-world, any compatible selection function decides the selectional counterfactual.

Ties

theorem Conditional.stalnaker_lewis_would_diverge : ∃ (ord : Fin 3 → Preorder (Fin 3)) (s : SelectionFunction (Fin 3)), IsCentered ord ∧ s.Compatible ord ∧ 0 ∈ selectionConditional s {1, 2} {1} ∧ 0 ∉ closestImp ord {1, 2} {1}

With two antecedent-worlds tied for closest, a compatible selection function makes if p, q true while the conditional of the closest worlds does not ([Lew73b], [Sta81]).