Lewis (1973): Causation

This file formalizes the counterfactual analysis of causation of [Lew73a] on deterministic Boolean structural equation models. An event depends causally on another when, had the cause not occurred, the effect would not have occurred (lewisButFor, lewisDependence), and causation is the ancestral of causal dependence, a chain of stepwise dependences (lewisCausation, via Relation.TransGen). Four scenarios exercise the analysis: a single cause, a chain, in which the distal cause is a cause through two steps (Chain.chain_causation), the common-cause case of the barometer and the storm, where neither effect depends on the other (Epiphenomena.barometer_not_causes_storm), and symmetric overdetermination, where neither of two sufficient causes passes the but-for test (Overdetermination.overdetermination_no_dependence_a), the limitation the paper concedes.

Implementation notes

The actual world is a context of a causal model, and the counterfactual is an intervention setting the cause to false in that context (CausalModel.solve), so the analysis is the but-for test of the model rather than a similarity ordering over worlds; the two agree on these deterministic scenarios. The paper's treatment of preemption is not represented.

References

• [Lew73a]

def Lewis1973.lewisButFor {U : Type u_1} {W : Type u_2} [DecidableEq W] (M : CausalModel U W fun (x : W) => Bool) [M.IsAcyclic] (u : U) (cause effect : W) : Prop

The but-for counterfactual holds when, had the cause not occurred, the effect would not have occurred, the counterfactual being an intervention setting the cause to false in the actual context u.

Equations

• Lewis1973.lewisButFor M u cause effect = (M.solve (Function.update ⊥ cause ↑false) u effect ≠ true)

def Lewis1973.lewisDependence {U : Type u_1} {W : Type u_2} [DecidableEq W] (M : CausalModel U W fun (x : W) => Bool) [M.IsAcyclic] (u : U) (cause effect : W) : Prop

The effect depends causally on the cause (p. 562) when both occur and the effect would not have occurred without the cause.

Equations

• Lewis1973.lewisDependence M u cause effect = (M.solve ⊥ u cause = true ∧ M.solve ⊥ u effect = true ∧ Lewis1973.lewisButFor M u cause effect)

@[instance_reducible]

noncomputable instance Lewis1973.instDecidableLewisButForOfFintype {U : Type u_1} {W : Type u_2} [DecidableEq W] (M : CausalModel U W fun (x : W) => Bool) [M.IsAcyclic] (u : U) [Fintype W] (cause effect : W) : Decidable (lewisButFor M u cause effect)

Equations

• Lewis1973.instDecidableLewisButForOfFintype M u cause effect = { decide := !decide (M.solve (Function.update ⊥ cause ↑false) u effect = true), reflects_decide := ⋯ }

@[instance_reducible]

noncomputable instance Lewis1973.instDecidableLewisDependenceOfFintype {U : Type u_1} {W : Type u_2} [DecidableEq W] (M : CausalModel U W fun (x : W) => Bool) [M.IsAcyclic] (u : U) [Fintype W] (cause effect : W) : Decidable (lewisDependence M u cause effect)

Equations

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

def Lewis1973.lewisCausation {U : Type u_1} {W : Type u_2} [DecidableEq W] (M : CausalModel U W fun (x : W) => Bool) [M.IsAcyclic] (u : U) (cause effect : W) : Prop

Causation is the ancestral of causal dependence (p. 563).

Equations

• Lewis1973.lewisCausation M u cause effect = Relation.TransGen (Lewis1973.lewisDependence M u) cause effect

theorem Lewis1973.dependence_implies_causation {U : Type u_1} {W : Type u_2} [DecidableEq W] {M : CausalModel U W fun (x : W) => Bool} [M.IsAcyclic] {u : U} {cause effect : W} (h : lewisDependence M u cause effect) : lewisCausation M u cause effect

Causal dependence is causation through a chain of one step.

theorem Lewis1973.not_lewisDependence_of_not_reflTransGen {U : Type u_1} {W : Type u_2} [DecidableEq W] {M : CausalModel U W fun (x : W) => Bool} [M.IsAcyclic] {u : U} {cause effect : W} (h : ¬Relation.ReflTransGen M.graph.Adj cause effect) : ¬lewisDependence M u cause effect

An effect does not depend on an event from which no directed path reaches it, since intervening on the event leaves the effect as it was.

inductive Lewis1973.SimpleCause.V : Type

• a : V
• b : V

@[instance_reducible]

instance Lewis1973.SimpleCause.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance Lewis1973.SimpleCause.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance Lewis1973.SimpleCause.instReprV : Repr V

Equations

• Lewis1973.SimpleCause.instReprV = { reprPrec := Lewis1973.SimpleCause.instReprV.repr }

