Sloman, Barbey & Hotaling (2009): A Causal Model Theory of cause/enable/prevent

@cite{sloman-barbey-hotaling-2009}

Cognitive Science 33(1): 21–50.

The foundational deterministic-binary statement of the structural-equation theory of causal verbs: cause, enable, and prevent denote distinct structural forms (Figure 4, eqs 2, 3, 4a–c). Subsequent literature has generalized this to graded/probabilistic causation (@cite{cao-white-lassiter-2025}), counterfactual simulation (@cite{beller-gerstenberg-2025}), and refined necessity definitions (@cite{nadathur-2024}). This file formalizes SBH 2009's specific structural claims as the historical foundation.

What is formalized

1. The structural predicates Sloman.causeSem and Sloman.enableSem. These are paper-specific predicates over the SEM's graph shape (parent-set cardinality), not over develop — purely structural, computable, decidable.

2. Experiment 4 (Labeling): SBH's most testable production claim: 1-link causal models are labeled "cause"; 2-link models (with an accessory) are labeled "enable". Theorems oneLink_excludes_enable and twoLink_implies_enable formalize the structural distinction.

3. Distinctness theorem witnessing that the SBH-style enable predicate is structurally distinct from the simple cause predicate (the disagreement with force-dynamic accounts that collapse them becomes theorem-provable).

What is NOT formalized

• Multi-premise inference (§4–§9): SBH's substitution composition has been superseded by counterfactual simulation (@cite{beller-gerstenberg-2025}).
• Experiments 1–3 (certainty inequalities): graded SUF / Bayesian models predict these directly; deterministic SBH has no graded analogue (see @cite{cao-white-lassiter-2025}).
• Truth-conditional enableSem over develop: the structural predicate is the contemporary view; the develop-based version (with required-accessory truth conditions) reduces to a special case.

Mathlib pattern

This study file demonstrates the V2 migration pattern: paper-specific predicates live in the study file (namespaced Sloman); they reference V2's BoolSEM / CausalGraph directly without going through legacy hubs. Structural predicates avoid the develop noncomputable cascade.

def SlomanBarbeyHotaling2009.Sloman.causeSem {V : Type u_1} (M : Core.Causal.BoolSEM V) (cause effect : V) : Prop

SBH eq (2): B := A — Sloman's structural cause predicate. The effect has exactly one parent (the cause).

Equations

• SlomanBarbeyHotaling2009.Sloman.causeSem M cause effect = (M.graph.parents effect = {cause})

@[implicit_reducible]

instance SlomanBarbeyHotaling2009.Sloman.instDecidableCauseSemOfDecidableEq {V : Type u_1} [DecidableEq V] (M : Core.Causal.BoolSEM V) (cause effect : V) : Decidable (causeSem M cause effect)

Equations

• SlomanBarbeyHotaling2009.Sloman.instDecidableCauseSemOfDecidableEq M cause effect = SlomanBarbeyHotaling2009.Sloman.instDecidableCauseSemOfDecidableEq._aux_1 M cause effect

def SlomanBarbeyHotaling2009.Sloman.enableSem {V : Type u_1} (M : Core.Causal.BoolSEM V) (cause effect : V) : Prop

SBH eq (3): B := A ∧ X — Sloman's structural enable predicate. The effect has at least two parents, including the cause. The "accessory variable" (Sloman's X) is the second-or-later parent.

Equations

• SlomanBarbeyHotaling2009.Sloman.enableSem M cause effect = (cause ∈ M.graph.parents effect ∧ 2 ≤ (M.graph.parents effect).card)

@[implicit_reducible]

instance SlomanBarbeyHotaling2009.Sloman.instDecidableEnableSemOfDecidableEq {V : Type u_1} [DecidableEq V] (M : Core.Causal.BoolSEM V) (cause effect : V) : Decidable (enableSem M cause effect)

Equations

• SlomanBarbeyHotaling2009.Sloman.instDecidableEnableSemOfDecidableEq M cause effect = SlomanBarbeyHotaling2009.Sloman.instDecidableEnableSemOfDecidableEq._aux_1 M cause effect

theorem SlomanBarbeyHotaling2009.oneLink_causeSem_excludes_enableSem {V : Type u_1} [DecidableEq V] {M : Core.Causal.BoolSEM V} {cause effect : V} (h : M.graph.parents effect = {cause}) : Sloman.causeSem M cause effect ∧ ¬Sloman.enableSem M cause effect

Exp 4 / 1-link: 1-link causal models satisfy causeSem and exclude enableSem. Maps SBH's empirical finding "participants label 1-link models as 'cause'" to a definitional fact about the structural form.

theorem SlomanBarbeyHotaling2009.twoLink_enableSem_excludes_causeSem {V : Type u_1} [DecidableEq V] {M : Core.Causal.BoolSEM V} {cause accessory effect : V} (h_ne : cause ≠ accessory) (h : M.graph.parents effect = {cause, accessory}) : Sloman.enableSem M cause effect ∧ ¬Sloman.causeSem M cause effect

Exp 4 / 2-link: 2-link causal models (with a distinct accessory) satisfy enableSem and exclude causeSem. Maps SBH's empirical finding "participants label 2-link models as 'enable'" to a definitional fact about the structural form.

theorem SlomanBarbeyHotaling2009.causeSem_excludes_enableSem {V : Type u_1} [DecidableEq V] (M : Core.Causal.BoolSEM V) (cause effect : V) : ¬(Sloman.causeSem M cause effect ∧ Sloman.enableSem M cause effect)

causeSem and enableSem are mutually exclusive.

No BoolSEM simultaneously satisfies both predicates for the same cause/effect pair. The structural disagreement Sloman et al. argue against force-dynamic accounts (which collapse cause/enable truth-conditionally) becomes a theorem.

Witness: the parent-set cardinality is 1 for causeSem but ≥ 2 for enableSem.