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 eager-totally developing produces xE at effect — the bare sufficiency clause over developDetVtx, kept for consumers that want plain development entailment (Glass, SBH, INUS, CC-selection).

• causallyEntails M s v x: [Nad23b] Definition 5 — the strict T_D fixed point (developDetVtx?) assigns x to v. The paper-faithful predicates below are stated over this notion.

• isConsistentSuper M base s': Definition 9b, "not the opposite" form.

• causallyNecessary M s cause xC effect xE: Definition 10b — preamble + achievability + no-alternative, with supersituations quantified over exogenous settlements (see IsExogenousSettlement for why the literal quantification is unfaithful to the paper's own verdicts).

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

Computability

The canonical predicates are noncomputable (WellFounded.fix); Decidable instances on them are Classical.dec and do not support decide. Concrete claims go through the fuel bridge instead: causallyEntails_iff_fuel and causallyNecessary_iff_fuel rewrite to the kernel-reducible developDetVtxFuel / causallyNecessaryFuel forms given a per-model rank certificate (the depth function already supplied to IsDAG.of_depth), after which decide evaluates them — including the Def 10b supersituation quantifiers, which range over the finite valuation space. Study idiom:

theorem foo : makeSem M bg c true e true := ⟨fun h => absurd (entails_iff.mp h) (by decide), entails_iff.mpr (by decide)⟩

with entails_iff a one-line per-model instantiation of causallyEntails_iff_fuel.

def Causation.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 Causation.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 Causation.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 [NL20] Definition 23's sufficiency clause (the development of s + (cause = xC) fixes the effect); Def 23's non-inevitability precondition (clause a) is not yet represented — see the module TODO. 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 Causation.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)

