Documentation

Studies.CiardelliZhangChampollion2018

Ciardelli, Zhang and Champollion 2018: Two switches in the theory of counterfactuals #

Two switches at the ends of a hallway control a light, on iff they are in the same position; both are up and the light is on (Fig. 1). Participants judged if switch A were down, the light would be off and its B counterpart true by a majority, and if switch A or switch B were down likewise, but not if switches A and B were not both up, the light would be off, though its antecedent is the De Morgan equivalent of the disjunction (Table 3). The contrast falsifies every minimal-change semantics, not one choice of similarity: whenever the two simple counterfactuals are true, any counterfactual quantifying over the closest antecedent worlds makes the not-both-up one true as well, a closest not-both-up world in which A is down being a closest A-down world (§1.2), and the argument extends to Kratzer's premise semantics (§6.3). The paper's positive proposal, a background semantics with the inquisitive lifting of disjunction (§3.2, §4), is not represented.

The four worlds, the wiring law and the five clauses are World, lightOn and the propositions aDn to lightOff, with aOrBdn_eq_notBothUp the De Morgan identity; under the Hamming similarity hammingSim the conditional of the closest worlds, Conditional.closestImp, makes all four counterfactuals true at the actual world, and selectionalCounterfactual and homogeneityCounterfactual make the falsified one true as well. minimal_change_forces_notBothUp is the §1.2 argument for any similarity ordering and consequent: a closest world of a union is a closest world of one of its parts (Preorder.minimals_union_subset); the three operators' versions are corollaries. The Table 3 counts are the rationals trueRate_*, table3_pattern the majority pattern the paper reads off them and deMorgan_antecedents_diverge the divergence of the equivalent pair.

References #

The switches scenario (Fig. 1) #

inductive CiardelliZhangChampollion2018.World :

The four worlds are named by the positions of A and B, u for up and d for down.

uu : World
ud : World
du : World
dd : World

Instances For

@[instance_reducible]

instance CiardelliZhangChampollion2018.instReprWorld :

Repr World

Equations

CiardelliZhangChampollion2018.instReprWorld = { reprPrec := CiardelliZhangChampollion2018.instReprWorld.repr }

def CiardelliZhangChampollion2018.instReprWorld.repr :

World → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance CiardelliZhangChampollion2018.instDecidableEqWorld :

DecidableEq World

Equations

CiardelliZhangChampollion2018.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CiardelliZhangChampollion2018.instFintypeWorld :

Fintype World

Equations

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

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.aUp :

Switch A is up.

Equations

CiardelliZhangChampollion2018.aUp = {CiardelliZhangChampollion2018.World.uu, CiardelliZhangChampollion2018.World.ud}

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.bUp :

Switch B is up.

Equations

CiardelliZhangChampollion2018.bUp = {CiardelliZhangChampollion2018.World.uu, CiardelliZhangChampollion2018.World.du}

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.lightOn :

The wiring puts the light on iff the switches are in the same position.

Equations

CiardelliZhangChampollion2018.lightOn = {CiardelliZhangChampollion2018.World.uu, CiardelliZhangChampollion2018.World.dd}

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.aDn :

Switch A is down.

Equations

CiardelliZhangChampollion2018.aDn = CiardelliZhangChampollion2018.aUp ᶜ

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.bDn :

Switch B is down.

Equations

CiardelliZhangChampollion2018.bDn = CiardelliZhangChampollion2018.bUp ᶜ

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.aOrBdn :

Switch A is down or switch B is down.

Equations

CiardelliZhangChampollion2018.aOrBdn = CiardelliZhangChampollion2018.aDn ∪ CiardelliZhangChampollion2018.bDn

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.notBothUp :

Switches A and B are not both up.

Equations

CiardelliZhangChampollion2018.notBothUp = (CiardelliZhangChampollion2018.aUp ∩ CiardelliZhangChampollion2018.bUp)ᶜ

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.lightOff :

The light is off.

Equations

CiardelliZhangChampollion2018.lightOff = CiardelliZhangChampollion2018.lightOn ᶜ

Instances For

De Morgan equivalence #

theorem CiardelliZhangChampollion2018.aOrBdn_eq_notBothUp :

aOrBdn = notBothUp

The two antecedents have the same truth conditions.

Predictions under Hamming similarity #

def CiardelliZhangChampollion2018.hamming :

World → World → ℕ

The number of switches on which two worlds differ.

Equations

Instances For

@[reducible, inline]

abbrev CiardelliZhangChampollion2018.hammingSim (w₀ : World) :

Preorder World

Similarity by Hamming distance, one natural ordering on the scenario.

Equations

CiardelliZhangChampollion2018.hammingSim w₀ = Preorder.lift (CiardelliZhangChampollion2018.hamming w₀)

Instances For

theorem CiardelliZhangChampollion2018.aDn_off_at_uu :

World.uu ∈ Conditional.closestImp hammingSim aDn lightOff

