Stalnaker 1981 @cite{stalnaker-1981}

A Defense of Conditional Excluded Middle. In Harper, Stalnaker & Pearce (eds.), Ifs, 87--104. Springer.

Core Contributions

1. CEM is valid under selection-function semantics + supervaluation
2. Uniqueness as vagueness: ties in similarity are semantic indeterminacy, handled by supervaluation rather than by abandoning uniqueness
3. Might counterfactuals: CEM + Lewis's definition of might as ¬(would ¬B) collapses might into would. Stalnaker treats might as genuine epistemic possibility, restoring the distinction via supervaluation over ties.
4. Distribution principle: (A □→ (B∨C)) ⊃ ((A □→ B) ∨ (A □→ C)) holds for selection semantics with uniqueness, fails for universal

Integration

• CEM: cem_selectional (Counterfactual.lean)
• Supervaluation bridge: selectional_as_supervaluation (Counterfactual.lean)
• Might collapse: lewis_might_eq_would_cem, lewis_might_eq_would_singleton
• Distribution: distribution_selectional, distribution_fails_universal
• This file: concrete worked examples (Bizet--Verdi, might/would, scope)

The Bizet--Verdi Example

The example originates with @cite{quine-1950}.

"If Bizet and Verdi had been compatriots, Bizet would have been Italian." "If Bizet and Verdi had been compatriots, Verdi would have been French."

On Lewis's analysis, both are false (each individual CF fails because not all closest worlds satisfy the consequent). On Stalnaker's, both are indeterminate — the selection function faces a genuine tie between the both-Italian and both-French worlds.

CEM still holds: for each conditional, the disjunction φ ∨ ¬φ is not false (it is gap ∨ gap under supervaluation). But under universal semantics CEM fails: both φ and ¬φ are false.

inductive Stalnaker1981.BVWorld : Type

Three possible worlds for the Bizet--Verdi scenario.

• actual : BVWorld
• bothItalian : BVWorld
• bothFrench : BVWorld

@[implicit_reducible]

instance Stalnaker1981.instReprBVWorld : Repr BVWorld

Equations

• Stalnaker1981.instReprBVWorld = { reprPrec := Stalnaker1981.instReprBVWorld.repr }

def Stalnaker1981.instReprBVWorld.repr : BVWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stalnaker1981.instDecidableEqBVWorld : DecidableEq BVWorld

Equations

• Stalnaker1981.instDecidableEqBVWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stalnaker1981.instFintypeBVWorld : Fintype BVWorld

Equations

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

def Stalnaker1981.bvSim : Core.Order.SimilarityOrdering BVWorld

Similarity ordering for Bizet--Verdi: actual is strictly closest to itself (centering), and bothItalian and bothFrench are equally close (mutual ≤). This models the tie that Stalnaker's supervaluation handles.

Equations

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

def Stalnaker1981.compatriots : BVWorld → Prop

The antecedent: Bizet and Verdi are compatriots.

Equations

• Stalnaker1981.compatriots Stalnaker1981.BVWorld.bothItalian = True
• Stalnaker1981.compatriots Stalnaker1981.BVWorld.bothFrench = True
• Stalnaker1981.compatriots Stalnaker1981.BVWorld.actual = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredBVWorldCompatriots : DecidablePred compatriots

Equations

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

def Stalnaker1981.bizetItalian : BVWorld → Prop

The consequent: Bizet is Italian.

Equations

• Stalnaker1981.bizetItalian Stalnaker1981.BVWorld.bothItalian = True
• Stalnaker1981.bizetItalian x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredBVWorldBizetItalian : DecidablePred bizetItalian

Equations

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

def Stalnaker1981.verdiFrench : BVWorld → Prop

The consequent: Verdi is French.

Equations

• Stalnaker1981.verdiFrench Stalnaker1981.BVWorld.bothFrench = True
• Stalnaker1981.verdiFrench x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredBVWorldVerdiFrench : DecidablePred verdiFrench

