Docs / Studies / Studies.Lewis1973a

Causation

Lewis, D. (1973). The Journal of Philosophy, 70(17), 556–567

Lewis analyses causation through counterfactuals over comparative similarity: an event depends causally on a distinct event when whether the one occurs depends counterfactually on whether the other does, and causation is the ancestral of causal dependence among actual events. On a deterministic causal model, every similarity that favours worlds keeping to the actual course of events longer and violating fewer laws, however it weighs the two, makes the counterfactual of setting a variable the intervention, which does not backtrack. Among actual events causal dependence is then the but-for test, and the analysis separates a cause from its epiphenomena and a preempting cause from the cause it preempts.

Implementation notes

A world is an assignment to the variables of the model, the actual world of a context is its solution, and the counterfactual is evaluated at the context. Time is rank in the causal order, the model having no other temporal structure, so the direction of counterfactual dependence is read off the causal graph rather than an independent direction of time, and in an acyclic model no event causes one of its causes. The equations of variables without parents record the circumstances the context fixes, and a world departing from them violates them. similarity weighs late divergence before violations, one resolution of the weighting the paper leaves open. An event is a Boolean variable, occurring where it is true. That c₂ would have caused e had c₁ been absent is read in the context without c₁, which is the counterfactual world since c₁ has no parents. Nomic dependence and the regularity analysis are not formalized.

TODO

The barometer: counterfactual dependence between families of many alternatives, and its irreversibility.

References

Lewis 1973a, Causation
Lewis 1973b, Counterfactuals formalized

Counterfactual and causal dependence

L61–65

L67–71

L76–79

Comparative similarity on a causal model

Under any similarity that brings a world closer when it departs from the actual course of events later or violates fewer laws, however it weighs the two, the counterfactual whose antecedent sets the variable c to b holds exactly when its consequent holds in the world of the intervention setting c to b. The closest such world keeps to the actual course of events until the time of c and violates only the law of c (pp. 566–567).

theorem mem_variablyStrictImp_iff_solve_update L203–222

{U : Type u_1} {V : Type u_2} {α : V → Type u_3} [∀ (v : V), Nonempty (α v)] {M : CausalModel U V α} [M.IsAcyclic] {u : U} {c : V} [DecidableEq V] {b : α c} {ord : U → Preorder ((v : V) → α v)} (hord : ∀ (x y : (v : V) → α v), score M u x < score M u y → x < y) {C : Set ((v : V) → α v)} :

u ∈ Conditional.variablyStrictImp (fun (x : U) => Set.univ) ord {x : (v : V) → α v | x c = b} C ↔ M.solve (Function.update ⊥ c ↑b) u ∈ C

Built from

L224–227

Had c been other than it is, every event that c does not reach would have been as it actually was: the counterfactual does not backtrack, and had an effect been absent its cause would have occurred just as it did (p. 566).

theorem mem_variablyStrictImp_similarity_of_not_reflTransGen L229–236

{U : Type u_1} {V : Type u_2} {α : V → Type u_3} [∀ (v : V), Nonempty (α v)] {M : CausalModel U V α} [M.IsAcyclic] {u : U} {c : V} [DecidableEq V] {b : α c} {v : V} (h : ¬Relation.ReflTransGen M.graph.Adj c v) :

u ∈ Conditional.variablyStrictImp (fun (x : U) => Set.univ) (similarity M) {x : (v : V) → α v | x c = b} {x : (v : V) → α v | x v = M.solve ⊥ u v}

Built from

Causation

L246–248

L250–255

L259–263

Among actual events, e depends causally on c exactly when, had c not been, e would not have been (p. 563).

theorem mem_dependsCausally_iff_of_actual L265–272

{U : Type u_1} {V : Type u_2} {M : CausalModel U V fun (x : V) => Bool} [M.IsAcyclic] {u : U} {c e : V} [DecidableEq V] (hc : M.solve ⊥ u c = true) (he : M.solve ⊥ u e = true) :

u ∈ dependsCausally (fun (x : U) => Set.univ) (similarity M) (occurs c) (occurs e) ↔ M.solve (Function.update ⊥ c ↑false) u e = false

Built from , ,

Effects and epiphenomena

The event c causes first e and then, through d, f, e being an epiphenomenon of c. Had e not occurred, c would not have been absent but would have failed to cause e, so neither c nor f depends on e, although e precedes f.

The epiphenomenon e causes neither its cause c nor the later effect f of c, though c causes both (pp. 565–566).

theorem Epiphenomena.epiphenomena L343–348

Cause sem { c := true } V.c V.e ∧ Cause sem { c := true } V.c V.f ∧ ¬Cause sem { c := true } V.e V.c ∧ ¬Cause sem { c := true } V.e V.f

Built from ,

Preemption

The events c₁ and c₂ both occur. c₁ causes e through d, and c₂ would have caused e through d₂ had c₁ been absent, but c₁ cuts that process off. Had d been absent, c₁ would still have been there to interfere with c₂, so e depends on d.

c₁ causes e through d, on which e depends, though e does not depend causally on c₁; and the preempted c₂, from which no causal chain leads to e, is no cause of it, though it is one where c₁ is absent (p. 567).

theorem Preemption.preemption L386–396

Cause sem { c₁ := true, c₂ := true } V.c₁ V.e ∧ { c₁ := true, c₂ := true } ∈ dependsCausally (fun (x : Context) => Set.univ) (similarity sem) (occurs V.d) (occurs V.e) ∧ { c₁ := true, c₂ := true } ∉ dependsCausally (fun (x : Context) => Set.univ) (similarity sem) (occurs V.c₁) (occurs V.e) ∧ ¬Cause sem { c₁ := true, c₂ := true } V.c₂ V.e ∧ Cause sem { c₁ := false, c₂ := true } V.c₂ V.e

Built from , , , , ,

L399–402

Symmetric overdetermination

Two causes each sufficient for the effect both occur, a case footnote 12 sets aside as no test of the analysis for want of firm naive opinions about it.