Causal Sufficiency

Causal sufficiency semantics for the verb "make" based on @cite{nadathur-lauer-2020} Definition 23.

Insight

"X made Y happen" asserts that X was sufficient for Y:

• Given the background situation, adding X guarantees Y
• The effect is inevitable once the cause is in place

Formal Definition (Def 23)

C is causally sufficient for E in situation s iff: normalDevelopment(s ⊕ {C = true}) includes E = true

In other words: if we add C to the background, E necessarily follows.

Linguistic Examples

1. "Kim made Sandy leave"

   • Kim's action (persuasion, coercion, etc.) was sufficient for Sandy leaving
   • Once Kim acted, Sandy's departure was guaranteed

2. "The short circuit made the fire start"

   • The short circuit alone was enough to cause the fire
   • No other conditions needed (beyond background)

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

Semantics of "make": X was causally sufficient for Y (@cite{nadathur-lauer-2020} §5.1).

Equations

• NadathurLauer2020.Sufficiency.makeSem dyn background causeEvent effectEvent = Core.StructuralEquationModel.causallySufficient dyn background causeEvent effectEvent

theorem NadathurLauer2020.Sufficiency.simple_isPositive (a b : Core.StructuralEquationModel.Variable) : Core.StructuralEquationModel.isPositiveDynamics { laws := [Core.StructuralEquationModel.CausalLaw.simple a b] } = true

Standard constructors produce positive dynamics.

theorem NadathurLauer2020.Sufficiency.conjunctive_isPositive (a b c : Core.StructuralEquationModel.Variable) : Core.StructuralEquationModel.isPositiveDynamics { laws := [Core.StructuralEquationModel.CausalLaw.conjunctive a b c] } = true

theorem NadathurLauer2020.Sufficiency.disjunctive_isPositive (a b c : Core.StructuralEquationModel.Variable) : Core.StructuralEquationModel.isPositiveDynamics (Core.StructuralEquationModel.CausalDynamics.disjunctiveCausation a b c) = true

theorem NadathurLauer2020.Sufficiency.chain_isPositive (a b c : Core.StructuralEquationModel.Variable) : Core.StructuralEquationModel.isPositiveDynamics (Core.StructuralEquationModel.CausalDynamics.causalChain a b c) = true

theorem NadathurLauer2020.Sufficiency.sufficiency_monotone_positive (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (c1 c2 effect : Core.StructuralEquationModel.Variable) (hPos : Core.StructuralEquationModel.isPositiveDynamics dyn = true) (h : causallySufficient dyn s c1 effect = true) : causallySufficient dyn (s.extend c2 true) c1 effect = true

Sufficiency is monotone for positive dynamics.

In causal models with no inhibitory connections (all preconditions require true, all effects set variables to true), adding c2 = true to the background preserves causal sufficiency.

Proof: Define trueLE s₁ s₂ ("every variable true in s₁ is true in s₂"). Show that positive dynamics preserve trueLE through applyLawsOnce (induction on the law list) and normalDevelopment (induction on fuel, with a fixpoint absorption lemma for the asymmetric case).

theorem NadathurLauer2020.Sufficiency.sufficient_implies_effect (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (cause effect : Core.StructuralEquationModel.Variable) (h : causallySufficient dyn s cause effect = true) : Core.StructuralEquationModel.developsToTrue dyn (s.extend cause true) effect = true

Sufficiency implies effect occurrence (after cause).

theorem NadathurLauer2020.Sufficiency.disjunctive_each_sufficient (a b c : Core.StructuralEquationModel.Variable) (_ha : a ≠ b) : have dyn := Core.StructuralEquationModel.CausalDynamics.disjunctiveCausation a b c; causallySufficient dyn Core.StructuralEquationModel.Situation.empty a c = true

In disjunctive causation (A ∨ B → C), each disjunct is sufficient.

theorem NadathurLauer2020.Sufficiency.conjunctive_neither_sufficient_alone (a b c : Core.StructuralEquationModel.Variable) (_ha : a ≠ b) (_hac : a ≠ c) (_hbc : b ≠ c) : have dyn := Core.StructuralEquationModel.CausalDynamics.conjunctiveCausation a b c; causallySufficient dyn Core.StructuralEquationModel.Situation.empty a c = false

In conjunctive causation (A ∧ B → C), neither alone is sufficient.

theorem NadathurLauer2020.Sufficiency.conjunctive_sufficient_with_other (a b c : Core.StructuralEquationModel.Variable) (_ha : a ≠ b) (_hac : a ≠ c) (_hbc : b ≠ c) : have dyn := Core.StructuralEquationModel.CausalDynamics.conjunctiveCausation a b c; have background := Core.StructuralEquationModel.Situation.empty.extend b true; causallySufficient dyn background a c = true

In conjunctive causation, A is sufficient when B is in the background.