Equations

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

theorem Stalnaker1981.bizet_italian_indeterminate : Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual = Core.Duality.Truth3.indet

"If B&V had been compatriots, Bizet would have been Italian" is indeterminate: some closest compatriot-worlds make it true (.bothItalian), others false (.bothFrench).

theorem Stalnaker1981.verdi_french_indeterminate : Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots verdiFrench BVWorld.actual = Core.Duality.Truth3.indet

"If B&V had been compatriots, Verdi would have been French" is also indeterminate, for the same reason.

theorem Stalnaker1981.bizet_verdi_cem : have φ := Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual; have ψ := Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots (fun (x : BVWorld) => ¬bizetItalian x) BVWorld.actual; max φ ψ ≠ Core.Duality.Truth3.false

CEM holds for Bizet--Verdi under selectional semantics. Derived from the generic cem_selectional — concrete examples inherit from the theory rather than being independently verified.

theorem Stalnaker1981.bizet_cem_fails_universal : ¬Semantics.Conditionals.Counterfactual.universalCounterfactual bvSim compatriots bizetItalian BVWorld.actual ∧ ¬Semantics.Conditionals.Counterfactual.universalCounterfactual bvSim compatriots (fun (x : BVWorld) => ¬bizetItalian x) BVWorld.actual

CEM fails under universal semantics. Lewis's theory makes both "would B" and "would ¬B" false — so their disjunction is false. This is the central empirical divergence.

Might Counterfactuals

Lewis defines "if A, might B" as ¬(A □→ ¬B). Combined with CEM, this collapses might into would:

1. CEM: (A □→ B) ∨ (A □→ ¬B)
2. If (A □→ ¬B), then ¬(A ◇→ B) by Lewis's def, so (A ◇→ B) → (A □→ B)
3. If (A □→ B), then (A ◇→ B) since would implies might
4. Therefore: (A ◇→ B) ↔ (A □→ B)

The general collapse is proved as lewis_might_eq_would_cem in Counterfactual.lean, with lewis_might_eq_would_singleton as the special case for unique closest worlds. Here we show concrete consequences:

• In Bizet--Verdi (ties), selectional might is true while would is gap — the distinction is preserved by supervaluation
• Lewis's might is also true here (no collapse because Lewis rejects CEM), but for the wrong reason: it conflates epistemic possibility with the absence of universal counterfactual negation

theorem Stalnaker1981.selectional_might_bizet_true : Semantics.Conditionals.Counterfactual.selectionalMight bvSim compatriots bizetItalian BVWorld.actual

In the Bizet--Verdi scenario, the selectional might is true — correctly predicting that "Bizet MIGHT have been Italian" is acceptable.

theorem Stalnaker1981.selectional_might_verdi_true : Semantics.Conditionals.Counterfactual.selectionalMight bvSim compatriots verdiFrench BVWorld.actual

Selectional might is also true for the French direction.

theorem Stalnaker1981.might_would_asymmetry : Semantics.Conditionals.Counterfactual.selectionalMight bvSim compatriots bizetItalian BVWorld.actual ∧ Semantics.Conditionals.Counterfactual.selectionalMight bvSim compatriots verdiFrench BVWorld.actual ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual = Core.Duality.Truth3.indet ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots verdiFrench BVWorld.actual = Core.Duality.Truth3.indet

The might/would asymmetry under supervaluation: both might conditionals are true even though neither would conditional is determinate (both are gap). This is the correct pattern: "Bizet might have been Italian" is acceptable, "Bizet would have been Italian" is neither true nor false.

inductive Stalnaker1981.SWorld : Type

Singleton collapse: with a single closest world, Lewis's might and would give identical results. This is the concrete instance of lewis_might_eq_would_singleton.

• actual : SWorld
• closest : SWorld

@[implicit_reducible]

instance Stalnaker1981.instReprSWorld : Repr SWorld