def Lewis1973.SimpleCause.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Lewis1973.SimpleCause.edges : Finset (V × V)

b follows a.

Equations

• Lewis1973.SimpleCause.edges = {(Lewis1973.SimpleCause.V.a, Lewis1973.SimpleCause.V.b)}

structure Lewis1973.SimpleCause.Context : Type

The context settles whether a occurs.

• a : Bool

def Lewis1973.SimpleCause.sem : CausalModel Context V fun (x : V) => Bool

b occurs when a does.

Equations

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

@[instance_reducible]

instance Lewis1973.SimpleCause.instDecidableRelVAdjGraphContextBoolSem : DecidableRel sem.graph.Adj

Equations

• Lewis1973.SimpleCause.instDecidableRelVAdjGraphContextBoolSem w v = Lewis1973.SimpleCause.instDecidableRelVAdjGraphContextBoolSem._aux_1 w v

instance Lewis1973.SimpleCause.instIsAcyclicContextVBoolSem : sem.IsAcyclic

theorem Lewis1973.SimpleCause.simple_butfor : lewisButFor sem { a := true } V.a V.b

A single cause passes the but-for test.

theorem Lewis1973.SimpleCause.simple_dependence : lewisDependence sem { a := true } V.a V.b

The effect depends on its single cause.

theorem Lewis1973.SimpleCause.simple_causation : lewisCausation sem { a := true } V.a V.b

A single cause is a cause.

inductive Lewis1973.Chain.V : Type

• a : V
• b : V
• c : V

@[instance_reducible]

instance Lewis1973.Chain.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance Lewis1973.Chain.instFintypeV : Fintype V

Equations

• Lewis1973.Chain.instFintypeV = { elems := { val := ↑Lewis1973.Chain.V.enumList, nodup := Lewis1973.Chain.V.enumList_nodup }, complete := Lewis1973.Chain.instFintypeV._proof_1 }

def Lewis1973.Chain.instReprV.repr : V → ℕ → Std.Format

Equations

• Lewis1973.Chain.instReprV.repr Lewis1973.Chain.V.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lewis1973.Chain.V.a")).group prec✝
• Lewis1973.Chain.instReprV.repr Lewis1973.Chain.V.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lewis1973.Chain.V.b")).group prec✝
• Lewis1973.Chain.instReprV.repr Lewis1973.Chain.V.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lewis1973.Chain.V.c")).group prec✝

@[instance_reducible]

instance Lewis1973.Chain.instReprV : Repr V

Equations

• Lewis1973.Chain.instReprV = { reprPrec := Lewis1973.Chain.instReprV.repr }

def Lewis1973.Chain.edges : Finset (V × V)

b follows a, and c follows b.

Equations

• Lewis1973.Chain.edges = {(Lewis1973.Chain.V.a, Lewis1973.Chain.V.b), (Lewis1973.Chain.V.b, Lewis1973.Chain.V.c)}

structure Lewis1973.Chain.Context : Type

The context settles whether a occurs.

• a : Bool

def Lewis1973.Chain.sem : CausalModel Context V fun (x : V) => Bool

The chain passes a on to b and b on to c.

Equations

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

@[instance_reducible]

instance Lewis1973.Chain.instDecidableRelVAdjGraphContextBoolSem : DecidableRel sem.graph.Adj

Equations

• Lewis1973.Chain.instDecidableRelVAdjGraphContextBoolSem w v = Lewis1973.Chain.instDecidableRelVAdjGraphContextBoolSem._aux_1 w v

instance Lewis1973.Chain.instIsAcyclicContextVBoolSem : sem.IsAcyclic

theorem Lewis1973.Chain.chain_direct_butfor : lewisButFor sem { a := true } V.a V.c

In a chain the distal cause passes the but-for test for the final effect.

theorem Lewis1973.Chain.chain_step_AB : lewisDependence sem { a := true } V.a V.b

The middle event depends on the first.

theorem Lewis1973.Chain.chain_step_BC : lewisDependence sem { a := true } V.b V.c

The final event depends on the middle one.

theorem Lewis1973.Chain.chain_causation : lewisCausation sem { a := true } V.a V.c

The first event causes the last through the chain.

The barometer reading and the storm are both effects of atmospheric pressure (pp. 561 and 564–565): the analysis makes the pressure the cause of each and neither effect a cause of the other.

inductive Lewis1973.Epiphenomena.V : Type

• pressure : V
• barometer : V
• storm : V

@[instance_reducible]

instance Lewis1973.Epiphenomena.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance Lewis1973.Epiphenomena.instFintypeV : Fintype V

Equations

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

@[instance_reducible]

