Sloman, Barbey and Hotaling (2009): A Causal Model Theory of Cause, Enable, and Prevent

This file formalizes the causal model theory of [SBH09]: the verbs refer to the causal model of a discourse, and in the deterministic binary case their meanings are the structural equations (2) to (4). A causes B asserts a link from A to B, B := A; A enables B asserts a link, an accessory variable also linked to B, and A necessary for B, B := A ∧ X; and A prevents B asserts a link along which A reduces B, B := ¬A with no accessory and B := ¬A ∧ X or B := ¬(A ∧ X) with one. The verbs are predicates on a causal model (Causes, Enables, Prevents), and the equations are models (causes, enables, prevents, preventsAnd, preventsNand) that satisfy them (causes_Causes, enables_Enables, prevents_Prevents, preventsAnd_Prevents, preventsNand_Prevents). The paper's experiments follow from the equations: an effect follows from its cause without any accessory, but from its enabler only once the accessory is settled (Experiments 1 to 3, causes_entails, enables_not_entails, enables_entails_of_accessory), and a one-link model is labelled cause while a two-link model is labelled enable (Experiment 4, not_enables_of_parents_eq_singleton, causes_not_Enables). Two-premise arguments are composed by substituting causes for effects, and the compositions the paper works out come out as the equations it names: causes then causes is C := A (causesCauses_causes), allows then prevents, or allows then not B causes C, is C := ¬(A ∧ X), the accessory form of prevents (allowsPrevents_prevents), prevents then prevents is C := A (preventsPrevents_causes), and the three-premise argument of section 4.2 composes to D := A (threePremise_causes).

Implementation notes

• A structural equation is a deterministic Boolean equation at the effect over its parents; the cause and the accessory variable are exogenous, read off the context. Entailment is strict causal entailment from an observation (CausalModel.CausallyEntails), on which an effect with an unsettled parent entails nothing: this is the paper's uncertainty when the accessory is unknown. Necessity is read in every context and under every intervention that leaves the effect open and turns the cause off: the effect is then off.
• The paper's experimental results stay in prose. In Experiments 1 to 3 confidence that the effect occurs was high only for a cause without an accessory and near the midpoint of the scale otherwise; in Experiment 4 one-link vignettes drew cause and two-link vignettes drew enable, help or allow. Of the sixteen two-premise argument forms of Goldvarg and Johnson-Laird's fourth experiment, the theory agrees with mental model theory on thirteen and predicts A prevents C for allows then prevents and for allows then not B causes C, and A causes C for prevents then prevents.

References

• [SBH09]
• [Pea09]

def SlomanBarbeyHotaling2009.Causes {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) (a b : V) : Prop

A causes B asserts a link from A to B.

Equations

