McKay & Van Inwagen 1977 @cite{mckay-vaninwagen-1977}

Counterfactuals with Disjunctive Antecedents. Philosophical Studies 31: 353–356.

Core Contribution

Defends @cite{lewis-1973}'s variably strict conditional semantics against the claim that Simplification of Disjunctive Antecedents (SDA) should be valid:

SDA: [(A ∨ B) > C] ⊃ (B > C)

Critics (Nute 1975, Fine 1975, Creary & Hill 1975) proposed SDA as a validity constraint on counterfactual logic. McKay & Van Inwagen refute this with two arguments:

1. The bumper crop argument: The English sentence "if good weather or sun cold, bumper crop" is false, but @cite{lewis-1973}'s disjunctive-closure reading (goodWeather ∨ sunCold) > bumperCrop is true. So the English sentence is NOT equivalent to the disjunctive-closure reading. The correct regimentation is the conjunction (goodWeather > bumperCrop) ∧ (sunCold > bumperCrop), which IS false — matching the English judgment.

2. The Spain counterexample: "If Spain had fought on the Axis side or the Allied side, Spain would have fought on the Axis side" is acceptable, but SDA gives the absurd "If Spain had fought on the Allied side, Spain would have fought on the Axis side."

Substrate consumption

Both readings reduce to the canonical Lewis universal counterfactual operator Conditionals.Counterfactual.universalCounterfactual. The disjunctive-closure reading evaluates the operator on A ∨ B; the conjunction regimentation conjoins per-disjunct evaluations. Worlds and predicates are typed Prop (not Bool) — DecidablePred instances are auto-derived from DecidableEq on the world enums.

The Bumper Crop Argument

The critics argue that Lewis's semantics is wrong using the sentence:

S: "If we were to have good weather this summer or if the sun were to grow cold, we would have a bumper crop."

They claim S is equivalent to the regimented counterfactual S* = (goodWeather ∨ sunCold) > bumperCrop. Since Lewis's semantics makes S* true (the closest (goodWeather ∨ sunCold)-world has good weather, hence bumper crop) but S is clearly false, Lewis must be wrong.

McKay & Van Inwagen's rebuttal: premise (2) is false — S is NOT equivalent to S*. The correct regimentation of S is the conjunction (goodWeather > bumperCrop) ∧ (sunCold > bumperCrop), which IS false on Lewis's semantics, matching the English judgment.

inductive McKayVanInwagen1977.CropWorld : Type

• actual : CropWorld
• goodWeather : CropWorld
• sunCold : CropWorld

def McKayVanInwagen1977.instReprCropWorld.repr : CropWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McKayVanInwagen1977.instReprCropWorld : Repr CropWorld

Equations

• McKayVanInwagen1977.instReprCropWorld = { reprPrec := McKayVanInwagen1977.instReprCropWorld.repr }

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidableEqCropWorld : DecidableEq CropWorld

Equations

• McKayVanInwagen1977.instDecidableEqCropWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance McKayVanInwagen1977.instFintypeCropWorld : Fintype CropWorld

Equations

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

def McKayVanInwagen1977.cropSim : Core.Order.SimilarityOrdering CropWorld

Good weather is much more similar to the actual world than the sun growing cold.

Equations

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

def McKayVanInwagen1977.goodWeather (w : CropWorld) : Prop

"Good weather" world predicate.

Equations

• McKayVanInwagen1977.goodWeather w = (w = McKayVanInwagen1977.CropWorld.goodWeather)

def McKayVanInwagen1977.sunCold (w : CropWorld) : Prop

"Sun cold" world predicate.

Equations

• McKayVanInwagen1977.sunCold w = (w = McKayVanInwagen1977.CropWorld.sunCold)

def McKayVanInwagen1977.bumperCrop (w : CropWorld) : Prop

"Bumper crop" world predicate. True at the good-weather world.

Equations

• McKayVanInwagen1977.bumperCrop w = (w = McKayVanInwagen1977.CropWorld.goodWeather)

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidablePredCropWorldGoodWeather : DecidablePred goodWeather

Equations

• McKayVanInwagen1977.instDecidablePredCropWorldGoodWeather w = decEq w McKayVanInwagen1977.CropWorld.goodWeather

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidablePredCropWorldSunCold : DecidablePred sunCold

Equations

• McKayVanInwagen1977.instDecidablePredCropWorldSunCold w = decEq w McKayVanInwagen1977.CropWorld.sunCold

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidablePredCropWorldBumperCrop : DecidablePred bumperCrop

Equations

• McKayVanInwagen1977.instDecidablePredCropWorldBumperCrop w = decEq w McKayVanInwagen1977.CropWorld.goodWeather

theorem McKayVanInwagen1977.bumperCrop_lewis_true : Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim (fun (w : CropWorld) => goodWeather w ∨ sunCold w) bumperCrop CropWorld.actual

S* (Lewis disjunctive closure) is TRUE: the closest (goodWeather ∨ sunCold)-world is a good-weather world. This is premise (3) of the critics' argument.

theorem McKayVanInwagen1977.bumperCrop_conjunction_false : ¬(Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim goodWeather bumperCrop CropWorld.actual ∧ Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim sunCold bumperCrop CropWorld.actual)