theorem Causation.SEM.developsToValue_iff {V : Type u_1} {α : V → Type u_2} (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.

theorem Causation.SEM.causallySufficient_iff {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) : M.causallySufficient s cause xC effect xE ↔ M.developsToValue (s.extend cause xC) effect xE

causallySufficient unfolds to developsToValue of the extended valuation.

def Causation.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 Causation.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 ([Las17b]): "Rewind to the antecedent's causal layer, Revise the antecedent, selectively Regenerate descendants while preserving causally-independent observations." Subsumes: - [Lew73a] / [NL20] deterministic counterfactuals (Dirac specialization) - [BG25] W/H/S aspects (graded probability) - [Las17b] probabilistic counterfactuals with overt probability operators

Key insight: under the high-stability assumption ([lucas-kemp-2015]),
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 (discussed in
[lassiter-2017-probabilistic-language]): 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 Causation.SEM.cfSeed {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) (observed : Valuation α) (antecedent : V) (xAnt : α antecedent) : Valuation α

Counterfactual seed ([Las17b] 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 Causation.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):

• whetherCause ([BG25] Eq 1, graded)
• sufficientCause ([BG25] Eq 3, graded)
• CaoWhiteLassiter2025.probSufficiency — [CWL25]'s SUF, i.e. Pearl's probability of sufficiency ([Pea19]): the counterfactual probability of the effect under intervening the cause, via abduction–action–prediction (not plain interventional probability)
• Lassiter probabilistic counterfactuals with overt probability operators

Equations

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

noncomputable def Causation.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 ([BG25] 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 — the canonical PMF.probOfSet of the complement event {v | ¬ v.hasValue effect xEff_actual} under the counterfactual distribution.

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

Equations

• M.whetherCause observed antecedent xAnt_alt effect xEff_actual = (M.counterfactualSimulate observed antecedent xAnt_alt).probOfSet {v : Causation.Valuation α | ¬v.hasValue effect xEff_actual}

noncomputable def Causation.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 ([BG25] 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. Definitionally whetherCause at the alternatives-removed background — the removal operation itself is the caller's responsibility (below).

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 Causation.SEM.counterfactualSimulate_eq_pure_of_deterministic {V : Type u_1} {α : V → Type u_2} [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 Causation.SEM.whetherCause_eq_indicator_of_deterministic {V : Type u_1} {α : V → Type u_2} [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 [Las17b] and [LK15] predict for high-stability deterministic systems.

@[reducible, inline]

abbrev Causation.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 Causation.causallySufficient semantics.

Equations

• M.causallySufficient s cause effect = Causation.SEM.causallySufficient M s cause true effect true

@[reducible, inline]

abbrev Causation.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 = Causation.SEM.manipulates M s cause true false effect

def Causation.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 Causation.BoolSEM.instDecidableHasDirectLaw {V : Type u_1} [DecidableEq V] (M : BoolSEM V) (cause effect : V) : Decidable (M.hasDirectLaw cause effect)

Equations

• M.instDecidableHasDirectLaw cause effect = Causation.BoolSEM.instDecidableHasDirectLaw._aux_1 M cause effect

Statement-level predicates are the canonical developDet-based forms above (causallySufficient, CCSelection.completesForEffect); concrete proofs compute a developDetOn iteration with decide and lift through the soundness bridge (developDet_hasValue_of_developDetOn_hasValue) or the CCSelection.*_of_developDetOn helpers. The former (vs, n)-indexed statement forms (causallySufficientOn/completesForEffectOn) were removed: they leaked the vertex list and fuel into theorem statements, and their negations asserted facts about an iteration trace rather than the causal notion.

theorem Causation.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 Causation.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 Causation.SEM.causallyEntails {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : Prop

Causal entailment ([Nad23b] Def 5): the strict T_D fixed point relative to s assigns x to v ("s ⊨_D ⟨v, x⟩"). Stated over the partial developDetVtx? — an undetermined exogenous vertex entails nothing, and an inner vertex entails nothing while any parent is u-valued. Contrast the eager-total developsToValue above.

Equations

• M.causallyEntails s v x = (M.developDetVtx? s v = some x)

@[implicit_reducible]

noncomputable instance Causation.SEM.instDecidableCausallyEntails {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : Decidable (M.causallyEntails s v x)

Equations

• M.instDecidableCausallyEntails s v x = Classical.dec (M.causallyEntails s v x)

theorem Causation.SEM.causallyEntails_iff_fuel {V : Type u_1} {α : V → Type u_2} [DecidableEq V] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (rank : V → ℕ) (hrank : ∀ {u v : V}, u ∈ M.graph.parents v → rank u < rank v) {n : ℕ} {v : V} (hn : rank v < n) (s : Valuation α) (x : α v) : M.causallyEntails s v x ↔ M.developDetVtxFuel s n v = some x

Transfer a fuel-mirror computation to causallyEntails (both polarities, via the fuel bridge). The study idiom for concrete claims: (causallyEntails_iff_fuel M rank @hrank hn s v x).mpr (by decide).

theorem Causation.SEM.causallySufficient_of_causallyEntails {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} (h : M.causallyEntails (s.extend cause xC) effect xE) : M.causallySufficient s cause xC effect xE

Strict causal entailment of the extended background implies the bare eager-total sufficiency predicate (causallySufficient): the partial development refines the total one wherever it resolves.

theorem Causation.SEM.causallyEntails_unique {V : Type u_1} {α : V → Type u_2} [DecidableEq V] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s : Valuation α} {v : V} {x y : α v} (hx : M.causallyEntails s v x) (hy : M.causallyEntails s v y) : x = y

Causal entailment is functional: a vertex entails at most one value.

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

Consistent supersituation ([Nad23b] Def 9b), faithful "not the opposite" form: s' extends base, and for every vertex s' newly fixes, base does not causally entail a different value there. Def 9b restricts the condition to inner variables; that restriction is automatic here, since developDetVtx? is none at undetermined exogenous vertices.

Equations

• M.isConsistentSuper base s' = (base.le s' ∧ ∀ (x : V) (xv : α x), base.get x = none → s'.get x = some xv → ∀ (yv : α x), yv ≠ xv → ¬M.causallyEntails base x yv)

@[implicit_reducible]

noncomputable instance Causation.SEM.instDecidableIsConsistentSuper {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (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')

theorem Causation.SEM.isConsistentSuper_self {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) : M.isConsistentSuper s s

Every valuation is a consistent supersituation of itself.

theorem Causation.SEM.causallyEntails_mono {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {s s' : Valuation α} (hcons : M.isConsistentSuper s s') {v : V} {x : α v} (h : M.causallyEntails s v x) : M.causallyEntails s' v x

Determinations cannot be undone ([Nad23b] Def 2 prose): causal entailment is monotone under consistent supersituations — whatever s causally entails, any Def-9b-consistent extension of s still causally entails.

def Causation.SEM.IsExogenousSettlement {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] (M : SEM V α) (base s' : Valuation α) : Prop

Exogenous settlement: s' extends base by fixing only exogenous (parentless) vertices.

Project-canonical restriction on Def 10b's supersituation quantifiers. Quantifying over all consistent supersituations (the literal Def 9b/10b reading) falsifies the paper's own §6.1.1 verdicts: relative to the Dreyfus background, fixing the undetermined inner vertex MSG (plus LST, ¬BRK) is Def-9b-consistent and reaches COM without entailing NRV, contradicting the claim that ⟨NRV,1⟩ is causally necessary for ⟨COM,1⟩. The paper's worked example (21b) considers only background settlements ("the only such available"); this definition makes that reading explicit.

Equations

• M.IsExogenousSettlement base s' = (base.le s' ∧ ∀ (v : V), base.get v = none → (s'.get v).isSome = true → M.graph.parents v = ∅)

theorem Causation.SEM.Valuation.le_iff_forall {V : Type u_1} {α : V → Type u_2} [DecidableValuation α] {s₁ s₂ : Valuation α} : s₁.le s₂ ↔ ∀ (v : V), (s₁.get v).isSome = true → s₁.get v = s₂.get v

Information order, executable characterization.

@[implicit_reducible]

instance Causation.SEM.instDecidableLeOfDecidableEqOfFintypeOfDecidableValuation {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [Fintype V] [DecidableValuation α] (s₁ s₂ : Valuation α) : Decidable (s₁.le s₂)

Equations

• Causation.SEM.instDecidableLeOfDecidableEqOfFintypeOfDecidableValuation s₁ s₂ = decidable_of_iff (∀ (v : V), (s₁.get v).isSome = true → s₁.get v = s₂.get v) ⋯

@[implicit_reducible]

instance Causation.SEM.instDecidableIsExogenousSettlementOfDecidableEqOfFintype {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [Fintype V] [DecidableValuation α] (M : SEM V α) (base s' : Valuation α) : Decidable (M.IsExogenousSettlement base s')

Equations

• M.instDecidableIsExogenousSettlementOfDecidableEqOfFintype base s' = Causation.SEM.instDecidableIsExogenousSettlementOfDecidableEqOfFintype._aux_1 M base s'

theorem Causation.SEM.IsExogenousSettlement.of_extend {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] {M : SEM V α} {s s' : Valuation α} {p : V} {xP : α p} (hexo : M.graph.parents p = ∅) (hp : s.get p = none) (h : M.IsExogenousSettlement (s.extend p xP) s') : M.IsExogenousSettlement s s'

An exogenous settlement of an extension at a fresh exogenous vertex is an exogenous settlement of the base.

theorem Causation.SEM.IsExogenousSettlement.isConsistentSuper {V : Type u_1} {α : V → Type u_2} [DecidableEq V] [DecidableValuation α] {M : SEM V α} [M.graph.IsDAG] [M.IsDeterministic] {base s' : Valuation α} (h : M.IsExogenousSettlement base s') : M.isConsistentSuper base s'

Exogenous settlements are automatically Def-9b-consistent: a newly fixed vertex is parentless and undetermined in base, so base causally entails nothing about it.

def Causation.SEM.causallyNecessary.precondition {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

Preamble of Definition 10 ([Nad23b], with footnote 8's rationale): the background entails neither the cause fact nor the effect fact. Shared by Def 10a (sufficiency, see Implicative.manageSem) and Def 10b (necessity, below).

Equations

• Causation.SEM.causallyNecessary.precondition M s cause xC effect xE = (¬M.causallyEntails s cause xC ∧ ¬M.causallyEntails s effect xE)

@[implicit_reducible]

noncomputable instance Causation.SEM.causallyNecessary.instDecidablePrecondition {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 (precondition M s cause xC effect xE)

Equations

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

def Causation.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 Def 10b: some consistent supersituation s' of s + (cause = xC) with effect ∉ dom(s') causally entails effect = xE. Quantified over exogenous settlements (see IsExogenousSettlement); Def 9b consistency is then automatic (IsExogenousSettlement.isConsistentSuper).

Equations

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

@[implicit_reducible]

noncomputable instance Causation.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

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

def Causation.SEM.causallyNecessary.noAlternative {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

No-alternative, clause (ii) of Def 10b in positive-implication form: every consistent supersituation of s (exogenous settlement, effect ∉ dom(s')) that causally entails effect = xE also causally entails cause = xC — every consistent path to the effect goes through the cause. The paper's exclusion s' ⊭ ⟨X,x⟩ is the developed entailment, not the syntactic s'.get cause ≠ some xC.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.SEM.causallyNecessary.instDecidableNoAlternative {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 (noAlternative M s cause xC effect xE)

Equations

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

def Causation.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 ([Nad23b] Definition 10b) over the strict T_D development, polymorphic over value types:

• Preamble: s entails neither cause = xC nor effect = xE.
• (i) Achievability: some consistent supersituation of s + (cause = xC) not fixing the effect entails effect = xE.
• (ii) No-alternative: every consistent supersituation of s not fixing the effect that entails effect = xE entails cause = xC.

Supersituations are quantified over exogenous settlements — see IsExogenousSettlement for why the literal Def 9b/10b quantification is unfaithful to the paper's own verdicts.

Equations

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

@[implicit_reducible]

noncomputable instance Causation.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)

def Causation.SEM.causallyNecessaryFuel {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.IsDeterministic] (n : ℕ) (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Prop

Executable mirror of causallyNecessary at fuel n: every causallyEntails clause replaced by its developDetVtxFuel form. Genuinely decidable (the supersituation quantifiers range over the Pi-Fintype of valuations). Connected to the canonical predicate by causallyNecessary_iff_fuel.

Equations

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

@[implicit_reducible]

instance Causation.SEM.instDecidableCausallyNecessaryFuelOfFintype {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (M : SEM V α) [M.IsDeterministic] (n : ℕ) (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : Decidable (M.causallyNecessaryFuel n s cause xC effect xE)

Equations

• M.instDecidableCausallyNecessaryFuelOfFintype n s cause xC effect xE = id inferInstance

theorem Causation.SEM.causallyNecessary_iff_fuel {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (rank : V → ℕ) (hrank : ∀ {u v : V}, u ∈ M.graph.parents v → rank u < rank v) {n : ℕ} (hn : ∀ (v : V), rank v < n) (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) : M.causallyNecessary s cause xC effect xE ↔ M.causallyNecessaryFuel n s cause xC effect xE

The canonical Def 10b coincides with its fuel form once the fuel exceeds a rank function for the graph. Study idiom: (causallyNecessary_iff_fuel M rank @hrank hn s …).mpr (by decide).

@[reducible, inline]

abbrev Causation.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 = Causation.SEM.causallyNecessary M s cause true effect true

@[implicit_reducible]

noncomputable instance Causation.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)