• SlomanBarbeyHotaling2009.Causes M a b = M.graph.Adj a b

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableCausesOfDecidableRelAdjGraphBool {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [DecidableRel M.graph.Adj] (a b : V) : Decidable (Causes M a b)

Equations

• SlomanBarbeyHotaling2009.instDecidableCausesOfDecidableRelAdjGraphBool M a b = SlomanBarbeyHotaling2009.instDecidableCausesOfDecidableRelAdjGraphBool._aux_1 M a b

def SlomanBarbeyHotaling2009.Necessary {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (a b : V) : Prop

A is necessary for B when, in every context and under every intervention that leaves B open and turns A off, B is off.

Equations

• SlomanBarbeyHotaling2009.Necessary M a b = ∀ (u : U) (I : V → Flat Bool), I b = ⊥ → I a = ↑false → M.solve I u b = false

def SlomanBarbeyHotaling2009.Enables {U : Type u_1} {V : Type u_2} (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (a b : V) : Prop

A enables B asserts a link from A to B, an accessory variable also linked to B, and A necessary for B.

Equations

• SlomanBarbeyHotaling2009.Enables M a b = (M.graph.Adj a b ∧ (∃ (x : V), x ≠ a ∧ M.graph.Adj x b) ∧ SlomanBarbeyHotaling2009.Necessary M a b)

def SlomanBarbeyHotaling2009.Prevents {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (s : V → Flat Bool) (a b : V) : Prop

A prevents B on the observation s asserts a link from A to B along which A being on entails B off.

Equations

• SlomanBarbeyHotaling2009.Prevents M s a b = (M.graph.Adj a b ∧ M.CausallyEntails (Function.update s a ↑true) b false)

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidablePreventsOfInhabitedOfFintypeOfDecidableRelAdjGraphBool {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] [Fintype U] [Inhabited U] [Fintype V] [DecidableRel M.graph.Adj] (s : V → Flat Bool) (a b : V) : Decidable (Prevents M s a b)

Equations

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

def SlomanBarbeyHotaling2009.EqCauses {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (s : V → Flat Bool) (a c : V) : Prop

The model realizes c := a on the observation s.

Equations

• SlomanBarbeyHotaling2009.EqCauses M s a c = ∀ (v : Bool), M.CausallyEntails (Function.update s a ↑v) c v

def SlomanBarbeyHotaling2009.EqPrevents {U : Type u_1} {V : Type u_2} [DecidableEq V] (M : CausalModel U V fun (x : V) => Bool) [M.IsAcyclic] (s : V → Flat Bool) (a c : V) : Prop

The model realizes c := ¬a on the observation s.

Equations

• SlomanBarbeyHotaling2009.EqPrevents M s a c = ∀ (v : Bool), M.CausallyEntails (Function.update s a ↑v) c !v

theorem SlomanBarbeyHotaling2009.not_enables_of_forall_adj {U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {a b : V} (h : ∀ (x : V), M.graph.Adj x b → x = a) : ¬Enables M a b

Experiment 4: with A alone the source of B, the relation is not an enabling one.

theorem SlomanBarbeyHotaling2009.EqCauses.not_eqPrevents {U : Type u_1} {V : Type u_2} [DecidableEq V] {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] [Fintype U] [Inhabited U] [Fintype V] [DecidableRel M.graph.Adj] {s : V → Flat Bool} {a c : V} (h : EqCauses M s a c) : ¬EqPrevents M s a c

The equations c := a and c := ¬a exclude each other on an observation.

The equations of section 3

inductive SlomanBarbeyHotaling2009.V : Type

The cause, the accessory variable and the effect.

• A : V
• X : V
• B : V

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableEqV : DecidableEq V

Equations

• SlomanBarbeyHotaling2009.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instFintypeV : Fintype V

Equations

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

structure SlomanBarbeyHotaling2009.Context : Type

The context settles the cause A and the accessory X.

• A : Bool
• X : Bool

def SlomanBarbeyHotaling2009.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• SlomanBarbeyHotaling2009.instDecidableEqContext.decEq { A := a, X := a_1 } { A := b, X := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableEqContext : DecidableEq Context

Equations

• SlomanBarbeyHotaling2009.instDecidableEqContext = SlomanBarbeyHotaling2009.instDecidableEqContext.decEq

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instFintypeContext : Fintype Context

Equations

• SlomanBarbeyHotaling2009.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × Bool) SlomanBarbeyHotaling2009.Context.proxyTypeEquiv

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instInhabitedContext : Inhabited Context

Equations

• SlomanBarbeyHotaling2009.instInhabitedContext = { default := SlomanBarbeyHotaling2009.instInhabitedContext.default }

def SlomanBarbeyHotaling2009.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instReprContext : Repr Context

Equations

• SlomanBarbeyHotaling2009.instReprContext = { reprPrec := SlomanBarbeyHotaling2009.instReprContext.repr }

def SlomanBarbeyHotaling2009.oneLinkEdges : Finset (V × V)

B reads its only parent A.

Equations

• SlomanBarbeyHotaling2009.oneLinkEdges = {(SlomanBarbeyHotaling2009.V.A, SlomanBarbeyHotaling2009.V.B)}

def SlomanBarbeyHotaling2009.twoLinkEdges : Finset (V × V)

B reads A and the accessory X.

Equations

• SlomanBarbeyHotaling2009.twoLinkEdges = {(SlomanBarbeyHotaling2009.V.A, SlomanBarbeyHotaling2009.V.B), (SlomanBarbeyHotaling2009.V.X, SlomanBarbeyHotaling2009.V.B)}

def SlomanBarbeyHotaling2009.oneLinkModel (f : Bool → Bool) : CausalModel Context V fun (x : V) => Bool

A one-link model with the given equation at B, B's only parent being A.

Equations

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

def SlomanBarbeyHotaling2009.twoLinkModel (f : Bool → Bool → Bool) : CausalModel Context V fun (x : V) => Bool

A two-link model with the given equation at B over A and the accessory X.

Equations

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

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolOneLinkModel (f : Bool → Bool) : DecidableRel (oneLinkModel f).graph.Adj

Equations

• SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolOneLinkModel f w v = SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolOneLinkModel._aux_1 f w v

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolTwoLinkModel (f : Bool → Bool → Bool) : DecidableRel (twoLinkModel f).graph.Adj

Equations

• SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolTwoLinkModel f w v = SlomanBarbeyHotaling2009.instDecidableRelVAdjGraphContextBoolTwoLinkModel._aux_1 f w v

instance SlomanBarbeyHotaling2009.instIsAcyclicContextVBoolOneLinkModel (f : Bool → Bool) : (oneLinkModel f).IsAcyclic

instance SlomanBarbeyHotaling2009.instIsAcyclicContextVBoolTwoLinkModel (f : Bool → Bool → Bool) : (twoLinkModel f).IsAcyclic

@[reducible, inline]

abbrev SlomanBarbeyHotaling2009.causes : CausalModel Context V fun (x : V) => Bool

(2) A causes B: B := A.

Equations

• SlomanBarbeyHotaling2009.causes = SlomanBarbeyHotaling2009.oneLinkModel id

@[reducible, inline]

abbrev SlomanBarbeyHotaling2009.enables : CausalModel Context V fun (x : V) => Bool

(3) A enables B: B := A ∧ X.

Equations

• SlomanBarbeyHotaling2009.enables = SlomanBarbeyHotaling2009.twoLinkModel fun (x1 x2 : Bool) => x1 && x2

@[reducible, inline]

abbrev SlomanBarbeyHotaling2009.prevents : CausalModel Context V fun (x : V) => Bool

(4a) A prevents B with no accessory: B := ¬A.

Equations

• SlomanBarbeyHotaling2009.prevents = SlomanBarbeyHotaling2009.oneLinkModel fun (x : Bool) => !x

@[reducible, inline]

abbrev SlomanBarbeyHotaling2009.preventsAnd : CausalModel Context V fun (x : V) => Bool

(4b) A prevents B with an accessory: B := ¬A ∧ X.

Equations

• SlomanBarbeyHotaling2009.preventsAnd = SlomanBarbeyHotaling2009.twoLinkModel fun (a x : Bool) => !a && x

@[reducible, inline]

abbrev SlomanBarbeyHotaling2009.preventsNand : CausalModel Context V fun (x : V) => Bool

(4c) A prevents B with an accessory: B := ¬(A ∧ X).

Equations

• SlomanBarbeyHotaling2009.preventsNand = SlomanBarbeyHotaling2009.twoLinkModel fun (a x : Bool) => !(a && x)

def SlomanBarbeyHotaling2009.accessory : V → Flat Bool

The accessory present.

Equations

• SlomanBarbeyHotaling2009.accessory = Function.update ⊥ SlomanBarbeyHotaling2009.V.X ↑true

theorem SlomanBarbeyHotaling2009.causes_Causes : Causes causes V.A V.B ∧ EqCauses causes ⊥ V.A V.B

A causes B holds of (2), and the model realizes B := A.

theorem SlomanBarbeyHotaling2009.causes_entails : causes.CausallyEntails (Function.update ⊥ V.A ↑true) V.B true

Experiments 2 and 3: from A causes B and A, B follows with no accessory settled.

theorem SlomanBarbeyHotaling2009.causes_not_Enables : ¬Enables causes V.A V.B

Experiment 4: the one-link model is not an enabling relation.

theorem SlomanBarbeyHotaling2009.enables_Enables : Enables enables V.A V.B

A enables B holds of (3), which has the link, the accessory, and the necessity of A, B being the conjunction of A and X.

theorem SlomanBarbeyHotaling2009.enables_not_entails : ¬enables.CausallyEntails (Function.update ⊥ V.A ↑true) V.B true

Experiments 1 and 3: from A enables B and A alone, B does not follow, the accessory being unknown.

theorem SlomanBarbeyHotaling2009.enables_entails_of_accessory : enables.CausallyEntails (Function.update accessory V.A ↑true) V.B true

With the accessory present, B follows from A.

theorem SlomanBarbeyHotaling2009.prevents_Prevents : Prevents prevents ⊥ V.A V.B ∧ EqPrevents prevents ⊥ V.A V.B

(4a) prevents: turning A on entails B off.

theorem SlomanBarbeyHotaling2009.preventsAnd_Prevents : Prevents preventsAnd accessory V.A V.B ∧ EqPrevents preventsAnd accessory V.A V.B

(4b) and (4c) prevent when the accessory is present, and (4b) does so as the equation B := ¬A on that observation.

theorem SlomanBarbeyHotaling2009.preventsNand_Prevents : Prevents preventsNand accessory V.A V.B ∧ EqPrevents preventsNand accessory V.A V.B

Two-premise arguments, section 4.1

The premises A relates to B and B relates to C are structural equations, and the conclusion is their composition, substituting the cause for the effect; the conclusion is the equation the composed model realizes between A and C.

inductive SlomanBarbeyHotaling2009.W : Type

The terms of a two-premise argument, with the first premise's accessory.

• A : W
• X : W
• B : W
• C : W

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableEqW : DecidableEq W

Equations

• SlomanBarbeyHotaling2009.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instFintypeW : Fintype W

Equations

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

def SlomanBarbeyHotaling2009.composeOneEdges : Finset (W × W)

B reads A, and C reads B.

Equations

• SlomanBarbeyHotaling2009.composeOneEdges = {(SlomanBarbeyHotaling2009.W.A, SlomanBarbeyHotaling2009.W.B), (SlomanBarbeyHotaling2009.W.B, SlomanBarbeyHotaling2009.W.C)}

def SlomanBarbeyHotaling2009.composeTwoEdges : Finset (W × W)

B reads A and the accessory X, and C reads B.

Equations

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

def SlomanBarbeyHotaling2009.composeOne (f g : Bool → Bool) : CausalModel Context W fun (x : W) => Bool

The composition of a first premise B := f A with a second premise C := g B.

Equations

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

def SlomanBarbeyHotaling2009.composeTwo (f : Bool → Bool → Bool) (g : Bool → Bool) : CausalModel Context W fun (x : W) => Bool

The composition of a first premise B := f A X with a second premise C := g B.

Equations

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

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeOne (f g : Bool → Bool) : DecidableRel (composeOne f g).graph.Adj

Equations

• SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeOne f g w v = SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeOne._aux_1 f g w v

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeTwo (f : Bool → Bool → Bool) (g : Bool → Bool) : DecidableRel (composeTwo f g).graph.Adj

Equations

• SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeTwo f g w v = SlomanBarbeyHotaling2009.instDecidableRelWAdjGraphContextBoolComposeTwo._aux_1 f g w v

instance SlomanBarbeyHotaling2009.instIsAcyclicContextWBoolComposeOne (f g : Bool → Bool) : (composeOne f g).IsAcyclic

instance SlomanBarbeyHotaling2009.instIsAcyclicContextWBoolComposeTwo (f : Bool → Bool → Bool) (g : Bool → Bool) : (composeTwo f g).IsAcyclic

def SlomanBarbeyHotaling2009.chainAccessory : W → Flat Bool

The first premise's accessory present.

Equations

• SlomanBarbeyHotaling2009.chainAccessory = Function.update ⊥ SlomanBarbeyHotaling2009.W.X ↑true

theorem SlomanBarbeyHotaling2009.causesCauses_causes : EqCauses (composeOne id id) ⊥ W.A W.C

(5) and (6): A causes B, B causes C compose to C := A, the conclusion A causes C.

theorem SlomanBarbeyHotaling2009.allowsPrevents_prevents : EqPrevents (composeTwo (fun (x1 x2 : Bool) => x1 && x2) fun (x : Bool) => !x) chainAccessory W.A W.C

A allows B, B prevents C, or equally not B causes C, compose to C := ¬(A ∧ X), the accessory form (4c) of prevents: with the accessory present, A prevents C.

theorem SlomanBarbeyHotaling2009.preventsPrevents_causes : EqCauses (composeOne (fun (x : Bool) => !x) fun (x : Bool) => !x) ⊥ W.A W.C

A prevents B, B prevents C compose to C := A, the conclusion A causes C.

A three-premise argument, section 4.2

inductive SlomanBarbeyHotaling2009.T : Type

The terms of the three-premise argument.

• A : T
• B : T
• C : T
• D : T

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableEqT : DecidableEq T

Equations

• SlomanBarbeyHotaling2009.instDecidableEqT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instFintypeT : Fintype T

Equations

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

def SlomanBarbeyHotaling2009.threePremiseEdges : Finset (T × T)

B reads A, C reads B, and D reads C.

Equations

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

structure SlomanBarbeyHotaling2009.ThreePremiseContext : Type

The context of the three-premise argument settles A.

• A : Bool

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableEqThreePremiseContext : DecidableEq ThreePremiseContext

Equations

• SlomanBarbeyHotaling2009.instDecidableEqThreePremiseContext = SlomanBarbeyHotaling2009.instDecidableEqThreePremiseContext.decEq

def SlomanBarbeyHotaling2009.instDecidableEqThreePremiseContext.decEq (x✝ x✝¹ : ThreePremiseContext) : Decidable (x✝ = x✝¹)

Equations

• SlomanBarbeyHotaling2009.instDecidableEqThreePremiseContext.decEq { A := a } { A := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instFintypeThreePremiseContext : Fintype ThreePremiseContext

Equations

• SlomanBarbeyHotaling2009.instFintypeThreePremiseContext = Fintype.ofEquiv Bool SlomanBarbeyHotaling2009.ThreePremiseContext.proxyTypeEquiv

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instInhabitedThreePremiseContext : Inhabited ThreePremiseContext

Equations

• SlomanBarbeyHotaling2009.instInhabitedThreePremiseContext = { default := SlomanBarbeyHotaling2009.instInhabitedThreePremiseContext.default }

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instReprThreePremiseContext : Repr ThreePremiseContext

Equations

• SlomanBarbeyHotaling2009.instReprThreePremiseContext = { reprPrec := SlomanBarbeyHotaling2009.instReprThreePremiseContext.repr }

def SlomanBarbeyHotaling2009.instReprThreePremiseContext.repr : ThreePremiseContext → ℕ → Std.Format

Equations

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

def SlomanBarbeyHotaling2009.threePremise : CausalModel ThreePremiseContext T fun (x : T) => Bool

The premises A causes B, B causes not C and C causes not D are B := A, C := ¬B and D := ¬C.

Equations

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

@[instance_reducible]

instance SlomanBarbeyHotaling2009.instDecidableRelTAdjGraphThreePremiseContextBoolThreePremise : DecidableRel threePremise.graph.Adj

Equations

• SlomanBarbeyHotaling2009.instDecidableRelTAdjGraphThreePremiseContextBoolThreePremise w v = SlomanBarbeyHotaling2009.instDecidableRelTAdjGraphThreePremiseContextBoolThreePremise._aux_1 w v

instance SlomanBarbeyHotaling2009.instIsAcyclicThreePremiseContextTBoolThreePremise : threePremise.IsAcyclic

theorem SlomanBarbeyHotaling2009.threePremise_causes : EqCauses threePremise ⊥ T.A T.D

The three premises compose to D := A, the conclusion A causes D.