The conjunction regimentation is FALSE: "if the sun grew cold, we'd have a bumper crop" is false. This matches the English judgment that S is false.

theorem McKayVanInwagen1977.lewis_ne_conjunction : Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim (fun (w : CropWorld) => goodWeather w ∨ sunCold w) bumperCrop CropWorld.actual ∧ ¬(Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim goodWeather bumperCrop CropWorld.actual ∧ Semantics.Conditionals.Counterfactual.universalCounterfactual cropSim sunCold bumperCrop CropWorld.actual)

Lewis's disjunctive closure is true while the conjunction regimentation is false. Since the English sentence S is false (matching the conjunction) while S* is true (matching Lewis), S ≠ S*: premise (2) is false.

The Spain Example

"Neither. Spain did not enter the war. But if she had fought on one side or the other, it would have been the Axis."

That is, we assert: (Axis ∨ Allies) > Axis. This is true on Lewis's semantics (Spain was ideologically closer to the Axis).

But if SDA were valid, it would follow that: Allies > Axis — "If Spain had fought on the Allied side, Spain would have fought on the Axis side." This is absurd.

inductive McKayVanInwagen1977.SpainWorld : Type

• actual : SpainWorld
• axis : SpainWorld
• allies : SpainWorld

@[implicit_reducible]

instance McKayVanInwagen1977.instReprSpainWorld : Repr SpainWorld

Equations

• McKayVanInwagen1977.instReprSpainWorld = { reprPrec := McKayVanInwagen1977.instReprSpainWorld.repr }

def McKayVanInwagen1977.instReprSpainWorld.repr : SpainWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidableEqSpainWorld : DecidableEq SpainWorld

Equations

• McKayVanInwagen1977.instDecidableEqSpainWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance McKayVanInwagen1977.instFintypeSpainWorld : Fintype SpainWorld

Equations

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

def McKayVanInwagen1977.spainSim : Core.Order.SimilarityOrdering SpainWorld

Axis is closer to actual than Allies (Spain's ideological alignment).

Equations

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

def McKayVanInwagen1977.foughtAxis (w : SpainWorld) : Prop

"Spain fought with the Axis" world predicate.

Equations

• McKayVanInwagen1977.foughtAxis w = (w = McKayVanInwagen1977.SpainWorld.axis)

def McKayVanInwagen1977.foughtAllies (w : SpainWorld) : Prop

"Spain fought with the Allies" world predicate.

Equations

• McKayVanInwagen1977.foughtAllies w = (w = McKayVanInwagen1977.SpainWorld.allies)

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidablePredSpainWorldFoughtAxis : DecidablePred foughtAxis

Equations

• McKayVanInwagen1977.instDecidablePredSpainWorldFoughtAxis w = decEq w McKayVanInwagen1977.SpainWorld.axis

@[implicit_reducible]

instance McKayVanInwagen1977.instDecidablePredSpainWorldFoughtAllies : DecidablePred foughtAllies

Equations

• McKayVanInwagen1977.instDecidablePredSpainWorldFoughtAllies w = decEq w McKayVanInwagen1977.SpainWorld.allies

theorem McKayVanInwagen1977.spain_lewis_true : Semantics.Conditionals.Counterfactual.universalCounterfactual spainSim (fun (w : SpainWorld) => foughtAxis w ∨ foughtAllies w) foughtAxis SpainWorld.actual

Lewis's disjunctive-closure reading is TRUE: the closest (Axis ∨ Allies)-world is the Axis-world, which satisfies C. The English sentence "if she had fought on one side or the other, it would have been the Axis" is acceptable.

theorem McKayVanInwagen1977.allies_implies_axis_false : ¬Semantics.Conditionals.Counterfactual.universalCounterfactual spainSim foughtAllies foughtAxis SpainWorld.actual

The absurd SDA simplification: "If Spain had fought on the Allied side, Spain would have fought on the Axis side" is false. This is what the SDA schema would derive from spain_lewis_true.

theorem McKayVanInwagen1977.spain_conjunction_false : ¬(Semantics.Conditionals.Counterfactual.universalCounterfactual spainSim foughtAxis foughtAxis SpainWorld.actual ∧ Semantics.Conditionals.Counterfactual.universalCounterfactual spainSim foughtAllies foughtAxis SpainWorld.actual)

The conjunction reading (both simplifications must hold) is FALSE, because the Allies simplification fails.

theorem McKayVanInwagen1977.sda_invalid : ∃ (W : Type) (x : DecidableEq W) (x_1 : Fintype W) (sim : Core.Order.SimilarityOrdering W) (A : W → Prop) (B : W → Prop) (C : W → Prop) (x_2 : DecidablePred A) (x_3 : DecidablePred B) (x_4 : DecidablePred C) (w : W), Semantics.Conditionals.Counterfactual.universalCounterfactual sim (fun (v : W) => A v ∨ B v) C w ∧ ¬Semantics.Conditionals.Counterfactual.universalCounterfactual sim B C w

SDA is not a valid schema for counterfactuals. There exist propositions A, B, C and a world w such that (A ∨ B) > C is true but B > C is false. The Spain example: (Axis ∨ Allies) > Axis is true, but Allies > Axis is false.