Causal Necessity

@cite{nadathur-2024} @cite{nadathur-lauer-2020} @cite{schulz-2011}

Causal necessity semantics for the verb "cause." The core definition causallyNecessary (in Core.Causal.SEM) implements @cite{nadathur-2024} Definition 10b (supersituation necessity: precondition + achievability + but-for), superseding the simple but-for test from @cite{nadathur-lauer-2020} 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 Semantics.Causation.Necessity.causeSem {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (background : Core.Causal.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 2024 Def 10b) for effect-as-xE. Polymorphic.

Equations

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

@[implicit_reducible]

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

Equations

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

noncomputable def Semantics.Causation.Necessity.isINUSCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (cause : V) (xC : α cause) (effect : V) (xE : α effect) (enablingConditions : Core.Causal.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 Semantics.Causation.Necessity.instDecidableIsINUSCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (cause : V) (xC : α cause) (effect : V) (xE : α effect) (enablingConditions : Core.Causal.Valuation α) : Decidable (isINUSCause M cause xC effect xE enablingConditions)

Equations

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

noncomputable def Semantics.Causation.Necessity.actuallyCaused {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [Core.Causal.DecidableValuation α] [(v : V) → Fintype (α v)] (M : Core.Causal.SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Core.Causal.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

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

@[implicit_reducible]

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

Equations

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