@cite{lewis-1973-causation}: Causation

@cite{lewis-1973-causation}

Formalization of Lewis's counterfactual analysis of causation against the V2 SEM substrate.

Three Key Concepts

1. Causal dependence (p. 563): e depends causally on c iff the counterfactual "if c had not occurred, e would not have occurred" holds — the but-for test.

2. Causation (p. 563): the transitive closure of causal dependence. c causes e iff there exists a causal chain from c to e where each consecutive pair is a causal dependence. Defined via mathlib's Relation.TransGen.

3. Epiphenomena asymmetry (p. 565): intervention-based counterfactuals correctly distinguish genuine causes from mere correlates. The barometer does not cause the storm, even though they are correlated via atmospheric pressure.

Bridge to Linglib Infrastructure

Lewis's causal dependence corresponds to the simple but-for test in our V2 SEM framework. For exogenous causes, lewisButFor is structurally identical to ¬ BoolSEM.causallySufficient with the alternative cause-value.

The key difference from @cite{nadathur-2024} Def 10b (causallyNecessary): Lewis's but-for operates on the actual world via minimal intervention, while Def 10b quantifies over consistent supersituations. For simple models they agree; for complex models with alternative pathways, Def 10b is strictly stronger. Bridge theorems comparing Lewis to Nadathur 2024 await the Necessity hub migration to V2.

Limitations

@cite{lewis-1973-causation} acknowledges two limitations:

• Overdetermination (fn. 12): symmetric overdetermination cases are excluded — neither overdetermining cause passes the but-for test.
• Late preemption: the transitive closure mechanism handles early preemption but struggles with late preemption.

noncomputable def Lewis1973.lewisButFor {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) : Prop

Lewis's but-for counterfactual: setting cause to false (the absent value) prevents the effect under developDetOn.

"If c had not occurred, e would not have occurred." Polymorphic over the vertex type W so each scenario can use its own enum.

Equations

• Lewis1973.lewisButFor M vs bg cause effect = ¬(Core.Causal.SEM.developDetOn M vs 1 (bg.extend cause false)).hasValue effect true

@[implicit_reducible]

noncomputable instance Lewis1973.instDecidableLewisButFor {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) : Decidable (lewisButFor M vs bg cause effect)

Equations

• Lewis1973.instDecidableLewisButFor M vs bg cause effect = Classical.dec (Lewis1973.lewisButFor M vs bg cause effect)

noncomputable def Lewis1973.lewisDependence {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) : Prop

Lewis's causal dependence (@cite{lewis-1973-causation} p. 563).

Three conjuncts: cause develops, effect develops, and without cause the effect does not developDet.

Equations

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

@[implicit_reducible]

noncomputable instance Lewis1973.instDecidableLewisDependence {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) : Decidable (lewisDependence M vs bg cause effect)

Equations

• Lewis1973.instDecidableLewisDependence M vs bg cause effect = Classical.dec (Lewis1973.lewisDependence M vs bg cause effect)

def Lewis1973.lewisCausation {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) : Prop

Lewis's causation: transitive closure of causal dependence (@cite{lewis-1973-causation} p. 563), via Relation.TransGen.

Equations

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

theorem Lewis1973.dependence_implies_causation {W : Type u_1} [Fintype W] [DecidableEq W] (M : Core.Causal.BoolSEM W) [Core.Causal.SEM.IsDeterministic M] (vs : List W) (bg : Core.Causal.Valuation fun (x : W) => Bool) (cause effect : W) (h : lewisDependence M vs bg cause effect) : lewisCausation M vs bg cause effect

Causal dependence implies causation (one-step chain).

inductive Lewis1973.SimpleCause.V : Type

• a : V
• b : V

@[implicit_reducible]

instance Lewis1973.SimpleCause.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance Lewis1973.SimpleCause.instFintypeV : Fintype V

Equations

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

@[implicit_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.varList : List V

Equations

• Lewis1973.SimpleCause.varList = [Lewis1973.SimpleCause.V.a, Lewis1973.SimpleCause.V.b]

def Lewis1973.SimpleCause.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Lewis1973.SimpleCause.sem : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Lewis1973.SimpleCause.instIsDeterministicVBoolSem : Core.Causal.SEM.IsDeterministic sem

Equations

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

def Lewis1973.SimpleCause.bg : Core.Causal.Valuation fun (x : V) => Bool

Equations

• Lewis1973.SimpleCause.bg = Core.Causal.Valuation.empty.extend Lewis1973.SimpleCause.V.a true

theorem Lewis1973.SimpleCause.simple_butfor : lewisButFor sem varList bg V.a V.b

Lewis's but-for holds for a simple cause.

theorem Lewis1973.SimpleCause.simple_dependence : lewisDependence sem varList bg V.a V.b

Lewis's causal dependence holds for a simple cause.

theorem Lewis1973.SimpleCause.simple_causation : lewisCausation sem varList bg V.a V.b

Lewis's causation holds (trivially, one-step chain).

inductive Lewis1973.Chain.V : Type

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

@[implicit_reducible]

instance Lewis1973.Chain.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_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 }

@[implicit_reducible]

instance Lewis1973.Chain.instReprV : Repr V

Equations

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

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✝

def Lewis1973.Chain.varList : List V

