@cite{konuk-et-al-2026}: Plural Causes

@cite{konuk-et-al-2026}

Formalizes Konuk, Quillien & Mascarenhas (2026) "Plural causes," Open Mind.

Core Contributions

1. Compound causes: A∧B is treated as a single compound binary variable for causal selection, not decomposed into individual contributions.
2. Necessity-Sufficiency Model (NSM): NSM(C) = P(C)·Suf(C) + (1-P(C))·Nec(C) from @cite{icard-et-al-2017}, applied to compound causes.
3. Anti-linearity: NSM(INT∧HIGH) > NSM(LOW∧INT) even though LOW and HIGH have comparable individual causal strength (Experiment 1).
4. Homogeneous loss: Loss judgments follow LOSS_strong = ¬A∧¬B∧¬C∧¬D, not classical ¬((A∧B)∨(C∧D)) (Experiment 2), mixed with classical via fitted parameter w ≈ 0.77.
5. Crossing avoidance: Within-disjunct plural causes (A∧B) preferred over cross-disjunct (A∧C) when the rule is (A∧B)∨(C∧D) (Experiment 2).

V2 substrate

The two scenarios (threshold game + disjunctive rule) share a single KonukVar inductive enum (9 vertices). Each scenario's win-vertex mechanism is a Boolean function of its parents (threshold-≥-2 for win; (A∧B)∨(C∧D) for exp2Win). Compound sufficiency/necessity are polymorphic predicates over BoolSEM defined via developDetOn with the explicit vertex list.

inductive KonukEtAl2026.KonukVar : Type

All vertices used by both Konuk experiments.

• urnA : KonukVar
• urnB : KonukVar
• urnC : KonukVar
• win : KonukVar
• exp2A : KonukVar
• exp2B : KonukVar
• exp2C : KonukVar
• exp2D : KonukVar
• exp2Win : KonukVar

@[implicit_reducible]

instance KonukEtAl2026.instDecidableEqKonukVar : DecidableEq KonukVar

Equations

• KonukEtAl2026.instDecidableEqKonukVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KonukEtAl2026.instFintypeKonukVar : Fintype KonukVar

Equations

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

@[implicit_reducible]

instance KonukEtAl2026.instReprKonukVar : Repr KonukVar

Equations

• KonukEtAl2026.instReprKonukVar = { reprPrec := KonukEtAl2026.instReprKonukVar.repr }

def KonukEtAl2026.instReprKonukVar.repr : KonukVar → ℕ → Std.Format

Equations

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

def KonukEtAl2026.konukGraph : Core.Causal.CausalGraph KonukVar

The shared causal graph for both experiments.

Equations

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

noncomputable def KonukEtAl2026.konukSEM : Core.Causal.BoolSEM KonukVar

The shared BoolSEM for both Konuk experiments.

Equations

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

@[implicit_reducible]

noncomputable instance KonukEtAl2026.instIsDeterministicKonukVarBoolKonukSEM : Core.Causal.SEM.IsDeterministic konukSEM

Equations

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

def KonukEtAl2026.konukVarList : List KonukVar

Topologically-ordered vertex list (roots before win-vertices).

Equations

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

noncomputable def KonukEtAl2026.compoundSufficient (M : Core.Causal.BoolSEM KonukVar) [Core.Causal.SEM.IsDeterministic M] (bg : Core.Causal.Valuation fun (x : KonukVar) => Bool) (causes : List KonukVar) (effect : KonukVar) : Prop

A compound cause is sufficient iff setting all its variables to true produces the effect under developDetOn.

Equations

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

@[implicit_reducible]

noncomputable instance KonukEtAl2026.instDecidableCompoundSufficient (M : Core.Causal.BoolSEM KonukVar) [Core.Causal.SEM.IsDeterministic M] (bg : Core.Causal.Valuation fun (x : KonukVar) => Bool) (causes : List KonukVar) (effect : KonukVar) : Decidable (compoundSufficient M bg causes effect)

Equations

• KonukEtAl2026.instDecidableCompoundSufficient M bg causes effect = Classical.dec (KonukEtAl2026.compoundSufficient M bg causes effect)

noncomputable def KonukEtAl2026.compoundNecessary (M : Core.Causal.BoolSEM KonukVar) [Core.Causal.SEM.IsDeterministic M] (bg : Core.Causal.Valuation fun (x : KonukVar) => Bool) (causes : List KonukVar) (effect : KonukVar) : Prop

A compound cause is necessary iff setting all its variables to false prevents the effect under developDetOn.

Equations

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

@[implicit_reducible]

noncomputable instance KonukEtAl2026.instDecidableCompoundNecessary (M : Core.Causal.BoolSEM KonukVar) [Core.Causal.SEM.IsDeterministic M] (bg : Core.Causal.Valuation fun (x : KonukVar) => Bool) (causes : List KonukVar) (effect : KonukVar) : Decidable (compoundNecessary M bg causes effect)

