[CZC18] switches under [Kra12] lumping CF

Companion to Studies/CiardelliZhangChampollion2018.lean (which formalizes CZC's argument against minimal-change semantics) and to Studies/Kratzer2012Lumping.lean (which formalizes the §5.4.4 lumping CF on the Paula apple-buying scenario). This file applies the lumping CF to CZC's switches scenario and proves it has a different failure pattern than minimal-change CF.

The result: asymmetric failure across operators

| Operator                          | aDn > OFF | bDn > OFF | ¬(A∧B) > OFF |
| --------------------------------- | --------- | --------- | ------------ |
| Empirics (Tables 7–8)             | TRUE 78%  | TRUE 76%  | FALSE 20%    |
| Lewis/Stalnaker minimal-change    | TRUE ✓    | TRUE ✓    | TRUE ✗       |
| Kratzer 2012 lumping CF           | FALSE ✗   | FALSE ✗   | FALSE ✓      |

Lewis fails on the disjunctive antecedent (CiardelliZhangChampollion2018.minimal_change_forces_notBothUp_off plus notBothUp_off_at_uu makes this concrete). Lumping fails on simple antecedents (this file: not_wouldCF_aDn_lightOff and not_wouldCF_bDn_lightOff). And lumping correctly predicts the disjunctive case false (not_wouldCF_notBothUp_lightOff) — though for the same structural reason it gets the simple ones wrong.

Neither operator predicts all three correctly. This is a genuine theoretical incompatibility — exactly the kind that the linglib "interconnection density" goal exists to surface.

Why the asymmetry

Lewis CF restricts to the closest antecedent-worlds. For aDn > OFF: the closest aDn-world to uu is du (Hamming distance 1), where lightOff holds. For ¬(A∧B) > OFF: the closest are {ud, du}, both lightOff. Lewis correctly predicts the simple ones; the disjunctive prediction inherits CZC §1.2's structural failure.

Lumping CF considers all consistent extensions of the antecedent within an admissible Base Set. With aDn as antecedent at uu: any consistent extension that includes aDn is compatible with both du-style and dd-style worlds (since aDn ∩ Worlds = {du, dd}). Follows {aDn} lightOff therefore fails, since dd is an aDn-world where lightOff is false (both switches down → light on by the wiring). Without a closest-worlds restriction, lumping has no way to break the du/dd symmetry on the simple counterfactuals.

The symmetric upside: lumping correctly predicts ¬(A∧B) > OFF false, because Follows {notBothUp} lightOff also fails (again dd blocks).

Formalization

We use the worlds-only switches model lifted to a SituationFrame via Frame.toDiscreteSituationFrame. Under discrete parthood, Intensional.Lumping.Lumps.discrete_iff reduces lumping to joint truth at w. This gives a clean (if degenerate) lumping behavior: every fact true at uu lumps every other fact true at uu, so the Crucial Set's lumping-closure clause forces any Crucial Set member containing a Base-Set element to contain all Base-Set elements — which is incompatible with the counterfactual antecedent.

Therefore every Crucial Set in this model collapses to the singleton {antecedent}, and wouldCF reduces to Follows {antecedent} consequent, i.e., "every antecedent-world satisfies the consequent."

Scope and caveats

This is the worlds-only model (no proper partial situations beyond worlds-as-themselves). A more sophisticated partial-situation model with the wiring law as a [Kra12] §5.5 non-accidental generalization (rather than a contingent member of Fw) might ameliorate the asymmetry. We do not explore that here.

Fw₀ choice: we use the empty Base Set. The result generalizes — for any Base Set choice including the wiring law and the actual switch positions, the same dd-blocking argument forces Follows {aDn} lightOff false (since aDn ∩ Worlds = {du, dd} regardless of Fw). The empty Base Set keeps the proofs direct.

The switches model

inductive CiardelliZhangChampollion2018Lumping.World : Type

The four switch-position worlds (same as CiardelliZhangChampollion2018.World; renamed locally to avoid namespace ambiguity).

• uu : World

  A up, B up — actual world; light on.

• ud : World

  A up, B down — light off.

• du : World

  A down, B up — light off.

• dd : World

  A down, B down — light on.

@[implicit_reducible]

instance CiardelliZhangChampollion2018Lumping.instReprWorld : Repr World

Equations

• CiardelliZhangChampollion2018Lumping.instReprWorld = { reprPrec := CiardelliZhangChampollion2018Lumping.instReprWorld.repr }

def CiardelliZhangChampollion2018Lumping.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CiardelliZhangChampollion2018Lumping.instDecidableEqWorld : DecidableEq World

Equations

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

@[implicit_reducible]

instance CiardelliZhangChampollion2018Lumping.instPartialOrderWorld : PartialOrder World

Discrete partial order on worlds: s ≤ t ↔ s = t. (Worlds-only model — no proper sub-situations.)

Equations

• CiardelliZhangChampollion2018Lumping.instPartialOrderWorld = Intensional.discreteOrder CiardelliZhangChampollion2018Lumping.World

def CiardelliZhangChampollion2018Lumping.switchesSituationFrame : Intensional.SituationFrame

The switches frame promoted to a SituationFrame with discrete parthood.

Equations

• CiardelliZhangChampollion2018Lumping.switchesSituationFrame = { Entity := Unit, Index := CiardelliZhangChampollion2018Lumping.World, order := inferInstance }

Propositions

Truth-makers at the worlds-only level (every world supports its own positive facts; nothing else).

def CiardelliZhangChampollion2018Lumping.aUp : Set switchesSituationFrame.Index

"Switch A is up."

Equations

• CiardelliZhangChampollion2018Lumping.aUp = {CiardelliZhangChampollion2018Lumping.World.uu, CiardelliZhangChampollion2018Lumping.World.ud}

def CiardelliZhangChampollion2018Lumping.aDn : Set switchesSituationFrame.Index

"Switch A is down."

Equations

• CiardelliZhangChampollion2018Lumping.aDn = {CiardelliZhangChampollion2018Lumping.World.du, CiardelliZhangChampollion2018Lumping.World.dd}

def CiardelliZhangChampollion2018Lumping.bUp : Set switchesSituationFrame.Index

"Switch B is up."

Equations

• CiardelliZhangChampollion2018Lumping.bUp = {CiardelliZhangChampollion2018Lumping.World.uu, CiardelliZhangChampollion2018Lumping.World.du}

def CiardelliZhangChampollion2018Lumping.bDn : Set switchesSituationFrame.Index

"Switch B is down."

Equations

• CiardelliZhangChampollion2018Lumping.bDn = {CiardelliZhangChampollion2018Lumping.World.ud, CiardelliZhangChampollion2018Lumping.World.dd}

def CiardelliZhangChampollion2018Lumping.notBothUp : Set switchesSituationFrame.Index

"At least one switch is down" (= ¬(A ∧ B)).

Equations

• CiardelliZhangChampollion2018Lumping.notBothUp = {CiardelliZhangChampollion2018Lumping.World.ud, CiardelliZhangChampollion2018Lumping.World.du, CiardelliZhangChampollion2018Lumping.World.dd}

def CiardelliZhangChampollion2018Lumping.lightOn : Set switchesSituationFrame.Index

"The light is on" (per the wiring law, holds iff both switches in the same position).

Equations

• CiardelliZhangChampollion2018Lumping.lightOn = {CiardelliZhangChampollion2018Lumping.World.uu, CiardelliZhangChampollion2018Lumping.World.dd}

def CiardelliZhangChampollion2018Lumping.lightOff : Set switchesSituationFrame.Index

"The light is off."

Equations

• CiardelliZhangChampollion2018Lumping.lightOff = {CiardelliZhangChampollion2018Lumping.World.ud, CiardelliZhangChampollion2018Lumping.World.du}

Worlds (maximal situations)

Under the discrete order, every world is maximal.

theorem CiardelliZhangChampollion2018Lumping.all_isWorld (w : switchesSituationFrame.Index) : Intensional.IsWorld w

theorem CiardelliZhangChampollion2018Lumping.worlds_eq_univ : switchesSituationFrame.Worlds = Set.univ

The Crucial Set collapses to a singleton

For any antecedent p not true at uu and any non-empty Base Set Fw₀ ⊆ {q : Set World | uu ∈ q}, the discrete-parthood lumping closure forces every Crucial Set member containing one Fw element to contain all of them — and that union is inconsistent with p. So the only consistent lumping-closed Crucial Set member is {p} itself.

For our negative result we use Fw₀ = ∅, which trivializes the lumping closure further: the only Crucial Set member is {p} because there are no Fw elements to add.

def CiardelliZhangChampollion2018Lumping.Fw₀ : Set (Set switchesSituationFrame.Index)

Empty Base Set.

Equations

• CiardelliZhangChampollion2018Lumping.Fw₀ = ∅

theorem CiardelliZhangChampollion2018Lumping.crucialSet_empty_Fw_eq_singleton (p : Set switchesSituationFrame.Index) (hp : (switchesSituationFrame.Worlds ∩ p).Nonempty) : Semantics.Conditionals.PremiseSemantic.CrucialSet Fw₀ World.uu p = {{p}}

With an empty Base Set, the Crucial Set for any antecedent consistent at some world reduces to the singleton {antecedent}.

The asymmetric failure: lumping CF on the simple antecedents

The headline result. wouldCF Fw₀ uu aDn lightOff is false — empirically the wrong prediction. The reason: Follows {aDn} lightOff fails because the world dd satisfies aDn but not lightOff (both switches down means the light is on by the wiring).

theorem CiardelliZhangChampollion2018Lumping.follows_aDn_lightOff_fails : ¬Semantics.Conditionals.Counterfactual.Follows {aDn} lightOff

dd is an aDn-world where lightOff fails — the witness that breaks Follows {aDn} lightOff.

theorem CiardelliZhangChampollion2018Lumping.follows_bDn_lightOff_fails : ¬Semantics.Conditionals.Counterfactual.Follows {bDn} lightOff

The symmetric witness for bDn.

theorem CiardelliZhangChampollion2018Lumping.follows_notBothUp_lightOff_fails : ¬Semantics.Conditionals.Counterfactual.Follows {notBothUp} lightOff

And for notBothUp (¬(A ∧ B)) — dd blocks here too, this time correctly matching the empirics.

Witnesses of antecedent consistency (for the Crucial Set proofs)

The three headline theorems

Lumping CF (with empty Fw₀) predicts false for all three counterfactuals. The first two are empirically wrong (lumping's failure); the third is empirically right (lumping's lucky catch).

theorem CiardelliZhangChampollion2018Lumping.not_wouldCF_aDn_lightOff : ¬Semantics.Conditionals.PremiseSemantic.wouldCF Fw₀ World.uu aDn lightOff

Lumping CF wrongly predicts aDn > OFF false (empirically ~78% true). The dd-world (both switches down → light on) satisfies the antecedent but not the consequent, blocking the Follows step that the singleton Crucial Set demands.

theorem CiardelliZhangChampollion2018Lumping.not_wouldCF_bDn_lightOff : ¬Semantics.Conditionals.PremiseSemantic.wouldCF Fw₀ World.uu bDn lightOff

Lumping CF wrongly predicts bDn > OFF false (empirically ~76% true). Symmetric to the aDn case.

theorem CiardelliZhangChampollion2018Lumping.not_wouldCF_notBothUp_lightOff : ¬Semantics.Conditionals.PremiseSemantic.wouldCF Fw₀ World.uu notBothUp lightOff

Lumping CF correctly predicts ¬(A ∧ B) > OFF false (empirically ~20% true, i.e., not-true). Same structural reason as the simple cases — the dd-world blocks Follows.

The asymmetry, formally

Pulling the three predictions together with the CiardelliZhangChampollion2018 results: lumping and minimal-change operators fail on disjoint subsets of the switches counterfactuals.

theorem CiardelliZhangChampollion2018Lumping.lumping_failure_pattern : ¬Semantics.Conditionals.PremiseSemantic.wouldCF Fw₀ World.uu aDn lightOff ∧ ¬Semantics.Conditionals.PremiseSemantic.wouldCF Fw₀ World.uu notBothUp lightOff

Asymmetric failure: lumping CF and minimal-change CF have disjoint failure modes on switches. Lumping is wrong on the simple antecedents (this file's not_wouldCF_aDn_lightOff / not_wouldCF_bDn_lightOff); minimal-change is wrong on the disjunctive antecedent (CZC2018's notBothUp_off_at_uu predicts true, contrary to empirics).

Statement form: lumping CF predicts aDn > OFF false (empirically wrong), AND lumping CF predicts notBothUp > OFF false (empirically right). The contrast with minimal-change is that minimal-change predicts aDn > OFF true and notBothUp > OFF true; the empirics are true / false.