@cite{ciardelli-zhang-champollion-2018} — Two switches in the theory of counterfactuals

Ciardelli, I., Zhang, L. & Champollion, L. (2018). Two switches in the theory of counterfactuals: A study of truth conditionality and minimal change. Linguistics and Philosophy 41(6): 577–621.

Headline finding

Two truth-conditionally equivalent clauses (A̅ ∨ B̅ and ¬(A ∧ B), related by De Morgan) make different semantic contributions when embedded as counterfactual antecedents. This challenges the textbook truth-conditional view of meaning AND falsifies any minimal-change semantics of counterfactuals — including Lewis-Stalnaker similarity semantics and Kratzer-style premise semantics.

The switches scenario (p. 578, Fig. 1)

Two switches A, B at opposite ends of a hallway. The light is on iff both switches are in the same position. Currently both are up, light is on. The crowdsourced experiment elicited truth judgments for five counterfactuals; the discriminating contrast (Tables 7–8, p. 607):

• A̅ > OFF ("If A were down, light would be off"): ~78% true
• B̅ > OFF: ~76% true
• A̅ ∨ B̅ > OFF: ~79% true
• ¬(A ∧ B) > OFF: ~20% true

A̅ ∨ B̅ and ¬(A ∧ B) are de-Morgan equivalent yet diverge sharply.

What this file proves

1. De Morgan equivalence: (A̅ ∨ B̅) = ¬(A ∧ B) as sets of worlds.
2. Concrete predictions across three operators: instantiating a Hamming-distance similarity ordering at the actual world uu, all three closest-worlds operators in linglib — universalCounterfactual (Lewis/Stalnaker), selectionalCounterfactual (Stalnaker + supervaluation, returns Truth3.true), and homogeneityCounterfactual (von Fintel/Križ, returns assertion = some true with satisfied presupposition) — all predict ¬(A ∧ B) > OFF true. This is the empirically falsified prediction (~20% true, Tables 7–8).
3. Generic structural argument (CZC §1.2 argument, p. 582): the operator-agnostic core (closestWorlds_predicate_forces_notBothUp) shows that for ANY similarity ordering and ANY consequent B, joint truth of "every closest aDn-world is B" and "every closest bDn-world is B" entails "every closest notBothUp-world is B". Three corollaries instantiate this for universalCounterfactual, selectionalCounterfactual, and homogeneityCounterfactual — closing CZC's claim that all minimal-change theories fail.

Connection to linglib's Kratzer infrastructure

@cite{ciardelli-zhang-champollion-2018} §6.3 extends the argument to standard premise semantics as formulated in @cite{kratzer-1981} (CZC cite both Kratzer 1981a and 1981b — only the 1981 "Notional Category" paper is in the linglib bib): "regardless of the particular ordering source that we consider, standard premise semantics still predicts that ... `¬(A ∧ B)