instance Lewis1973.Epiphenomena.instReprV : Repr V

Equations

• Lewis1973.Epiphenomena.instReprV = { reprPrec := Lewis1973.Epiphenomena.instReprV.repr }

def Lewis1973.Epiphenomena.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Lewis1973.Epiphenomena.edges : Finset (V × V)

The pressure bears on the barometer and on the storm.

Equations

• Lewis1973.Epiphenomena.edges = {(Lewis1973.Epiphenomena.V.pressure, Lewis1973.Epiphenomena.V.barometer), (Lewis1973.Epiphenomena.V.pressure, Lewis1973.Epiphenomena.V.storm)}

structure Lewis1973.Epiphenomena.Context : Type

The context settles the pressure.

• pressure : Bool

def Lewis1973.Epiphenomena.sem : CausalModel Context V fun (x : V) => Bool

The barometer and the storm both follow the pressure.

Equations

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

@[instance_reducible]

instance Lewis1973.Epiphenomena.instDecidableRelVAdjGraphContextBoolSem : DecidableRel sem.graph.Adj

Equations

• Lewis1973.Epiphenomena.instDecidableRelVAdjGraphContextBoolSem w v = Lewis1973.Epiphenomena.instDecidableRelVAdjGraphContextBoolSem._aux_1 w v

instance Lewis1973.Epiphenomena.instIsAcyclicContextVBoolSem : sem.IsAcyclic

theorem Lewis1973.Epiphenomena.pressure_causes_barometer : lewisDependence sem { pressure := true } V.pressure V.barometer

Pressure causes the barometer reading.

theorem Lewis1973.Epiphenomena.pressure_causes_storm : lewisDependence sem { pressure := true } V.pressure V.storm

Pressure causes the storm.

theorem Lewis1973.Epiphenomena.barometer_not_causes_storm (u : Context) : ¬lewisDependence sem u V.barometer V.storm

The barometer does not cause the storm. No path runs from the barometer to the storm, so intervening on the barometer leaves the pressure, and so the storm, in place.

theorem Lewis1973.Epiphenomena.storm_not_causes_barometer (u : Context) : ¬lewisDependence sem u V.storm V.barometer

The storm does not cause the barometer reading.

Symmetric overdetermination (fn. 12): with two sufficient causes both present, neither is necessary, so neither passes the but-for test.

inductive Lewis1973.Overdetermination.V : Type

• a : V
• b : V
• e : V

@[instance_reducible]

instance Lewis1973.Overdetermination.instDecidableEqV : DecidableEq V

Equations

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

@[instance_reducible]

instance Lewis1973.Overdetermination.instFintypeV : Fintype V

Equations

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

def Lewis1973.Overdetermination.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lewis1973.Overdetermination.instReprV : Repr V

Equations

• Lewis1973.Overdetermination.instReprV = { reprPrec := Lewis1973.Overdetermination.instReprV.repr }

def Lewis1973.Overdetermination.edges : Finset (V × V)

Both causes bear on the effect.

Equations

• Lewis1973.Overdetermination.edges = {(Lewis1973.Overdetermination.V.a, Lewis1973.Overdetermination.V.e), (Lewis1973.Overdetermination.V.b, Lewis1973.Overdetermination.V.e)}

structure Lewis1973.Overdetermination.Context : Type

The context settles the two causes.

• a : Bool
• b : Bool

def Lewis1973.Overdetermination.sem : CausalModel Context V fun (x : V) => Bool

The effect occurs when either cause does.

Equations

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

@[instance_reducible]

instance Lewis1973.Overdetermination.instDecidableRelVAdjGraphContextBoolSem : DecidableRel sem.graph.Adj

Equations

• Lewis1973.Overdetermination.instDecidableRelVAdjGraphContextBoolSem w v = Lewis1973.Overdetermination.instDecidableRelVAdjGraphContextBoolSem._aux_1 w v

instance Lewis1973.Overdetermination.instIsAcyclicContextVBoolSem : sem.IsAcyclic

theorem Lewis1973.Overdetermination.overdetermination_no_butfor_a : ¬lewisButFor sem { a := true, b := true } V.a V.e

Neither overdetermining cause passes the but-for test, both being present.

theorem Lewis1973.Overdetermination.overdetermination_no_butfor_b : ¬lewisButFor sem { a := true, b := true } V.b V.e

theorem Lewis1973.Overdetermination.overdetermination_no_dependence_a : ¬lewisDependence sem { a := true, b := true } V.a V.e

Neither overdetermining cause is one the effect depends on.

theorem Lewis1973.Overdetermination.overdetermination_no_dependence_b : ¬lewisDependence sem { a := true, b := true } V.b V.e