If A were down, the light would be off is true at the actual world, since the closest A-down world is du.

theorem CiardelliZhangChampollion2018.bDn_off_at_uu :

World.uu ∈ Conditional.closestImp hammingSim bDn lightOff

If B were down, the light would be off is true at the actual world.

theorem CiardelliZhangChampollion2018.aOrBdn_off_at_uu :

World.uu ∈ Conditional.closestImp hammingSim aOrBdn lightOff

If A or B were down, the light would be off is true at the actual world, since the closest worlds are ud and du.

theorem CiardelliZhangChampollion2018.notBothUp_off_at_uu :

World.uu ∈ Conditional.closestImp hammingSim notBothUp lightOff

If A and B were not both up, the light would be off is predicted true at the actual world, the antecedent being equivalent to the disjunction; participants judged it true only by a minority (Table 3).

theorem CiardelliZhangChampollion2018.selectional_notBothUp_off_at_uu :

Conditional.selectionalCounterfactual hammingSim notBothUp lightOff World.uu = 1

The selectional counterfactual makes the same prediction.

theorem CiardelliZhangChampollion2018.homogeneity_notBothUp_off_at_uu :

Conditional.homogeneityCounterfactual hammingSim notBothUp lightOff World.uu = 1

The homogeneity counterfactual makes the same prediction, with its presupposition satisfied.

Minimal change forces the equivalence (§1.2) #

theorem CiardelliZhangChampollion2018.minimal_change_forces_notBothUp (ord : World → Preorder World) (w₀ : World) {C : Set World} (h_a : w₀ ∈ Conditional.closestImp ord aDn C) (h_b : w₀ ∈ Conditional.closestImp ord bDn C) :

w₀ ∈ Conditional.closestImp ord notBothUp C

For any similarity ordering and consequent, if the A-down and the B-down counterfactuals are true, so is the not-both-up one, since a closest not-both-up world is a closest A-down or a closest B-down world.

theorem CiardelliZhangChampollion2018.selectional_minimal_change_forces_notBothUp_off (ord : World → Preorder World) [(w : World) → DecidableRel LE.le] (w₀ : World) (h_a : Conditional.selectionalCounterfactual ord aDn lightOff w₀ = 1) (h_b : Conditional.selectionalCounterfactual ord bDn lightOff w₀ = 1) :

Conditional.selectionalCounterfactual ord notBothUp lightOff w₀ = 1

The selectional counterfactual's true verdict is the same quantifier.

theorem CiardelliZhangChampollion2018.homogeneity_minimal_change_forces_notBothUp_off (ord : World → Preorder World) (w₀ : World) (h_a : Conditional.homogeneityCounterfactual ord aDn lightOff w₀ = 1) (h_b : Conditional.homogeneityCounterfactual ord bDn lightOff w₀ = 1) :

Conditional.homogeneityCounterfactual ord notBothUp lightOff w₀ = 1

The homogeneity counterfactual's true verdict, with its presupposition satisfied, is the same quantifier.

The main experiment (Table 3) #

def CiardelliZhangChampollion2018.trueRate_aDn_off :

ℚ

The proportion judged true of if A were down, the light would be off.

Equations

CiardelliZhangChampollion2018.trueRate_aDn_off = 169 / 256

Instances For

def CiardelliZhangChampollion2018.trueRate_bDn_off :

ℚ

The proportion judged true of if B were down, the light would be off.

Equations

CiardelliZhangChampollion2018.trueRate_bDn_off = 153 / 235

Instances For

def CiardelliZhangChampollion2018.trueRate_aOrBdn_off :

ℚ

The proportion judged true of if A or B were down, the light would be off.

Equations

CiardelliZhangChampollion2018.trueRate_aOrBdn_off = 251 / 362

Instances For

def CiardelliZhangChampollion2018.trueRate_notBothUp_off :

ℚ

The proportion judged true of if A and B were not both up, the light would be off.

Equations

CiardelliZhangChampollion2018.trueRate_notBothUp_off = 82 / 372

Instances For

def CiardelliZhangChampollion2018.trueRate_notBothUp_on :

ℚ

The proportion judged true of if A and B were not both up, the light would be on.

Equations

CiardelliZhangChampollion2018.trueRate_notBothUp_on = 43 / 200

Instances For

theorem CiardelliZhangChampollion2018.table3_pattern :

(1 / 2 < trueRate_aDn_off ∧ 1 / 2 < trueRate_bDn_off ∧ 1 / 2 < trueRate_aOrBdn_off) ∧ trueRate_notBothUp_off < 1 / 2 ∧ trueRate_notBothUp_on < 1 / 2

The first three sentences were judged true by a majority and the two not-both-up sentences were not.

theorem CiardelliZhangChampollion2018.deMorgan_antecedents_diverge :

trueRate_notBothUp_off < trueRate_aOrBdn_off

The De Morgan pair diverges, the disjunctive antecedent being judged true more often than its equivalent.