Documentation

Studies.McKayVanInwagen1977

McKay and van Inwagen (1977): Counterfactuals with Disjunctive Antecedents #

This file formalizes the defence in [McKVI77] of the variably strict conditional of [Lew73b] against simplification of disjunctive antecedents, the inference from a counterfactual with a disjunctive antecedent to the counterfactual from either disjunct. Two arguments are stated on the substrate's variably strict conditional. The bumper-crop argument: the English sentence is false while the disjunctive-closure reading is true, so the sentence is regimented as the conjunction of the per-disjunct counterfactuals, which is false as required. 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, yet simplification would yield the absurd counterfactual from the Allied disjunct.

Implementation notes #

Both readings reduce to Conditional.variablyStrictImp, evaluated on the disjunction or conjoined over the disjuncts, with propositions as sets of worlds of enumerated world types. Similarity is a ranking of the worlds, so it is total as [Lew73b]'s comparative similarity requires, and with finitely many worlds each verdict is computed on the closest antecedent-worlds (holds).

References #

theorem McKayVanInwagen1977.holds {W : Type u_1} [Finite W] {α : Type u_2} [LinearOrder α] (d : W → W → α) (p q : Set W) :

Conditional.variablyStrictImp (fun (w : W) => Preorder.lift (d w)) p q = Conditional.closestImp (fun (w : W) => Preorder.lift (d w)) p q

On a ranking of finitely many worlds the variably strict conditional is the conditional of the closest antecedent-worlds.

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 :

actual : CropWorld
goodWeather : CropWorld
sunCold : CropWorld

Instances For

def McKayVanInwagen1977.instReprCropWorld.repr :

CropWorld → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance McKayVanInwagen1977.instReprCropWorld :

Equations

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

@[instance_reducible]

instance McKayVanInwagen1977.instDecidableEqCropWorld :

DecidableEq CropWorld

Equations

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

@[instance_reducible]

instance McKayVanInwagen1977.instFintypeCropWorld :

Fintype CropWorld

Equations

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

def McKayVanInwagen1977.cropRank :

CropWorld → ℕ

A good-weather world is more like the actual world than any world in which the sun grows cold, which the paper takes to be "surely true".

Equations

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.cropSim :

CropWorld → Preorder CropWorld

Similarity to the actual world, by rank.

Equations

McKayVanInwagen1977.cropSim x✝ = Preorder.lift McKayVanInwagen1977.cropRank

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.goodWeather :

The good-weather worlds.

Equations

McKayVanInwagen1977.goodWeather = {McKayVanInwagen1977.CropWorld.goodWeather}

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.sunCold :

The worlds where the sun grows cold.

Equations

McKayVanInwagen1977.sunCold = {McKayVanInwagen1977.CropWorld.sunCold}

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.bumperCrop :

The bumper-crop worlds: the good-weather world.

Equations

McKayVanInwagen1977.bumperCrop = {McKayVanInwagen1977.CropWorld.goodWeather}

Instances For

theorem McKayVanInwagen1977.bumperCrop_lewis_true :

CropWorld.actual ∈ Conditional.variablyStrictImp cropSim (goodWeather ∪ sunCold) bumperCrop

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 :

¬(CropWorld.actual ∈ Conditional.variablyStrictImp cropSim goodWeather bumperCrop ∧ CropWorld.actual ∈ Conditional.variablyStrictImp cropSim sunCold bumperCrop)

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 :

CropWorld.actual ∈ Conditional.variablyStrictImp cropSim (goodWeather ∪ sunCold) bumperCrop ∧ ¬(CropWorld.actual ∈ Conditional.variablyStrictImp cropSim goodWeather bumperCrop ∧ CropWorld.actual ∈ Conditional.variablyStrictImp cropSim sunCold bumperCrop)

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 :

actual : SpainWorld
axis : SpainWorld
allies : SpainWorld

Instances For

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

Instances For

@[instance_reducible]

instance McKayVanInwagen1977.instDecidableEqSpainWorld :

DecidableEq SpainWorld

Equations

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

@[instance_reducible]

instance McKayVanInwagen1977.instFintypeSpainWorld :

Fintype SpainWorld

Equations

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

def McKayVanInwagen1977.spainRank :

SpainWorld → ℕ

Axis-worlds rank closer to actual than Allied ones: the paper asserts the counterfactual without stating an ordering, and this is the ranking that makes it true.

Equations

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.spainSim :

SpainWorld → Preorder SpainWorld

Similarity to the actual world, by rank.

Equations

McKayVanInwagen1977.spainSim x✝ = Preorder.lift McKayVanInwagen1977.spainRank

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.foughtAxis :

The worlds where Spain fought with the Axis.

Equations

McKayVanInwagen1977.foughtAxis = {McKayVanInwagen1977.SpainWorld.axis}

Instances For

@[reducible, inline]

abbrev McKayVanInwagen1977.foughtAllies :

The worlds where Spain fought with the Allies.

Equations

McKayVanInwagen1977.foughtAllies = {McKayVanInwagen1977.SpainWorld.allies}

Instances For

theorem McKayVanInwagen1977.spain_lewis_true :

SpainWorld.actual ∈ Conditional.variablyStrictImp spainSim (foughtAxis ∪ foughtAllies) foughtAxis

Lewis's disjunctive-closure reading is TRUE: the closest (Axis ∨ Allies)-world is the Axis-world. 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 :

SpainWorld.actual ∉ Conditional.variablyStrictImp spainSim foughtAllies foughtAxis

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.sda_invalid :

∃ (W : Type) (ord : W → Preorder W) (A : Set W) (B : Set W) (C : Set W), ∃ w ∈ Conditional.variablyStrictImp ord (A ∪ B) C, w ∉ Conditional.variablyStrictImp ord B C

SDA is not a valid schema for counterfactuals. The Spain example: (Axis ∨ Allies) > Axis is true, but Allies > Axis is false.