Causal Necessity

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

Causal necessity semantics for the verb "cause." The core definition causallyNecessary implements @cite{nadathur-2024} Definition 10b (supersituation necessity with 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"

Formal Definition (@cite{nadathur-2024} Def 10b)

⟨C, true⟩ is causally necessary for ⟨E, true⟩ relative to situation s iff:

• Precondition: s ⊭_D ⟨C, true⟩ and s ⊭_D ⟨E, true⟩
• (i) Achievability: ∃ consistent supersituation s' of s[C↦true] with E ∉ dom(s') where s' ⊨_D ⟨E, true⟩
• (ii) But-for: ¬∃ consistent supersituation s' of s with E ∉ dom(s') satisfying s' ⊨_D ⟨E, true⟩ while s' ⊭_D ⟨C, true⟩

Linguistic Examples

1. "The short circuit caused the fire"

   • Without the short circuit, the fire wouldn't have started
   • The short circuit was necessary (in that context)

2. "Kim's actions caused Sandy to leave"

   • If Kim hadn't acted, Sandy would have stayed
   • Kim's action was a but-for cause

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?

These can come apart in overdetermination cases:

• Lightning AND arsonist both present
• Lightning sufficient for fire
• Lightning NOT necessary (arsonist would have caused it anyway)

def NadathurLauer2020.Necessity.causeSem (dyn : Core.StructuralEquationModel.CausalDynamics) (background : Core.StructuralEquationModel.Situation) (causeEvent effectEvent : Core.StructuralEquationModel.Variable) : Bool

Semantics of "cause": effect occurred AND cause was necessary. Necessity uses @cite{nadathur-2024} Def 10b (supersituation test).

Equations

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

theorem NadathurLauer2020.Necessity.redundant_cause_not_necessary (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (c1 c2 effect : Core.StructuralEquationModel.Variable) (hne : c1 ≠ c2) (hPos : Core.StructuralEquationModel.isPositiveDynamics dyn = true) (h_c2_present : s.hasValue c2 true = true) (h_c2_sufficient : Core.StructuralEquationModel.causallySufficient dyn (s.remove c1) c2 effect = true) : causallyNecessary dyn s c1 effect = false

An alternative sufficient cause makes the original unnecessary.

Requires positive dynamics (no inhibitory connections) and c1 ≠ c2: in positive dynamics, setting c1 = false doesn't trigger new laws, so the sufficient alternative c2 still fires the effect. Without positivity, a law with precondition (c1, false) could inhibit the effect.

Under Def 10b, this follows from the precondition check: if c2 is sufficient and present in s, then the effect is already causally entailed by s (via monotonicity), so the precondition s ⊭_D ⟨effect, true⟩ fails.

theorem NadathurLauer2020.Necessity.sufficiency_not_implies_necessity : ∃ (dyn : Core.StructuralEquationModel.CausalDynamics), ∃ (s : Core.StructuralEquationModel.Situation), ∃ (cause : Core.StructuralEquationModel.Variable), ∃ (effect : Core.StructuralEquationModel.Variable), Core.StructuralEquationModel.causallySufficient dyn s cause effect = true ∧ causallyNecessary dyn s cause effect = false

Sufficiency does NOT imply necessity (overdetermination).

theorem NadathurLauer2020.Necessity.necessity_not_implies_sufficiency : ∃ (dyn : Core.StructuralEquationModel.CausalDynamics), ∃ (s : Core.StructuralEquationModel.Situation), ∃ (cause : Core.StructuralEquationModel.Variable), ∃ (effect : Core.StructuralEquationModel.Variable), causallyNecessary dyn s cause effect = true ∧ Core.StructuralEquationModel.causallySufficient dyn Core.StructuralEquationModel.Situation.empty cause effect = false

Necessity does NOT imply sufficiency (conjunctive causes).

def NadathurLauer2020.Necessity.isINUSCause (dyn : Core.StructuralEquationModel.CausalDynamics) (cause effect : Core.StructuralEquationModel.Variable) (enablingConditions : Core.StructuralEquationModel.Situation) : Bool

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

Equations

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

def NadathurLauer2020.Necessity.actuallyCaused (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) : Bool

Actual causation: C factually occurred, E factually occurred, and C was causally necessary for E.

Under @cite{nadathur-2024} Definition 10b, necessity must be tested against a background that does NOT contain the cause (the precondition rejects situations where cause is already entailed). We strip the cause from s via s.remove cause before passing to causeSem.

This is the retrospective causal judgment: "did C actually cause E in situation s?"

Equations

• NadathurLauer2020.Necessity.actuallyCaused dyn s cause effect = (s.hasValue cause true && NadathurLauer2020.Necessity.causeSem dyn (s.remove cause) cause effect)

theorem NadathurLauer2020.Necessity.actuallyCaused_eq_causeSem (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) : actuallyCaused dyn s cause effect = (s.hasValue cause true && causeSem dyn (s.remove cause) cause effect)

actuallyCaused is causeSem applied to the actual situation with the cause stripped from the background.

theorem NadathurLauer2020.Necessity.actual_cause_cause_occurred (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) (h : actuallyCaused dyn s cause effect = true) : s.hasValue cause true = true

Actual causation implies the cause occurred.

theorem NadathurLauer2020.Necessity.actual_cause_effect_occurred (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) (h : actuallyCaused dyn s cause effect = true) : (Core.StructuralEquationModel.normalDevelopment dyn ((s.remove cause).extend cause true)).hasValue effect true = true

Actual causation implies the effect occurred.

theorem NadathurLauer2020.Necessity.actual_cause_necessary (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) (h : actuallyCaused dyn s cause effect = true) : causallyNecessary dyn (s.remove cause) cause effect = true

Actual causation implies causal necessity.