Equations

• Lewis1973.Chain.varList = [Lewis1973.Chain.V.a, Lewis1973.Chain.V.b, Lewis1973.Chain.V.c]

def Lewis1973.Chain.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Lewis1973.Chain.sem : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Lewis1973.Chain.instIsDeterministicVBoolSem : Core.Causal.SEM.IsDeterministic sem

Equations

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

def Lewis1973.Chain.bg : Core.Causal.Valuation fun (x : V) => Bool

Equations

• Lewis1973.Chain.bg = Core.Causal.Valuation.empty.extend Lewis1973.Chain.V.a true

theorem Lewis1973.Chain.chain_direct_butfor : lewisButFor sem varList bg V.a V.c

In the chain A→B→C, removing A prevents C.

theorem Lewis1973.Chain.chain_step_AB : lewisDependence sem varList bg V.a V.b

B depends on A.

theorem Lewis1973.Chain.chain_step_BC : lewisDependence sem varList bg V.b V.c

C depends on B.

theorem Lewis1973.Chain.chain_causation : lewisCausation sem varList bg V.a V.c

Lewis's causation via the full chain A→B→C.

@cite{lewis-1973-causation} p. 565: barometer reading (B) and storm (S) are both effects of atmospheric pressure (P). The counterfactual analysis correctly identifies P as the common cause and rejects spurious "barometer causes storm" inference.

inductive Lewis1973.Epiphenomena.V : Type

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

@[implicit_reducible]

instance Lewis1973.Epiphenomena.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance Lewis1973.Epiphenomena.instFintypeV : Fintype V

Equations

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

@[implicit_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.varList : List V

Equations

• Lewis1973.Epiphenomena.varList = [Lewis1973.Epiphenomena.V.pressure, Lewis1973.Epiphenomena.V.barometer, Lewis1973.Epiphenomena.V.storm]

def Lewis1973.Epiphenomena.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Lewis1973.Epiphenomena.sem : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Lewis1973.Epiphenomena.instIsDeterministicVBoolSem : Core.Causal.SEM.IsDeterministic sem

Equations

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

def Lewis1973.Epiphenomena.bg : Core.Causal.Valuation fun (x : V) => Bool

Equations

• Lewis1973.Epiphenomena.bg = Core.Causal.Valuation.empty.extend Lewis1973.Epiphenomena.V.pressure true

theorem Lewis1973.Epiphenomena.pressure_causes_barometer : lewisDependence sem varList bg V.pressure V.barometer

Pressure causes the barometer reading.

theorem Lewis1973.Epiphenomena.pressure_causes_storm : lewisDependence sem varList bg V.pressure V.storm

Pressure causes the storm.

theorem Lewis1973.Epiphenomena.barometer_not_causes_storm : ¬lewisDependence sem varList bg V.barometer V.storm

The barometer does NOT cause the storm.

@cite{lewis-1973-causation} p. 565: intervention on the barometer (do(B=false)) cuts B's incoming law (P→B) but leaves P→S intact. P still causes S regardless of B.

theorem Lewis1973.Epiphenomena.storm_not_causes_barometer : ¬lewisDependence sem varList bg V.storm V.barometer

The storm does NOT cause the barometer.

@cite{lewis-1973-causation} fn. 12: symmetric overdetermination cases are excluded — neither overdetermining factor passes the but-for test.

Model: A ∨ B → E. With both present, neither is necessary. 

inductive Lewis1973.Overdetermination.V : Type

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

@[implicit_reducible]

instance Lewis1973.Overdetermination.instDecidableEqV : DecidableEq V

Equations

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

@[implicit_reducible]

instance Lewis1973.Overdetermination.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Lewis1973.Overdetermination.instReprV : Repr V

Equations

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

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

Equations

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

def Lewis1973.Overdetermination.varList : List V

Equations

• Lewis1973.Overdetermination.varList = [Lewis1973.Overdetermination.V.a, Lewis1973.Overdetermination.V.b, Lewis1973.Overdetermination.V.e]

def Lewis1973.Overdetermination.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Lewis1973.Overdetermination.sem : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Lewis1973.Overdetermination.instIsDeterministicVBoolSem : Core.Causal.SEM.IsDeterministic sem

Equations

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

def Lewis1973.Overdetermination.bg : Core.Causal.Valuation fun (x : V) => Bool

Both causes present.

Equations

• Lewis1973.Overdetermination.bg = (Core.Causal.Valuation.empty.extend Lewis1973.Overdetermination.V.a true).extend Lewis1973.Overdetermination.V.b true

theorem Lewis1973.Overdetermination.overdetermination_no_butfor_a : ¬lewisButFor sem varList bg V.a V.e

Neither overdetermining cause passes the but-for test (B alive when A removed; A alive when B removed).

theorem Lewis1973.Overdetermination.overdetermination_no_butfor_b : ¬lewisButFor sem varList bg V.b V.e

theorem Lewis1973.Overdetermination.overdetermination_no_dependence_a : ¬lewisDependence sem varList bg V.a V.e

Neither overdetermining cause is a Lewis causal dependent.

theorem Lewis1973.Overdetermination.overdetermination_no_dependence_b : ¬lewisDependence sem varList bg V.b V.e