SEM: Causal Counterfactual Predicates (V2)

Polymorphic counterfactual predicates over a SEM V α, plus BoolSEM-flavored aliases for legacy SBH-style binary semantics.

• developsToValue M s v x: after developing s, vertex v has value x. Replaces the old developsToTrue (Bool-specialized) with a polymorphic version.

• causallySufficient M s cause xC effect xE: extending s with xC at cause then developing produces xE at effect. Polymorphic generalization of @cite{nadathur-lauer-2020} Definition 23.

• causallyNecessary M s cause xC effect xE: @cite{nadathur-2024} Definition 10b — precondition + achievability + but-for clauses. Refactored to use abstract quantification over Valuation α (see "Refactor" below); the previous allExtensions/freeExtensions enumeration was noncomputable and opaque to structural reduction.

BoolSEM-namespace aliases specialize the polymorphic predicates to α := fun _ => Bool with xC = true, xE = true (legacy SBH semantics).

Refactor (post-Deterministic.lean)

Internally these predicates call developDetVtx M s v = x (per-vertex, structurally reducible via WellFounded.fix_eq) instead of the old opaque (M.developDet s).hasValue v x. The (M.developDet s).hasValue v x API shape still works via developDet_hasValue_iff — same call sites, cleanly reducible internals.

causallyNecessary's achievability/but-for clauses are now stated as abstract quantifications over Valuation α (∃ s', s.le s' ∧ ... / ∀ s', s.le s' → ...) rather than enumeration over a noncomputable allExtensions list. Concrete proofs supply existential witnesses directly and discharge universals by case analysis on which free vertices s' fixes (the isConsistentSuper clause constrains s''s values to agree with developDetVtx M s). Same paper content; structurally provable.

Computability

developDet is noncomputable (cascading from WellFounded.fix). Predicates here are noncomputable. Decidable instances via Classical.dec. Concrete proofs reduce structurally via developDetVtx_unfold + rfl rather than through Fintype.elems.toList opacity (which blocked the previous substrate). Matches the mathlib Polynomial.eval precedent: noncomputable canonical definition, structurally reducible per-vertex unfolding lemmas.