OFF` is true as well, contrary to our experimental findings." Per Lewis 1981, standard premise semantics is equivalent to ordering semantics with a weak partial order, which puts it in scope of the §1.2 argument formalized above.

Whether the argument extends to @cite{kratzer-2012}'s lumping-based revision (§5.4.4) is open and not addressed by CZC. The lumping CF truth condition (§5.4.4) is a quantifier alternation — "for every set in F_{w,p} there is a superset that implies q" — not the maximization-of-consistency pattern that the §1.2 argument falsifies. Lumping constrains which propositions can accompany an antecedent into a Crucial Set (the lumping-closure condition); it doesn't relax the for-all-supersets quantifier. Whether this rescues the analysis on the switches scenario requires building a properly situation-semantic switches model and instantiating Semantics.Conditionals.PremiseSemantic.wouldCF; we leave this as future work.

For the first concrete wouldCF instantiation on a situation-semantic scenario, see Phenomena.Conditionals.Studies.Kratzer2012Lumping — which formalizes Kratzer's own apple-buying example (§5.4.1–§5.4.3). That file establishes the template for an eventual situation-semantic switches model that would settle the question raised here.

The CZC positive proposal — a foreground/background distinction combined with inquisitive lifting (§4) — and §6.4's SNCA derivation (Proposition 2 + Lemma 1) are also left as future formalization.

The switches scenario

inductive Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World : Type

The four worlds, indexed by (A-position, B-position). Naming: u = up, d = down. So uu = both up, etc.

• uu : World

  A up, B up — the actual world; light is ON.

• ud : World

  A up, B down — light is OFF.

• du : World

  A down, B up — light is OFF.

• dd : World

  A down, B down — light is ON.

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instReprWorld : Repr World

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instReprWorld = { reprPrec := Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instReprWorld.repr }

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidableEqWorld : DecidableEq World

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instFintypeWorld : Fintype World

Equations

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

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp : World → Prop

Atomic propositions: switch positions and the light.

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.uu = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.ud = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.du = False
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.dd = False

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp : World → Prop

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.uu = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.du = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.ud = False
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.dd = False

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn : World → Prop

The wiring law (@cite{ciardelli-zhang-champollion-2018}, p. 578): light is on iff both switches are in the same position.

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.uu = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.dd = True
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.ud = False
• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.World.du = False

Antecedents and consequents

We follow the paper's notation: A̅ (aDn) means "switch A is down" and so on. The two key antecedents — A̅ ∨ B̅ (aOrBdn) and ¬(A ∧ B) (notBothUp) — are de-Morgan equivalent.

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aDn (w : World) : Prop

"Switch A is down."

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aDn w = ¬Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aUp w

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bDn (w : World) : Prop

"Switch B is down."

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bDn w = ¬Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bUp w

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aOrBdn (w : World) : Prop

"Switch A is down or switch B is down."

Equations

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

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.notBothUp (w : World) : Prop

"Switches A and B are not both up" (= ¬(A ∧ B)).

Equations

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

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOff (w : World) : Prop

"The light is off."

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOff w = ¬Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.lightOn w

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldAUp : DecidablePred aUp

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldBUp : DecidablePred bUp

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldLightOn : DecidablePred lightOn

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldADn : DecidablePred aDn

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldADn x✝ = Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldADn._aux_1 x✝

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldBDn : DecidablePred bDn

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldBDn x✝ = Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldBDn._aux_1 x✝

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldAOrBdn : DecidablePred aOrBdn

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldAOrBdn x✝ = Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldAOrBdn._aux_1 x✝

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldNotBothUp : DecidablePred notBothUp

Equations

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

@[implicit_reducible]

instance Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.instDecidablePredWorldLightOff : DecidablePred lightOff

Equations

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

De Morgan equivalence

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aOrBdn_iff_notBothUp (w : World) : aOrBdn w ↔ notBothUp w

A̅ ∨ B̅ and ¬(A ∧ B) are pointwise-equivalent: the two antecedents have identical truth conditions across the four worlds.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aOrBdn_eq_notBothUp : aOrBdn = notBothUp

The same equivalence as set equality (the truth-conditional content of the two antecedents coincides).

Concrete similarity ordering: Hamming distance

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.hamming : World → World → ℕ

Hamming distance between two worlds: the number of switch positions on which they disagree.

Equations

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

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.hammingSim : Core.Order.SimilarityOrdering World

Standard "edit distance" similarity ordering: w₁ is at least as close to w₀ as w₂ is iff hamming w₀ w₁ ≤ hamming w₀ w₂. This is one natural ordering on this scenario; the abstract theorem below shows the falsification doesn't depend on this choice.

Equations

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

Predictions of the universal/Lewis-Stalnaker counterfactual

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aDn_off_at_uu : Semantics.Conditionals.Counterfactual.universalCounterfactual hammingSim aDn lightOff World.uu

Prediction 1: A̅ > OFF is true at uu. (The closest A̅-world to uu is du — Hamming distance 1 — and the light is off there.) Empirically: ~78% true.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.bDn_off_at_uu : Semantics.Conditionals.Counterfactual.universalCounterfactual hammingSim bDn lightOff World.uu

Prediction 2: B̅ > OFF is true at uu. By the symmetric argument. Empirically: ~76% true.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.aOrBdn_off_at_uu : Semantics.Conditionals.Counterfactual.universalCounterfactual hammingSim aOrBdn lightOff World.uu

Prediction 3: A̅ ∨ B̅ > OFF is true at uu. The closest A̅ ∨ B̅-worlds are {ud, du} (both at Hamming distance 1), and the light is off in both. Empirically: ~79% true.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.notBothUp_off_at_uu : Semantics.Conditionals.Counterfactual.universalCounterfactual hammingSim notBothUp lightOff World.uu

Prediction 4 (the falsified one): ¬(A ∧ B) > OFF is also predicted true at uu, since ¬(A ∧ B) and A̅ ∨ B̅ are de-Morgan equivalent. Empirically: only ~20% true.

This is the central empirical contrast of @cite{ciardelli-zhang-champollion-2018}: a truth-conditional semantics combined with minimal change cannot reproduce the sharp divergence between the two predictions, since the two antecedents are forced to behave identically.

Same falsified prediction under selectional and homogeneity

@cite{ciardelli-zhang-champollion-2018}'s argument targets any minimal-change semantics. Both selectionalCounterfactual (Stalnaker

• supervaluation) and homogeneityCounterfactual (von Fintel/Križ) share the same closest-worlds substrate as universalCounterfactual, and so make the same falsified prediction on the switches scenario.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.selectional_notBothUp_off_at_uu : Semantics.Conditionals.Counterfactual.selectionalCounterfactual hammingSim notBothUp lightOff World.uu = Core.Duality.Truth3.true

Selectional CF also predicts ¬(A ∧ B) > OFF true at uu.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.homogeneity_notBothUp_off_at_uu : Semantics.Conditionals.Counterfactual.homogeneityCounterfactual hammingSim notBothUp lightOff World.uu = { presupposition := Semantics.Conditionals.Counterfactual.PresupStatus.satisfied, assertion := some true }

Homogeneity CF also predicts ¬(A ∧ B) > OFF true at uu, with satisfied presupposition (the closest worlds are not mixed on lightOff).

Abstract minimal-change forcing (@cite{ciardelli-zhang-champollion-2018} §1.2, p. 582)

The concrete predictions above used a specific similarity ordering. The following theorem strengthens the argument: for any similarity ordering whatsoever, if both A̅ > OFF and B̅ > OFF are true at a world, then ¬(A ∧ B) > OFF is forced true at that world. So there is no choice of similarity that vindicates the empirical pattern — the fault lies with the minimal-change architecture itself.

The generic structural argument

CZC's §1.2 proof actually targets any operator definable as "every closest A-world satisfies B". We expose the generic version first; the universal/selectional/homogeneity instantiations below all collapse to it.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.closestWorlds_predicate_forces_notBothUp (sim : Core.Order.SimilarityOrdering World) (w₀ : World) (B : World → Prop) [DecidablePred B] (h_a : ∀ w' ∈ sim.closestWorlds w₀ (Finset.filter aDn Finset.univ), B w') (h_b : ∀ w' ∈ sim.closestWorlds w₀ (Finset.filter bDn Finset.univ), B w') (w' : World) : w' ∈ sim.closestWorlds w₀ (Finset.filter notBothUp Finset.univ) → B w'

Generic minimal-change forcing: for any similarity ordering and any consequent predicate B, joint truth of "every closest aDn-world is B" and "every closest bDn-world is B" entails "every closest notBothUp-world is B".

This is the operator-agnostic core of CZC §1.2 p. 582. The structural fact is SimilarityOrdering.mem_closestWorlds_of_subset: a closest notBothUp-world that happens to be aDn is also a closest aDn-world (since aDn ⊆ notBothUp as Finsets), so h_a applies; symmetric for bDn.

Operator-specific corollaries

All three of universalCounterfactual, selectionalCounterfactual, and homogeneityCounterfactual reduce their "true" verdict to the same ∀ w' ∈ closestWorlds, B w' condition (the first if branch in each definition). The structural lemma above therefore applies verbatim, only differing in how each operator packages its truth value.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.minimal_change_forces_notBothUp_off (sim : Core.Order.SimilarityOrdering World) (w₀ : World) (h_a : Semantics.Conditionals.Counterfactual.universalCounterfactual sim aDn lightOff w₀) (h_b : Semantics.Conditionals.Counterfactual.universalCounterfactual sim bDn lightOff w₀) : Semantics.Conditionals.Counterfactual.universalCounterfactual sim notBothUp lightOff w₀

Universal CF version (Lewis/Stalnaker). Direct corollary of the generic lemma since universalCounterfactual is the universal quantifier over closest worlds.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.selectional_minimal_change_forces_notBothUp_off (sim : Core.Order.SimilarityOrdering World) (w₀ : World) (h_a : Semantics.Conditionals.Counterfactual.selectionalCounterfactual sim aDn lightOff w₀ = Core.Duality.Truth3.true) (h_b : Semantics.Conditionals.Counterfactual.selectionalCounterfactual sim bDn lightOff w₀ = Core.Duality.Truth3.true) : Semantics.Conditionals.Counterfactual.selectionalCounterfactual sim notBothUp lightOff w₀ = Core.Duality.Truth3.true

Selectional CF version (Stalnaker + supervaluation). When both simple counterfactuals return .true (every closest world is OFF), so does the disjunctive-antecedent counterfactual.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.homogeneity_minimal_change_forces_notBothUp_off (sim : Core.Order.SimilarityOrdering World) (w₀ : World) (h_a : Semantics.Conditionals.Counterfactual.homogeneityCounterfactual sim aDn lightOff w₀ = { presupposition := Semantics.Conditionals.Counterfactual.PresupStatus.satisfied, assertion := some true }) (h_b : Semantics.Conditionals.Counterfactual.homogeneityCounterfactual sim bDn lightOff w₀ = { presupposition := Semantics.Conditionals.Counterfactual.PresupStatus.satisfied, assertion := some true }) : Semantics.Conditionals.Counterfactual.homogeneityCounterfactual sim notBothUp lightOff w₀ = { presupposition := Semantics.Conditionals.Counterfactual.PresupStatus.satisfied, assertion := some true }

Homogeneity CF version (von Fintel/Križ). When both simple counterfactuals satisfy their presupposition with assertion = some true (every closest world is OFF), so does the disjunctive- antecedent version.

Empirical data (Tables 7 and 8, p. 607)

The "True" percentages from the main experiment, separated by presentation order. Reported as rationals for exact comparison.

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aDn_off_T7 : ℚ

Table 7: target precedes filler.

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aDn_off_T7 = 80 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_bDn_off_T7 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_bDn_off_T7 = 76 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aOrBdn_off_T7 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aOrBdn_off_T7 = 79 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_notBothUp_off_T7 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_notBothUp_off_T7 = 20 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aDn_off_T8 : ℚ

Table 8: filler precedes target.

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aDn_off_T8 = 53 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_bDn_off_T8 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_bDn_off_T8 = 53 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aOrBdn_off_T8 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_aOrBdn_off_T8 = 59 / 100

def Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_notBothUp_off_T8 : ℚ

Equations

• Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.percentTrue_notBothUp_off_T8 = 25 / 100

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.deMorgan_antecedents_diverge_T7 : percentTrue_aOrBdn_off_T7 - percentTrue_notBothUp_off_T7 ≥ 1 / 2

The discriminating empirical contrast (Table 7, p. 607): the two de-Morgan-equivalent antecedents A̅ ∨ B̅ and ¬(A ∧ B) produce sharply divergent truth-judgment rates when embedded as counterfactual antecedents.

theorem Phenomena.Conditionals.Studies.CiardelliZhangChampollion2018.prediction_pattern_falsified_T7 : percentTrue_aDn_off_T7 ≥ 3 / 4 ∧ percentTrue_bDn_off_T7 ≥ 3 / 4 ∧ percentTrue_notBothUp_off_T7 ≤ 1 / 4

The simple antecedents A̅ > OFF and B̅ > OFF are robustly judged true while ¬(A ∧ B) > OFF is robustly judged not-true (Table 7). This is the contrast that the abstract minimal-change forcing theorem rules out for any similarity ordering.