Stalnaker (1981): A Defense of Conditional Excluded Middle

This file formalizes Stalnaker's defense of the selection-function analysis of conditionals against Lewis's comparative-similarity analysis. The two differ by the limit assumption, that every possible antecedent has closest worlds, and the uniqueness assumption, that it has at most one; in the logic of conditionals the first is the consequence condition and the second is conditional excluded middle, which is equivalent to the distribution of a conditional over a disjunctive consequent (cem_iff_distribution). Uniqueness is neutralized by supervaluation: the selection functions in use correspond to orderings with ties, and a conditional is true when every completion makes it true (superCounterfactual), so conditional excluded middle stays valid while Quine's two counterfactuals about Bizet and Verdi come out neither true nor false rather than, as for Lewis, both false (bizet_italian_indet, bizet_verdi_cem, bizet_cem_fails_universal); distribution likewise separates the analyses (distribution_needs_uniqueness, distribution_fails_bizetverdi). Because Lewis's antecedents are necessity operators, his analysis predicts a scope ambiguity between a quantifier inside and outside a counterfactual, as with the woman President Carter would have appointed to the Supreme Court; selection predicts none, the two scopes coinciding (selection_scope), and indeterminacy rather than ambiguity explains why no particular woman would have been appointed (court_no_particular_woman).

The limit assumption cannot be neutralized in the same way, and dropping it has bizarre consequences: for Lewis's line a little less than an inch long, his analysis makes if the line had been more than one inch long, it would not have been x inches long true for every length x, so that there is no length the line might have had, and the consequence condition fails. Nothing turns on lengths: the same holds of any antecedent without closest worlds (lewisWould_ne, not_lewisMight_eq, not_consequence_lewisWould). Finally, Lewis's might as the dual of would collapses into would under conditional excluded middle; reading might instead as a possibility operator over the whole conditional keeps Lewis's formulation, if A, might B true exactly when if A, would not-B is not true, for a possible antecedent (selectionalMight_iff), and separates might from would through indeterminacy (might_would_asymmetry).

Implementation notes

The conditional logic of the first section is abstract: a conditional operator on propositions with right weakening, agglomeration and a valid tautological consequent, the finite form of the consequence condition. The limit assumption is stated for an arbitrary similarity ordering and antecedent without closest worlds, the situation of the line example, rather than on a model of lengths. The selection-similarity correspondence of the paper's opening, the Moore-paradoxical status of denying a would while affirming a might, and the Kennedy example are not formalized.

References

• [Sta81]
• [Lew73b]
• [Qui50]
• [vF66]

Conditional excluded middle and distribution

structure Stalnaker1981.ConsequenceCondition {W : Type u_1} (cond : Set W → Set W → Set W) : Prop

A conditional operator satisfies the finite consequence condition when it weakens its consequent, agglomerates consequents, and has every tautological consequent.

• mono (A B C : Set W) : B ⊆ C → cond A B ⊆ cond A C
• agg (A B C : Set W) : cond A B ∩ cond A C ⊆ cond A (B ∩ C)
• taut (A : Set W) : cond A Set.univ = Set.univ

def Stalnaker1981.CEM {W : Type u_1} (cond : Set W → Set W → Set W) : Prop

Conditional excluded middle holds for an operator when a conditional or its opposite holds everywhere.

Equations

• Stalnaker1981.CEM cond = ∀ (A B : Set W), cond A B ∪ cond A Bᶜ = Set.univ

def Stalnaker1981.Distribution {W : Type u_1} (cond : Set W → Set W → Set W) : Prop

An operator distributes when a conditional with a disjunctive consequent yields one with a disjunct.

Equations

• Stalnaker1981.Distribution cond = ∀ (A B C : Set W), cond A (B ∪ C) ⊆ cond A B ∪ cond A C

theorem Stalnaker1981.cem_iff_distribution {W : Type u_1} (cond : Set W → Set W → Set W) (h : ConsequenceCondition cond) : CEM cond ↔ Distribution cond