def Core.Causal.SEM.developsToValue {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : Prop

After developing the SEM against s, vertex v has the value x.

Polymorphic generalization of the old developsToTrue (which fixed α := fun _ => Bool and x := true).

Equations

• M.developsToValue s v x = (M.developDet s).hasValue v x

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instDecidableDevelopsToValue {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : Decidable (M.developsToValue s v x)

Equations

• M.instDecidableDevelopsToValue s v x = Classical.dec (M.developsToValue s v x)

def Core.Causal.SEM.causallySufficient {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

Causal sufficiency: forcing cause to xC makes effect developDet to xE.

Polymorphic generalization of @cite{nadathur-lauer-2020} Definition 23. The Bool case (BoolSEM.causallySufficient) recovers the legacy semantics "cause = true produces effect = true".

Equations

• M.causallySufficient s cause xC effect xE = M.developsToValue (s.extend cause xC) effect xE

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instDecidableCausallySufficient {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (M.causallySufficient s cause xC effect xE)

Equations

• M.instDecidableCausallySufficient s cause xC effect xE = Classical.dec (M.causallySufficient s cause xC effect xE)

@[simp]

theorem Core.Causal.SEM.developsToValue_iff {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : M.developsToValue s v x ↔ (M.developDet s).hasValue v x

developsToValue unfolds to (developDet M s).hasValue v x.

@[simp]

theorem Core.Causal.SEM.causallySufficient_iff {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : M.causallySufficient s cause xC effect xE ↔ M.developsToValue (s.extend cause xC) effect xE

causallySufficient unfolds to developsToValue of the extended valuation.

def Core.Causal.SEM.manipulates {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC1 xC2 : α cause) (effect : V) : Prop

Interventionist manipulation (Woodward's criterion): cause's value affects effect's value under developDet. Defined via extend rather than intervene because for deterministic acyclic SEMs they agree and extend doesn't require re-establishing IsDeterministic on the intervened SEM.

Equations

• M.manipulates s cause xC1 xC2 effect = ((M.developDet (s.extend cause xC1)).get effect ≠ (M.developDet (s.extend cause xC2)).get effect)

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instDecidableManipulates {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC1 xC2 : α cause) (effect : V) : Decidable (M.manipulates s cause xC1 xC2 effect)

Equations

• M.instDecidableManipulates s cause xC1 xC2 effect = Classical.dec (M.manipulates s cause xC1 xC2 effect)

Pearl-style counterfactual simulation via Lassiter's RRR heuristic (@cite{lassiter-2017-probabilistic-language} §3): "Rewind to the antecedent's causal layer, Revise the antecedent, selectively Regenerate descendants while preserving causally-independent observations." Subsumes: - @cite{lewis-1973-causation} / @cite{nadathur-lauer-2020} deterministic counterfactuals (Dirac specialization) - @cite{beller-gerstenberg-2025} W/H/S aspects (graded probability) - @cite{lassiter-2017-probabilistic-language} probabilistic counterfactuals with overt probability operators

Key insight: under the high-stability assumption (Lucas & Kemp 2015
ESM), Pearl 3-step abduction reduces to "preserve causally-independent
observations, regenerate descendants" — no explicit exogenous noise
types needed. The existing `develop` PMF naturally produces the right
distribution when fed the counterfactual seed valuation.

Morgenbesser's coin example (Barker 1998, Lassiter §1): bet → win ←
heads. Observed `{bet:=false, win:=false, heads:=true}`. Counterfactual
`bet := true`. Then `cfSeed = {bet:=true, heads:=true, win:=none}`
(heads is causally independent so preserved; win is descendant of bet
so regenerated). `develop` computes `win := bet ∧ heads = true`. The
counterfactual probability of winning is 1, matching Lassiter's
prediction (and contradicting "Rewind, Revise, Re-run" without
selective regeneration). 

noncomputable def Core.Causal.SEM.cfSeed {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) (observed : Valuation α) (antecedent : V) (xAnt : α antecedent) : Valuation α

Counterfactual seed (Lassiter §3 RRR): the partial valuation that counterfactualSimulate feeds to develop. Sets antecedent := xAnt, leaves descendants of antecedent undetermined (to be regenerated), preserves observed values for causally-independent vertices.

Equations

• M.cfSeed observed antecedent xAnt v = if h : v = antecedent then some (⋯ ▸ xAnt) else if M.graph.IsStrictAncestor antecedent v then none else observed.get v

noncomputable def Core.Causal.SEM.counterfactualSimulate {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] (observed : Valuation α) (antecedent : V) (xAnt : α antecedent) : PMF (Valuation α)

Pearl 3-step counterfactual via Lassiter RRR, PMF-valued. Given actually-observed observed and a counterfactual intervention antecedent := xAnt, returns the probability distribution over counterfactual valuations.

For deterministic SEMs, collapses to a Dirac at developDet M (cfSeed ...) (see counterfactualSimulate_eq_pure_of_deterministic below).

Subsumes (with appropriate derived predicates):

• causallyNecessary (@cite{nadathur-2024} Def 10b, discrete)
• whetherCause (@cite{beller-gerstenberg-2025} Eq 1, graded)
• sufficientCause (@cite{beller-gerstenberg-2025} Eq 3, graded)
• Lassiter probabilistic counterfactuals with overt probability operators

probabilisticSuf (@cite{cao-white-lassiter-2025}) is not a special case — it's interventional probability without observation conditioning; lives in Interventional.lean.

Equations

• M.counterfactualSimulate observed antecedent xAnt = M.develop (M.cfSeed observed antecedent xAnt)

noncomputable def Core.Causal.SEM.whetherCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] (observed : Valuation α) (antecedent : V) (xAnt_alt : α antecedent) (effect : V) (xEff_actual : α effect) : ENNReal

Whether-causation (@cite{beller-gerstenberg-2025} Eq 1): W(A → e) = P(e' ≠ e | s, remove(A)). Probability that the counterfactual outcome differs from the actual outcome xEff_actual if the antecedent were xAnt_alt instead of its actual value.

For deterministic SEMs, collapses to a {0,1} indicator (see whetherCause_eq_indicator_of_deterministic).

Equations

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

noncomputable def Core.Causal.SEM.sufficientCause {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] (alternativesRemoved : Valuation α) (antecedent : V) (xAnt_alt : α antecedent) (effect : V) (xEff_actual : α effect) : ENNReal

Sufficient-causation (@cite{beller-gerstenberg-2025} Eq 3): S(A → e) = P(W(A → e') | s, remove(\A)). Probability that A would have been a whether-cause if all alternative causes had been removed.

The caller supplies alternativesRemoved : Valuation α — the supersituation of s where alternative causes are set to their absent values. In the typical case this is s with the causally-independent siblings of antecedent set to their absent values. The substrate doesn't currently provide a removeAlternatives constructor; callers build it explicitly via s.extend altᵢ xAbsentᵢ chains.

Equations

• M.sufficientCause alternativesRemoved antecedent xAnt_alt effect xEff_actual = M.whetherCause alternativesRemoved antecedent xAnt_alt effect xEff_actual

theorem Core.Causal.SEM.counterfactualSimulate_eq_pure_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (observed : Valuation α) (antecedent : V) (xAnt : α antecedent) : M.counterfactualSimulate observed antecedent xAnt = PMF.pure (M.developDet (M.cfSeed observed antecedent xAnt))

Bridge: under IsDeterministic, counterfactualSimulate is the Dirac of the per-vertex counterfactual valuation developDet M (cfSeed ...). Follows immediately from develop_eq_pure_of_deterministic (Basic.lean).

theorem Core.Causal.SEM.whetherCause_eq_indicator_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (observed : Valuation α) (antecedent : V) (xAnt_alt : α antecedent) (effect : V) (xEff_actual : α effect) : M.whetherCause observed antecedent xAnt_alt effect xEff_actual = if (M.developDet (M.cfSeed observed antecedent xAnt_alt)).hasValue effect xEff_actual then 0 else 1

Bridge: under IsDeterministic, whetherCause is the {0,1} indicator of whether the counterfactual outcome differs from xEff_actual. The graded B&G W collapses to the discrete Lewis-style "would the effect have been different?" — exactly the collapse Lassiter §3 / Lucas-Kemp predict for high-stability deterministic systems.

Port of @cite{nadathur-2024} Definition 10b to V2. Specialized to BoolSEM (the binary substrate the original definition was given on); polymorphic generalization to multi-valued α can come if a consumer needs it.

@[reducible, inline]

abbrev Core.Causal.BoolSEM.developsToTrue {V : Type u_1} (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] (s : Valuation fun (x : V) => Bool) (v : V) : Prop

BoolSEM-flavored developsToValue: vertex v develops to true.

Equations

• M.developsToTrue s v = Core.Causal.SEM.developsToValue M s v true

@[reducible, inline]

abbrev Core.Causal.BoolSEM.causallySufficient {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] (s : Valuation fun (x : V) => Bool) (cause effect : V) : Prop

BoolSEM-flavored causallySufficient: setting cause = true develops effect = true. Matches old Core.Causal.causallySufficient semantics.

Equations

• M.causallySufficient s cause effect = Core.Causal.SEM.causallySufficient M s cause true effect true

@[reducible, inline]

abbrev Core.Causal.BoolSEM.manipulates {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] (s : Valuation fun (x : V) => Bool) (cause effect : V) : Prop

BoolSEM-flavored manipulates: cause's value (true vs false) flips effect's value under developDet.

Equations

• M.manipulates s cause effect = Core.Causal.SEM.manipulates M s cause true false effect

def Core.Causal.BoolSEM.hasDirectLaw {V : Type u_1} (M : BoolSEM V) (cause effect : V) : Prop

Direct causal connection: cause is a parent of effect in the SEM's graph. Pure structural predicate (no developDet); fully decidable structurally via Finset.decidableMem.

Equations

• M.hasDirectLaw cause effect = (cause ∈ M.graph.parents effect)

@[implicit_reducible]

instance Core.Causal.BoolSEM.instDecidableHasDirectLaw {V : Type u_1} [DecidableEq V] (M : BoolSEM V) (cause effect : V) : Decidable (M.hasDirectLaw cause effect)

Equations

• M.instDecidableHasDirectLaw cause effect = Core.Causal.BoolSEM.instDecidableHasDirectLaw._aux_1 M cause effect

developDetOn-flavored variants

The causallySufficient and completesForEffect predicates above use the canonical developDet (per-vertex WellFounded.fix), which reduces only through developDetVtx_unfold lemmas. Paper-replication study files with concrete inductive vertex types prefer the developDetOn-based variants below, which iterate a stepOnceDetOn on an explicit vertex list and reduce structurally by rfl after unfold.

Choose:

• causallySufficient / completesForEffect — polymorphic, downstream-derivable;
• causallySufficientOn / completesForEffectOn — concrete, kernel-rfl-reducible.

noncomputable def Core.Causal.BoolSEM.causallySufficientOn {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [SEM.IsDeterministic M] (vs : List V) (bg : Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Prop

developDetOn-flavored sufficiency: with cause = true under bg, iterating stepOnceDetOn on vs n times produces effect = true.

Equations

• M.causallySufficientOn vs bg n cause effect = (Core.Causal.SEM.developDetOn M vs n (bg.extend cause true)).hasValue effect true

noncomputable def Core.Causal.BoolSEM.completesForEffectOn {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [SEM.IsDeterministic M] (vs : List V) (bg : Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Prop

developDetOn-flavored completion: sufficiency + but-for. The developDetOn analogue of Semantics.Causation.CCSelection.completesForEffect.

Equations

• M.completesForEffectOn vs bg n cause effect = (M.causallySufficientOn vs bg n cause effect ∧ ¬(Core.Causal.SEM.developDetOn M vs n (bg.extend cause false)).hasValue effect true)

@[implicit_reducible]

noncomputable instance Core.Causal.BoolSEM.instDecidableCausallySufficientOn {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [SEM.IsDeterministic M] (vs : List V) (bg : Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Decidable (M.causallySufficientOn vs bg n cause effect)

Equations

• M.instDecidableCausallySufficientOn vs bg n cause effect = Classical.dec (M.causallySufficientOn vs bg n cause effect)

@[implicit_reducible]

noncomputable instance Core.Causal.BoolSEM.instDecidableCompletesForEffectOn {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [SEM.IsDeterministic M] (vs : List V) (bg : Valuation fun (x : V) => Bool) (n : ℕ) (cause effect : V) : Decidable (M.completesForEffectOn vs bg n cause effect)

Equations

• M.instDecidableCompletesForEffectOn vs bg n cause effect = Classical.dec (M.completesForEffectOn vs bg n cause effect)

theorem Core.Causal.BoolSEM.manipulates_of_developDetOn_ne {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] {s : Valuation fun (x : V) => Bool} (vs : List V) (n : ℕ) {cause effect : V} (y1 y2 : Bool) (h1 : (SEM.developDetOn M vs n (s.extend cause true)).hasValue effect y1) (h2 : (SEM.developDetOn M vs n (s.extend cause false)).hasValue effect y2) (hne : y1 ≠ y2) : M.manipulates s cause effect

Positive manipulates bridge: if developDetOn produces different explicit values y1 ≠ y2 for cause=true vs cause=false, then manipulates holds.

y1, y2 are explicit (not implicit) so consumers can write exact manipulates_of_developDetOn_ne M (vs := …) (n := …) true false (by decide) (by decide) (by decide) without (by decide) running into metavariable inference issues.

theorem Core.Causal.BoolSEM.not_manipulates_of_developDetOn_eq {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] {s : Valuation fun (x : V) => Bool} (vs : List V) (n : ℕ) {cause effect : V} (y : Bool) (h1 : (SEM.developDetOn M vs n (s.extend cause true)).hasValue effect y) (h2 : (SEM.developDetOn M vs n (s.extend cause false)).hasValue effect y) : ¬M.manipulates s cause effect

Negative manipulates bridge: if developDetOn produces the same explicit value y for cause=true and cause=false, then manipulates is false.

y is explicit (not implicit) so consumers can write exact not_manipulates_of_developDetOn_eq M (vs := …) (n := …) true (by decide) (by decide) without metavariable issues.

def Core.Causal.SEM.isConsistentSuper {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (base s' : Valuation α) : Prop

Consistent supersituation check (@cite{nadathur-2024} Def 9b): s' is consistent with base under M iff every value s' fixes on a vertex undetermined in base agrees with what per-vertex development of base would produce.

Refactored from the previous ∀ yv ≠ xv, ¬ hasValue form: in the deterministic case the vertex's value is unique, so the condition simplifies to "the s'-fixed value equals the developed value."

Equations

• M.isConsistentSuper base s' = ∀ (x : V) (xv : α x), base.get x = none → s'.get x = some xv → M.developDetVtx base x = xv

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instDecidableIsConsistentSuper {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (base s' : Valuation α) : Decidable (M.isConsistentSuper base s')

Equations

• M.instDecidableIsConsistentSuper base s' = Classical.dec (M.isConsistentSuper base s')

def Core.Causal.SEM.causallyNecessary.precondition {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

Precondition (@cite{nadathur-2024} Def 10b): neither cause = xC nor effect = xE is already entailed by s under M. Stated directly via developDetVtx.

Equations

• Core.Causal.SEM.causallyNecessary.precondition M s cause xC effect xE = (M.developDetVtx s cause ≠ xC ∧ M.developDetVtx s effect ≠ xE)

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.causallyNecessary.instDecidablePrecondition {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (precondition M s cause xC effect xE)

Equations

• Core.Causal.SEM.causallyNecessary.instDecidablePrecondition M s cause xC effect xE = Classical.dec (Core.Causal.SEM.causallyNecessary.precondition M s cause xC effect xE)

def Core.Causal.SEM.causallyNecessary.achievable {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

Achievability clause (i) of @cite{nadathur-2024} Def 10b. Abstract quantification over Valuation α: there exists a supersituation of s.extend cause xC (consistent with the per-vertex development) under which effect develops to xE.

Concrete proofs supply the existential witness directly (typically just the extended valuation itself, or a minimal further extension).

Equations

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

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.causallyNecessary.instDecidableAchievable {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (achievable M s cause xC effect xE)

Equations

• Core.Causal.SEM.causallyNecessary.instDecidableAchievable M s cause xC effect xE = Classical.dec (Core.Causal.SEM.causallyNecessary.achievable M s cause xC effect xE)

def Core.Causal.SEM.causallyNecessary.noAlternative {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

But-for clause (ii) of @cite{nadathur-2024} Def 10b. Abstract quantification: every consistent supersituation of s that doesn't fix cause = xC must fail to develop effect = xE.

Concrete proofs case-analyze on which free vertices s' fixes; the isConsistentSuper clause forces those values to agree with developDetVtx M s, narrowing the cases to a finite enumeration.

Equations

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

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.causallyNecessary.instDecidableNoAlternative {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (noAlternative M s cause xC effect xE)

Equations

• Core.Causal.SEM.causallyNecessary.instDecidableNoAlternative M s cause xC effect xE = Classical.dec (Core.Causal.SEM.causallyNecessary.noAlternative M s cause xC effect xE)

def Core.Causal.SEM.causallyNecessary {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

Causal Necessity (@cite{nadathur-2024} Definition 10b), polymorphic over value types.

⟨cause, xC⟩ is causally necessary for ⟨effect, xE⟩ relative to s under M iff:

• Precondition: s does not develop cause to xC nor effect to xE.
• (i) Achievability: some consistent supersituation of s.extend cause xC develops effect to xE.
• (ii) But-for: no consistent supersituation of s lacking cause = xC develops effect to xE.

Supersedes the simple but-for test from @cite{nadathur-lauer-2020} Definition 24. Refactored from the previous allExtensions/freeExtensions enumeration to abstract Valuation α quantification — see Counterfactual.lean module docstring.

Equations

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

@[implicit_reducible]

noncomputable instance Core.Causal.SEM.instDecidableCausallyNecessary {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (M.causallyNecessary s cause xC effect xE)

Equations

• M.instDecidableCausallyNecessary s cause xC effect xE = Classical.dec (M.causallyNecessary s cause xC effect xE)

@[reducible, inline]

abbrev Core.Causal.BoolSEM.causallyNecessary {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] (s : Valuation fun (x : V) => Bool) (cause effect : V) : Prop

BoolSEM-flavored causallyNecessary: setting cause = true is necessary (Def 10b) for effect = true.

Equations

• M.causallyNecessary s cause effect = Core.Causal.SEM.causallyNecessary M s cause true effect true

@[implicit_reducible]

noncomputable instance Core.Causal.BoolSEM.instDecidableCausallyNecessary {V : Type u_1} [DecidableEq V] (M : BoolSEM V) [M.graph.IsDAG] [SEM.IsDeterministic M] (s : Valuation fun (x : V) => Bool) (cause effect : V) : Decidable (M.causallyNecessary s cause effect)

Equations

• M.instDecidableCausallyNecessary s cause effect = Classical.dec (M.causallyNecessary s cause effect)