Causal Necessity

[Nad23b] [NL20] [Sch11b]

Causal necessity semantics for the verb "cause." The core definition causallyNecessary (in Causation.SEM) implements [Nad23b] Definition 10b (supersituation necessity: precondition + achievability + but-for), superseding the simple but-for test from [NL20] Definition 24.

Insight

"X caused Y" asserts that X was necessary for Y: without X, Y would not have occurred (counterfactual dependence). X is a but-for cause: "but for X, not Y."

Necessity vs Sufficiency

Verb	Semantics	Test
cause	Necessity (Def 10b)	No consistent supersituation achieves E without C
make	Sufficiency (Def 23)	Does adding C guarantee E?

The legacy CausalDynamics-based causeSem/isINUSCause/ actuallyCaused were deleted in Phase D-H. The polymorphic V2 versions are promoted to canonical here.

noncomputable def Causation.Necessity.causeSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

V2 causal-necessity semantics for "cause": setting cause to xC develops effect to xE AND cause-as-xC is causally necessary (Nadathur 2023 Def 10b) for effect-as-xE. Polymorphic.

Equations

• Causation.Necessity.causeSem M background cause xC effect xE = (M.causallyEntails (background.extend cause xC) effect xE ∧ M.causallyNecessary background cause xC effect xE)

@[implicit_reducible]

noncomputable instance Causation.Necessity.instDecidableCauseSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (bg : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (causeSem M bg cause xC effect xE)

Equations

• Causation.Necessity.instDecidableCauseSem M bg cause xC effect xE = Classical.dec (Causation.Necessity.causeSem M bg cause xC effect xE)

noncomputable def Causation.Necessity.isINUSCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (cause : V) (xC : α cause) (effect : V) (xE : α effect) (enablingConditions : Valuation α) : Prop

V2 INUS cause (Mackie): insufficient but necessary part of an unnecessary but sufficient condition. Polymorphic.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.Necessity.instDecidableIsINUSCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (cause : V) (xC : α cause) (effect : V) (xE : α effect) (enablingConditions : Valuation α) : Decidable (isINUSCause M cause xC effect xE enablingConditions)

Equations

• Causation.Necessity.instDecidableIsINUSCause M cause xC effect xE enablingConditions = Classical.dec (Causation.Necessity.isINUSCause M cause xC effect xE enablingConditions)

noncomputable def Causation.Necessity.actuallyCaused {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

V2 actual causation: cause factually took value xC, and was causally necessary (Def 10b) for effect-as-xE — tested against the actual situation with cause stripped from the background. Polymorphic.

Equations

• Causation.Necessity.actuallyCaused M s cause xC effect xE = (s.hasValue cause xC ∧ Causation.Necessity.causeSem M (s.remove cause) cause xC effect xE)

@[implicit_reducible]

noncomputable instance Causation.Necessity.instDecidableActuallyCaused {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (actuallyCaused M s cause xC effect xE)

Equations

• Causation.Necessity.instDecidableActuallyCaused M s cause xC effect xE = Classical.dec (Causation.Necessity.actuallyCaused M s cause xC effect xE)