Under the consequence condition, conditional excluded middle and distribution are equivalent.

Selection: excluded middle and scope

theorem Stalnaker1981.selection_cem {W : Type u_1} (s : Conditional.SelectionFunction W) (A B : Set W) (w : W) : w ∈ Conditional.selectionConditional s A B ∨ w ∈ Conditional.selectionConditional s A Bᶜ

A determinate selection function validates conditional excluded middle.

theorem Stalnaker1981.selection_scope {W : Type u_1} (s : Conditional.SelectionFunction W) {ι : Type u_2} {A : Set W} (hA : A.Nonempty) (F : ι → Set W) (w : W) : w ∈ Conditional.selectionConditional s A (⋃ (x : ι), F x) ↔ ∃ (x : ι), w ∈ Conditional.selectionConditional s A (F x)

Under selection, a quantifier inside the consequent and one outside the conditional coincide for a possible antecedent, so there is no scope ambiguity.

Bizet and Verdi

inductive Stalnaker1981.BVWorld : Type

The worlds of the Bizet–Verdi example are the actual world and the two closest worlds in which the composers are compatriots.

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

@[instance_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.

@[instance_reducible]

instance Stalnaker1981.instDecidableEqBVWorld : DecidableEq BVWorld

Equations

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

@[instance_reducible]

instance Stalnaker1981.instFintypeBVWorld : Fintype BVWorld

Equations

• Stalnaker1981.instFintypeBVWorld = { elems := { val := ↑Stalnaker1981.BVWorld.enumList, nodup := Stalnaker1981.BVWorld.enumList_nodup }, complete := Stalnaker1981.instFintypeBVWorld._proof_1 }

@[reducible, inline]

abbrev Stalnaker1981.bvSim (w₀ : BVWorld) : Preorder BVWorld

Similarity to w₀ puts w₀ strictly closest, and from the actual world the two compatriot worlds tie.

Equations

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

@[instance_reducible]

instance Stalnaker1981.instDecidableRelBVWorldLe (w₀ : BVWorld) : DecidableRel LE.le

Equations

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

theorem Stalnaker1981.isCentered_bvSim : Conditional.IsCentered bvSim

@[reducible, inline]

abbrev Stalnaker1981.compatriots : Set BVWorld

Bizet and Verdi are compatriots.

Equations

• Stalnaker1981.compatriots = {Stalnaker1981.BVWorld.bothItalian, Stalnaker1981.BVWorld.bothFrench}

@[reducible, inline]

abbrev Stalnaker1981.bizetItalian : Set BVWorld

Bizet is Italian.

Equations

• Stalnaker1981.bizetItalian = {Stalnaker1981.BVWorld.bothItalian}

@[reducible, inline]

abbrev Stalnaker1981.verdiFrench : Set BVWorld

Verdi is French.

Equations

• Stalnaker1981.verdiFrench = {Stalnaker1981.BVWorld.bothFrench}

theorem Stalnaker1981.bizet_italian_indet : Conditional.superCounterfactual bvSim compatriots bizetItalian BVWorld.actual = 0

If Bizet and Verdi had been compatriots, Bizet would have been Italian is neither true nor false on the supervaluation over completions, since the closest compatriot worlds disagree.

theorem Stalnaker1981.verdi_french_indet : Conditional.superCounterfactual bvSim compatriots verdiFrench BVWorld.actual = 0

If Bizet and Verdi had been compatriots, Verdi would have been French is neither true nor false.

theorem Stalnaker1981.bizet_verdi_cem : max (Conditional.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual) (Conditional.selectionalCounterfactual bvSim compatriots bizetItalianᶜ BVWorld.actual) ≠ -1

Conditional excluded middle holds for the example under supervaluation, since the disjunction of the conditional and its opposite is not false.

theorem Stalnaker1981.bizet_cem_fails_universal : BVWorld.actual ∉ Conditional.closestImp bvSim compatriots bizetItalian ∧ BVWorld.actual ∉ Conditional.closestImp bvSim compatriots bizetItalianᶜ

On the universal analysis both counterfactuals are false, and excluded middle fails, because the two closest compatriot worlds disagree on Bizet's nationality.

theorem Stalnaker1981.distribution_fails_bizetverdi : BVWorld.actual ∈ Conditional.closestImp bvSim compatriots (bizetItalian ∪ verdiFrench) ∧ BVWorld.actual ∉ Conditional.closestImp bvSim compatriots bizetItalian ∧ BVWorld.actual ∉ Conditional.closestImp bvSim compatriots verdiFrench

Quine's if they had been compatriots, Bizet would have been Italian or Verdi French is true on the universal analysis, but neither disjunct's conditional is, so distribution fails.

theorem Stalnaker1981.distribution_needs_uniqueness : Conditional.selectionalCounterfactual bvSim compatriots (bizetItalian ∪ verdiFrench) BVWorld.actual = 1 ∧ Conditional.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual = 0 ∧ Conditional.selectionalCounterfactual bvSim compatriots verdiFrench BVWorld.actual = 0

Under supervaluation the disjunctive conditional is true while each disjunct's conditional is indeterminate. Distribution holds on every completion but not on the supervaluation, whose closest worlds are not unique.

The Supreme Court appointment

inductive Stalnaker1981.CourtWorld : Type

The worlds of the appointment example are the actual world, with no vacancy, and two equally close worlds in which a vacancy is filled by a different woman.

• 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.

@[instance_reducible]

instance Stalnaker1981.instReprCourtWorld : Repr CourtWorld

Equations

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

@[instance_reducible]

instance Stalnaker1981.instDecidableEqCourtWorld : DecidableEq CourtWorld

Equations

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

@[instance_reducible]

instance Stalnaker1981.instFintypeCourtWorld : Fintype CourtWorld

Equations

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

@[reducible, inline]

abbrev Stalnaker1981.courtSim (w₀ : CourtWorld) : Preorder CourtWorld

Similarity to w₀ puts w₀ strictly closest, and from the actual world the two vacancy worlds tie.

Equations

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

@[instance_reducible]

instance Stalnaker1981.instDecidableRelCourtWorldLe (w₀ : CourtWorld) : DecidableRel LE.le

Equations

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

theorem Stalnaker1981.isCentered_courtSim : Conditional.IsCentered courtSim

@[reducible, inline]

abbrev Stalnaker1981.vacancy : Set CourtWorld

A vacancy occurs.

Equations

• Stalnaker1981.vacancy = {Stalnaker1981.CourtWorld.w1, Stalnaker1981.CourtWorld.w2}

inductive Stalnaker1981.Woman : Type

The women who might be appointed.

• a : Woman
• b : Woman

@[instance_reducible]

instance Stalnaker1981.instDecidableEqWoman : DecidableEq Woman

Equations

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

@[instance_reducible]

instance Stalnaker1981.instFintypeWoman : Fintype Woman

Equations

• Stalnaker1981.instFintypeWoman = { elems := { val := ↑Stalnaker1981.Woman.enumList, nodup := Stalnaker1981.Woman.enumList_nodup }, complete := Stalnaker1981.instFintypeWoman._proof_1 }

def Stalnaker1981.appointed : Woman → Set CourtWorld

Woman a is appointed in the first vacancy world, woman b in the second.

Equations

• Stalnaker1981.appointed Stalnaker1981.Woman.a = {Stalnaker1981.CourtWorld.w1}
• Stalnaker1981.appointed Stalnaker1981.Woman.b = {Stalnaker1981.CourtWorld.w2}

@[instance_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldMemSetAppointed (x : Woman) : DecidablePred fun (x_1 : CourtWorld) => x_1 ∈ appointed x

Equations

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

@[instance_reducible]

instance Stalnaker1981.instDecidablePredCourtWorldMemSetIUnionWomanAppointed : DecidablePred fun (x : CourtWorld) => x ∈ ⋃ (x : Woman), appointed x

Equations

• Stalnaker1981.instDecidablePredCourtWorldMemSetIUnionWomanAppointed w = decidable_of_iff (∃ (x : Stalnaker1981.Woman), w ∈ Stalnaker1981.appointed x) ⋯

theorem Stalnaker1981.court_scope_universal : CourtWorld.actual ∈ Conditional.closestImp courtSim vacancy (⋃ (x : Woman), appointed x) ∧ ¬∃ (x : Woman), CourtWorld.actual ∈ Conditional.closestImp courtSim vacancy (appointed x)

On the universal analysis the narrow scope, he would have appointed some woman, is true while the wide scope, some woman is such that he would have appointed her, is false, a scope ambiguity that Lewis's analysis predicts and speakers do not perceive.

theorem Stalnaker1981.court_no_particular_woman : Conditional.superCounterfactual courtSim vacancy (⋃ (x : Woman), appointed x) CourtWorld.actual = 1 ∧ ∀ (x : Woman), Conditional.superCounterfactual courtSim vacancy (appointed x) CourtWorld.actual = 0

Under supervaluation the narrow scope is true while each woman's conditional is indeterminate, so there is no particular woman he would have appointed, by underdetermination rather than ambiguity.

The limit assumption

theorem Stalnaker1981.lewisWould_ne {W : Type u_1} {ord : W → Preorder W} {A : Set W} {w : W} (h : (ord w).minimals A = ∅) (x : W) : w ∈ Conditional.variablyStrictImp ord A {x}ᶜ

Where an antecedent has no closest worlds, as for [Lew73b]'s line more than an inch long, if A, it would not be x is true on Lewis's analysis for every world x, since below any antecedent-world there is a closer one.

theorem Stalnaker1981.not_lewisMight_eq {W : Type u_1} {ord : W → Preorder W} {A : Set W} {w : W} (h : (ord w).minimals A = ∅) (x : W) : w ∉ Conditional.might (Conditional.variablyStrictImp ord) A {x}

So there is no world the antecedent might have been, on Lewis's might.

theorem Stalnaker1981.not_consequence_lewisWould {W : Type u_1} {ord : W → Preorder W} {A : Set W} {w : W} (h : (ord w).minimals A = ∅) (hA : A.Nonempty) : ⋂ x ∈ A, {x}ᶜ ⊆ Aᶜ ∧ (∀ x ∈ A, w ∈ Conditional.variablyStrictImp ord A {x}ᶜ) ∧ w ∉ Conditional.variablyStrictImp ord A Aᶜ

Without the limit assumption the consequence condition fails. The consequents not x, over all antecedent-worlds x, jointly entail not A, each conditional is true, and for a possible antecedent the conditional with the entailed consequent is false.

Might

theorem Stalnaker1981.selectionalMight_iff {W : Type u_1} [Fintype W] (ord : W → Preorder W) [(w : W) → DecidableRel LE.le] (A B : Set W) [DecidablePred fun (x : W) => x ∈ A] [DecidablePred fun (x : W) => x ∈ B] (w : W) (h : ((ord w).minimals A).Nonempty) : Conditional.selectionalMight ord A B w ↔ Conditional.selectionalCounterfactual ord A Bᶜ w ≠ 1

Might as a possibility operator over the conditional keeps Lewis's formulation, on which if A, might B is true exactly when if A, would not-B is not true.

theorem Stalnaker1981.might_would_asymmetry : Conditional.selectionalMight bvSim compatriots bizetItalian BVWorld.actual ∧ Conditional.selectionalMight bvSim compatriots verdiFrench BVWorld.actual ∧ Conditional.selectionalCounterfactual bvSim compatriots bizetItalian BVWorld.actual = 0 ∧ Conditional.selectionalCounterfactual bvSim compatriots verdiFrench BVWorld.actual = 0

In the Bizet–Verdi example both might conditionals are true while both would conditionals are indeterminate. So might and would part, as they cannot on Lewis's dual under excluded middle.