Equations

• KonukEtAl2026.instDecidableCompoundNecessary M bg causes effect = Classical.dec (KonukEtAl2026.compoundNecessary M bg causes effect)

theorem KonukEtAl2026.anyPair_sufficient_AB : compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.urnA, KonukVar.urnB] KonukVar.win

Any pair of urns is sufficient (compound sufficiency).

theorem KonukEtAl2026.anyPair_sufficient_AC : compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.urnA, KonukVar.urnC] KonukVar.win

theorem KonukEtAl2026.anyPair_sufficient_BC : compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.urnB, KonukVar.urnC] KonukVar.win

theorem KonukEtAl2026.compound_pair_necessary_in_actual : compoundNecessary konukSEM KonukEtAl2026.thresholdActual✝ [KonukVar.urnA, KonukVar.urnB] KonukVar.win ∧ compoundNecessary konukSEM KonukEtAl2026.thresholdActual✝ [KonukVar.urnA, KonukVar.urnC] KonukVar.win ∧ compoundNecessary konukSEM KonukEtAl2026.thresholdActual✝ [KonukVar.urnB, KonukVar.urnC] KonukVar.win

But compound pairs ARE necessary in the actual world.

Individual urns are not necessary (overdetermination), but compound pairs are — removing any pair drops below threshold. This justifies treating A∧B as the unit of causal attribution.

def KonukEtAl2026.pLow : ℚ

Equations

• KonukEtAl2026.pLow = 1 / 20

def KonukEtAl2026.pInt : ℚ

Equations

• KonukEtAl2026.pInt = 1 / 2

def KonukEtAl2026.pHigh : ℚ

Equations

• KonukEtAl2026.pHigh = 19 / 20

def KonukEtAl2026.nsmThreshold (pX pY pZ : ℚ) : ℚ

NSM for a compound pair {X,Y} in the threshold-≥-2 game (Suf=1).

NSM = 1 - P(WIN ∧ ¬C), where P(WIN ∧ ¬C) is the probability that exactly one of {X,Y} is on AND the third urn Z is also on.

Equations

• KonukEtAl2026.nsmThreshold pX pY pZ = 1 - (pX * (1 - pY) + (1 - pX) * pY) * pZ

theorem KonukEtAl2026.nsm_intHigh : nsmThreshold pInt pHigh pLow = 39 / 40

NSM({INT, HIGH}) = 39/40.

theorem KonukEtAl2026.nsm_lowInt : nsmThreshold pLow pInt pHigh = 21 / 40

NSM({LOW, INT}) = 21/40.

theorem KonukEtAl2026.antiLinearity_nsm : nsmThreshold pInt pHigh pLow > nsmThreshold pLow pInt pHigh

Anti-linearity: INT∧HIGH has strictly higher NSM than LOW∧INT.

The additive hypothesis predicts LOW∧INT ≈ INT∧HIGH (since LOW and HIGH have comparable individual NSM in the threshold game). The holistic NSM gives 39/40 vs 21/40, matching the empirical finding.

def KonukEtAl2026.lossClassical (a b c d : Bool) : Bool

Classical LOSS = ¬((A∧B) ∨ (C∧D)) ≡ ¬(A∧B) ∧ ¬(C∧D).

Equations

• KonukEtAl2026.lossClassical a b c d = (!(a && b) && !(c && d))

def KonukEtAl2026.lossStrong (a b c d : Bool) : Bool

Homogeneous LOSS = ¬A ∧ ¬B ∧ ¬C ∧ ¬D.

Equations

• KonukEtAl2026.lossStrong a b c d = (!a && !b && !c && !d)

theorem KonukEtAl2026.lossStrong_implies_classical (a b c d : Bool) : lossStrong a b c d = true → lossClassical a b c d = true

LOSS_strong entails classical LOSS.

theorem KonukEtAl2026.lossStrong_strictly_stronger : ∃ (a : Bool) (b : Bool) (c : Bool) (d : Bool), lossClassical a b c d = true ∧ lossStrong a b c d = false

Classical LOSS does NOT entail LOSS_strong.

Witness: A=1, B=0, C=0, D=0 — neither A∧B nor C∧D holds (classical LOSS), but A is present (LOSS_strong fails).

def KonukEtAl2026.lossMixed (w : ℚ) (a b c d : Bool) : ℚ

Mixture model: w · LOSS_strong + (1-w) · LOSS_classical.

Fitted w ≈ 0.77, reflecting the dominance of the homogeneous reading over the classical reading.

Equations

• KonukEtAl2026.lossMixed w a b c d = (w * if KonukEtAl2026.lossStrong a b c d = true then 1 else 0) + (1 - w) * if KonukEtAl2026.lossClassical a b c d = true then 1 else 0