Equations

• Stalnaker1981.instReprSWorld = { reprPrec := Stalnaker1981.instReprSWorld.repr }

def Stalnaker1981.instReprSWorld.repr : SWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stalnaker1981.instDecidableEqSWorld : DecidableEq SWorld

Equations

• Stalnaker1981.instDecidableEqSWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stalnaker1981.instFintypeSWorld : Fintype SWorld

Equations

• Stalnaker1981.instFintypeSWorld = { elems := {Stalnaker1981.SWorld.actual, Stalnaker1981.SWorld.closest}, complete := Stalnaker1981.instFintypeSWorld._proof_1 }

def Stalnaker1981.sSim : Core.Order.SimilarityOrdering SWorld

Singleton similarity: actual is strictly closest to itself (centering), and closest is the unique closest non-actual world.

Equations

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

def Stalnaker1981.sAnte : SWorld → Prop

Equations

• Stalnaker1981.sAnte Stalnaker1981.SWorld.closest = True
• Stalnaker1981.sAnte x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredSWorldSAnte : DecidablePred sAnte

Equations

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

def Stalnaker1981.sCons : SWorld → Prop

Equations

• Stalnaker1981.sCons Stalnaker1981.SWorld.closest = True
• Stalnaker1981.sCons x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredSWorldSCons : DecidablePred sCons

Equations

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

theorem Stalnaker1981.singleton_collapse : Semantics.Conditionals.Counterfactual.lewisMight sSim sAnte sCons SWorld.actual ↔ Semantics.Conditionals.Counterfactual.universalCounterfactual sSim sAnte sCons SWorld.actual

With a unique closest world, Lewis's might = would.

Distribution Principle

On Lewis's account, conditionals act like necessity operators on their consequents. The distribution principle

(A □→ (B ∨ C)) ⊃ ((A □→ B) ∨ (A □→ C))

holds for selection semantics with uniqueness (one world, B∨C ⊃ B or C) but fails for universal semantics (∀ distributes over ∧, not ∨).

theorem Stalnaker1981.distribution_fails_bizetverdi : Semantics.Conditionals.Counterfactual.universalCounterfactual bvSim compatriots (fun (w : BVWorld) => bizetItalian w ∨ verdiFrench w) BVWorld.actual ∧ ¬Semantics.Conditionals.Counterfactual.universalCounterfactual bvSim compatriots bizetItalian BVWorld.actual ∧ ¬Semantics.Conditionals.Counterfactual.universalCounterfactual bvSim compatriots verdiFrench BVWorld.actual

Under universal semantics: compatriots □→ (Italian ∨ French) is true (every compatriot-world satisfies one or the other), but NEITHER compatriots □→ Italian NOR compatriots □→ French is true. Distribution fails.

theorem Stalnaker1981.distribution_needs_uniqueness : Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots (fun (w : BVWorld) => bizetItalian w ∨ verdiFrench w) BVWorld.actual = Core.Duality.Truth3.true ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual = Core.Duality.Truth3.indet ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual bvSim compatriots verdiFrench BVWorld.actual = Core.Duality.Truth3.indet

Under selectional semantics with ties, the compound conditional (B∨C) is true (all closest worlds agree on B∨C), but the individual conditionals are indeterminate. The uniqueness premise of distribution_selectional is not met here (two closest worlds).

Conditionals and Quantifier Scope

On Lewis's analysis, conditional antecedents determine a set of possible worlds, so conditionals interact with quantifiers exactly like necessity operators. The scope distinction between (A > (∃x)Fx) and (∃x)(A > Fx) is semantically significant.

The Supreme Court dialogue:

• "He has to appoint some woman" (narrow scope: ∃ under □)
• "He doesn't have to appoint any particular woman" (no wide scope)

The same pattern arises in counterfactuals when there are ties: the selection function will pick a world where someone is appointed, but no particular woman is the one who would be appointed.

