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

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

Core Contribution

Defends Lewis'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 Lewis'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."

Integration

• The conjunction regimentation corresponds to sdaEval in AlternativeSensitive.lean
• Lewis's disjunctive-closure semantics corresponds to lewisDAC

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.CropWorld : Type

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

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprCropWorld.repr : CropWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprCropWorld : Repr CropWorld

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprCropWorld = { reprPrec := Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprCropWorld.repr }

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instDecidableEqCropWorld : DecidableEq CropWorld

Equations

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

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqCropWorld.beq : CropWorld → CropWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqCropWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqCropWorld : BEq CropWorld

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqCropWorld = { beq := Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqCropWorld.beq }

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.cropCloser : CropWorld → CropWorld → CropWorld → Bool

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.cropDomain : List CropWorld

Equations

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

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.goodWeather : CropWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.goodWeather Phenomena.Conditionals.Studies.McKayVanInwagen1977.CropWorld.goodWeather = true
• Phenomena.Conditionals.Studies.McKayVanInwagen1977.goodWeather x✝ = false

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.sunCold : CropWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.sunCold Phenomena.Conditionals.Studies.McKayVanInwagen1977.CropWorld.sunCold = true
• Phenomena.Conditionals.Studies.McKayVanInwagen1977.sunCold x✝ = false

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.bumperCrop : CropWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.bumperCrop Phenomena.Conditionals.Studies.McKayVanInwagen1977.CropWorld.goodWeather = true
• Phenomena.Conditionals.Studies.McKayVanInwagen1977.bumperCrop x✝ = false

theorem Phenomena.Conditionals.Studies.McKayVanInwagen1977.bumperCrop_lewis_true : Semantics.Conditionals.AlternativeSensitive.lewisDAC cropCloser cropDomain goodWeather sunCold bumperCrop CropWorld.actual = true

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.bumperCrop_conjunction_false : Semantics.Conditionals.AlternativeSensitive.sdaEval cropCloser cropDomain [goodWeather, sunCold] bumperCrop CropWorld.actual = false

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.lewis_ne_conjunction : Semantics.Conditionals.AlternativeSensitive.lewisDAC cropCloser cropDomain goodWeather sunCold bumperCrop CropWorld.actual ≠ Semantics.Conditionals.AlternativeSensitive.sdaEval cropCloser cropDomain [goodWeather, sunCold] bumperCrop CropWorld.actual

Lewis's disjunctive closure and the conjunction regimentation diverge. 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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.SpainWorld : Type

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

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprSpainWorld.repr : SpainWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprSpainWorld : Repr SpainWorld

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprSpainWorld = { reprPrec := Phenomena.Conditionals.Studies.McKayVanInwagen1977.instReprSpainWorld.repr }

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instDecidableEqSpainWorld : DecidableEq SpainWorld

Equations

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

instance Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqSpainWorld : BEq SpainWorld

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqSpainWorld = { beq := Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqSpainWorld.beq }

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqSpainWorld.beq : SpainWorld → SpainWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.instBEqSpainWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.spainCloser : SpainWorld → SpainWorld → SpainWorld → Bool

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.spainDomain : List SpainWorld

Equations

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

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAxis : SpainWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAxis Phenomena.Conditionals.Studies.McKayVanInwagen1977.SpainWorld.axis = true
• Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAxis x✝ = false

def Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAllies : SpainWorld → Bool

Equations

• Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAllies Phenomena.Conditionals.Studies.McKayVanInwagen1977.SpainWorld.allies = true
• Phenomena.Conditionals.Studies.McKayVanInwagen1977.foughtAllies x✝ = false

theorem Phenomena.Conditionals.Studies.McKayVanInwagen1977.spain_lewis_true : Semantics.Conditionals.AlternativeSensitive.lewisDAC spainCloser spainDomain foughtAxis foughtAllies foughtAxis SpainWorld.actual = true

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.allies_implies_axis_false : Semantics.Conditionals.AlternativeSensitive.sdaEval spainCloser spainDomain [foughtAllies] foughtAxis SpainWorld.actual = false

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 Phenomena.Conditionals.Studies.McKayVanInwagen1977.spain_conjunction_false : Semantics.Conditionals.AlternativeSensitive.sdaEval spainCloser spainDomain [foughtAxis, foughtAllies] foughtAxis SpainWorld.actual = false

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

theorem Phenomena.Conditionals.Studies.McKayVanInwagen1977.sda_invalid : ∃ (W : Type) (x : DecidableEq W) (closer : W → W → W → Bool) (domain : List W) (A : W → Bool) (B : W → Bool) (C : W → Bool) (w : W), Semantics.Conditionals.AlternativeSensitive.lewisDAC closer domain A B C w = true ∧ Semantics.Conditionals.AlternativeSensitive.sdaEval closer domain [B] C w = false

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.

Divergence of Readings

In both examples, Lewis's disjunctive closure (lewisDAC) returns true while the conjunction regimentation (sdaEval) returns false. But the English judgments differ:

• Spain: the English sentence is acceptable (matches Lewis)
• Bumper crop: the English sentence is unacceptable (matches conjunction)

This shows that natural-language "or" in counterfactual antecedents does not uniformly correspond to either formal reading. The ambiguity is between conjunction/SDA (each disjunct evaluated separately) and Lewis's disjunctive closure (disjuncts combined before evaluation).

theorem Phenomena.Conditionals.Studies.McKayVanInwagen1977.readings_diverge : (Semantics.Conditionals.AlternativeSensitive.lewisDAC spainCloser spainDomain foughtAxis foughtAllies foughtAxis SpainWorld.actual = true ∧ Semantics.Conditionals.AlternativeSensitive.sdaEval spainCloser spainDomain [foughtAxis, foughtAllies] foughtAxis SpainWorld.actual = false) ∧ Semantics.Conditionals.AlternativeSensitive.lewisDAC cropCloser cropDomain goodWeather sunCold bumperCrop CropWorld.actual = true ∧ Semantics.Conditionals.AlternativeSensitive.sdaEval cropCloser cropDomain [goodWeather, sunCold] bumperCrop CropWorld.actual = false

Both examples show the two formal readings diverge: Lewis gives true, conjunction gives false. The English judgments select different readings in each case — confirming that natural-language "or" in counterfactual antecedents is ambiguous between the two.