theorem KonukEtAl2026.lossMixed_at_one (a b c d : Bool) : lossMixed 1 a b c d = if lossStrong a b c d = true then 1 else 0

At w = 1, the mixture reduces to LOSS_strong.

theorem KonukEtAl2026.lossMixed_at_zero (a b c d : Bool) : lossMixed 0 a b c d = if lossClassical a b c d = true then 1 else 0

At w = 0, the mixture reduces to classical LOSS.

theorem KonukEtAl2026.loss_gap_iff_pluralGap (f : Fin 4 → Bool) : lossClassical (f 0) (f 1) (f 2) (f 3) = true ∧ lossStrong (f 0) (f 1) (f 2) (f 3) = false ↔ lossClassical (f 0) (f 1) (f 2) (f 3) = true ∧ Semantics.Plurality.Distributivity.someSatisfy (fun (i : Fin 4) (x : Unit) => f i = true) Finset.univ () = (true = true)

The loss gap (classical but not strong) is exactly someSatisfy for the "is present" predicate: some but not all variables are false.

The classical negation ¬(A∧B) ∧ ¬(C∧D) allows worlds where some variables are true and others false. The homogeneous negation ¬A∧¬B∧¬C∧¬D requires all false. The gap is the truth-value gap from @cite{kriz-spector-2021}.

inductive KonukEtAl2026.DisjunctMembership : Type

Disjunct membership classification for a pair of variables.

• withinAB : DisjunctMembership
• withinCD : DisjunctMembership
• crossDisjunct : DisjunctMembership

@[implicit_reducible]

instance KonukEtAl2026.instDecidableEqDisjunctMembership : DecidableEq DisjunctMembership

Equations

• KonukEtAl2026.instDecidableEqDisjunctMembership x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KonukEtAl2026.instReprDisjunctMembership : Repr DisjunctMembership

Equations

• KonukEtAl2026.instReprDisjunctMembership = { reprPrec := KonukEtAl2026.instReprDisjunctMembership.repr }

def KonukEtAl2026.instReprDisjunctMembership.repr : DisjunctMembership → ℕ → Std.Format

Equations

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

def KonukEtAl2026.classifyPair (i j : Fin 4) : DisjunctMembership

Classify a pair of Experiment 2 variables by disjunct membership.

Equations

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

theorem KonukEtAl2026.ab_within : classifyPair 0 1 = DisjunctMembership.withinAB

theorem KonukEtAl2026.cd_within : classifyPair 2 3 = DisjunctMembership.withinCD

theorem KonukEtAl2026.ac_cross : classifyPair 0 2 = DisjunctMembership.crossDisjunct

theorem KonukEtAl2026.bd_cross : classifyPair 1 3 = DisjunctMembership.crossDisjunct

theorem KonukEtAl2026.structural_crossing_avoidance : compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.exp2A, KonukVar.exp2B] KonukVar.exp2Win ∧ compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.exp2C, KonukVar.exp2D] KonukVar.exp2Win ∧ ¬compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.exp2A, KonukVar.exp2C] KonukVar.exp2Win ∧ ¬compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.exp2B, KonukVar.exp2D] KonukVar.exp2Win

Structural crossing avoidance: within-disjunct compound {A,B} is sufficient for WIN, but cross-disjunct compound {A,C} is NOT.

A∧B matches a conjunctive law, so setting A=B=1 fires the law and produces WIN. But A∧C does not match any single law.

theorem KonukEtAl2026.triple1_AB_sufficient_and_necessary : compoundSufficient konukSEM Core.Causal.Valuation.empty [KonukVar.exp2A, KonukVar.exp2B] KonukVar.exp2Win ∧ compoundNecessary konukSEM KonukEtAl2026.triple1Actual✝ [KonukVar.exp2A, KonukVar.exp2B] KonukVar.exp2Win

In Triple-1, the compound A∧B is both sufficient (in empty bg) and necessary (in actual world).

theorem KonukEtAl2026.triple0_lossStrong_needs_all : lossStrong false false true false = false ∧ lossStrong false false false false = true

In Triple-0 (loss), under homogeneous representation LOSS = ¬A∧¬B∧¬D, the white ball from D is indispensable.

theorem KonukEtAl2026.lossStrong_iff_allFalse (f : Fin 4 → Bool) : lossStrong (f 0) (f 1) (f 2) (f 3) = true ↔ ∀ (i : Fin 4), f i = false

LOSS_strong holds iff every individual variable is false.

theorem KonukEtAl2026.lossStrong_eq_noneSatisfy (f : Fin 4 → Bool) : (lossStrong (f 0) (f 1) (f 2) (f 3) = true) = Semantics.Plurality.Distributivity.noneSatisfy (fun (i : Fin 4) (x : Unit) => f i = true) Finset.univ ()

LOSS_strong is exactly noneSatisfy from @cite{kriz-spector-2021}.