inductive Stalnaker1981.CourtWorld : Type

• actual : CourtWorld
• w1 : CourtWorld
• w2 : CourtWorld

def Stalnaker1981.instReprCourtWorld.repr : CourtWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stalnaker1981.instReprCourtWorld : Repr CourtWorld

Equations

• Stalnaker1981.instReprCourtWorld = { reprPrec := Stalnaker1981.instReprCourtWorld.repr }

@[implicit_reducible]

instance Stalnaker1981.instDecidableEqCourtWorld : DecidableEq CourtWorld

Equations

• Stalnaker1981.instDecidableEqCourtWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stalnaker1981.instFintypeCourtWorld : Fintype CourtWorld

w1 and w2 are equally close to actual (mutual ≤): the president's choice is underdetermined.

Equations

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

def Stalnaker1981.courtSim : Core.Order.SimilarityOrdering CourtWorld

Equations

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

def Stalnaker1981.vacancy : CourtWorld → Prop

The antecedent: a vacancy occurs.

Equations

• Stalnaker1981.vacancy Stalnaker1981.CourtWorld.actual = False
• Stalnaker1981.vacancy x✝ = True

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldVacancy : DecidablePred vacancy

Equations

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

def Stalnaker1981.appointA : CourtWorld → Prop

Woman A is appointed in w1.

Equations

• Stalnaker1981.appointA Stalnaker1981.CourtWorld.w1 = True
• Stalnaker1981.appointA x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldAppointA : DecidablePred appointA

Equations

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

def Stalnaker1981.appointB : CourtWorld → Prop

Woman B is appointed in w2.

Equations

• Stalnaker1981.appointB Stalnaker1981.CourtWorld.w2 = True
• Stalnaker1981.appointB x✝ = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldAppointB : DecidablePred appointB

Equations

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

def Stalnaker1981.someoneAppointed : CourtWorld → Prop

Someone is appointed (narrow scope ∃).

Equations

• Stalnaker1981.someoneAppointed Stalnaker1981.CourtWorld.w1 = True
• Stalnaker1981.someoneAppointed Stalnaker1981.CourtWorld.w2 = True
• Stalnaker1981.someoneAppointed Stalnaker1981.CourtWorld.actual = False

@[implicit_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldSomeoneAppointed : DecidablePred someoneAppointed

Equations

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

theorem Stalnaker1981.narrow_scope_true : Semantics.Conditionals.Counterfactual.universalCounterfactual courtSim vacancy someoneAppointed CourtWorld.actual

Narrow scope: "he would appoint some woman" — all closest worlds have someone appointed, so this is true even under universal semantics.

theorem Stalnaker1981.wide_scope_A_gap : Semantics.Conditionals.Counterfactual.selectionalCounterfactual courtSim vacancy appointA CourtWorld.actual = Core.Duality.Truth3.indet

Wide scope fails for each particular woman: "he would appoint woman A" is indeterminate (gap) under selectional semantics.

theorem Stalnaker1981.wide_scope_B_gap : Semantics.Conditionals.Counterfactual.selectionalCounterfactual courtSim vacancy appointB CourtWorld.actual = Core.Duality.Truth3.indet

theorem Stalnaker1981.scope_contrast : Semantics.Conditionals.Counterfactual.selectionalCounterfactual courtSim vacancy someoneAppointed CourtWorld.actual = Core.Duality.Truth3.true ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual courtSim vacancy appointA CourtWorld.actual = Core.Duality.Truth3.indet ∧ Semantics.Conditionals.Counterfactual.selectionalCounterfactual courtSim vacancy appointB CourtWorld.actual = Core.Duality.Truth3.indet

The scope contrast: narrow scope (someone appointed) is true, but wide scope for each individual is indeterminate. This illustrates Stalnaker's point that counterfactual antecedents purport to pick a unique world even when the choice is underdetermined — scope interacts with the selection function.