Causal sufficiency and causal necessity

Nadathur and Lauer draw on two relations of causal dependence for the meanings of periphrastic causatives, both over the strict development of an observation (CausalModel.CausallyEntails). A fact is causally sufficient for another relative to a background when the background does not settle the effect but, with the cause added, does. A fact is causally necessary for another when the background does not settle the effect, some supersituation of the background with the cause settles the effect, and every supersituation of the background that settles the effect settles the cause.

Main definitions

• CausalModel.CausallySufficient: Nadathur and Lauer's causal sufficiency
• CausalModel.CausallyNecessary: Nadathur and Lauer's causal necessity, over a given relation of supersituation
• CausalModel.IsExogenousSettlement: an extension of an observation at exogenous variables

Main results

• CausalModel.CausallySufficient.reflTransGen: a cause sufficient for an effect is its ancestor
• CausalModel.CausallySufficient.solve_eq, CausalModel.CausallyNecessary.solve_eq: in every context where the background holds, a sufficient cause brings its effect about, and an effect needs its necessary cause
• CausalModel.CausallyEntails.of_isExogenousSettlement: settling exogenous variables settles no less
• CausalModel.isExogenousSettlement_update, CausalModel.IsExogenousSettlement.trans

Implementation notes

Necessity takes the supersituations it quantifies over as a parameter: every supersituation, (· ≤ ·), for Nadathur and Lauer, and for the worked examples of [Nad23b] the exogenous settlements, the extensions at the variables with no parents that the background leaves open. Over every supersituation, one settling a variable between cause and effect reaches the effect around the cause. In a finite model each relation is decided through the computed strict development (CausalModel.causallyEntails_iff_develop).

References

• [NL20]
• [Nad23b]

def CausalModel.CausallySufficient {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [M.IsAcyclic] [DecidableEq V] (s : (v : V) → Flat (α v)) (c : V) (x : α c) (e : V) (y : α e) : Prop

M.CausallySufficient s c x e y says that c = x is causally sufficient for e = y relative to the background s. The background does not settle the effect, and the background together with the cause does.

Equations

• M.CausallySufficient s c x e y = (¬M.CausallyEntails s e y ∧ M.CausallyEntails (Function.update s c ↑x) e y)

def CausalModel.CausallyNecessary {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [M.IsAcyclic] [DecidableEq V] (r : ((v : V) → Flat (α v)) → ((v : V) → Flat (α v)) → Prop) (s : (v : V) → Flat (α v)) (c : V) (x : α c) (e : V) (y : α e) : Prop

M.CausallyNecessary r s c x e y says that c = x is causally necessary for e = y relative to the background s, where r s s' says that s' is a supersituation of s. The background does not settle the effect; some supersituation of the background with the cause added, leaving the effect open, settles the effect; and every supersituation of the background leaving the effect open that settles the effect settles the cause.

Equations

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

def CausalModel.IsExogenousSettlement {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [M.IsAcyclic] (s s' : (v : V) → Flat (α v)) : Prop

s' settles the observation s further at exogenous variables only, those with no parents that the strict development of s leaves open.

Equations

• M.IsExogenousSettlement s s' = (s ≤ s' ∧ ∀ (v : V), s v = ⊥ → s' v ≠ ⊥ → (∀ (w : V), ¬M.graph.Adj w v) ∧ ∀ (x : α v), ¬M.CausallyEntails s v x)

theorem CausalModel.CausallySufficient.reflTransGen {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] {s : (v : V) → Flat (α v)} {c : V} {x : α c} {e : V} {y : α e} (h : M.CausallySufficient s c x e y) : Relation.ReflTransGen M.graph.Adj c e

A cause sufficient for an effect is an ancestor of it: without a path from the cause, adding it leaves the effect as the background left it.

theorem CausalModel.CausallyEntails.of_isExogenousSettlement {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] {s s' : (v : V) → Flat (α v)} (hs : M.IsExogenousSettlement s s') {v : V} {x : α v} (h : M.CausallyEntails s v x) : M.CausallyEntails s' v x

Settling exogenous variables settles no less. What the strict development of an observation settles, that of any exogenous settlement of it settles too.

theorem CausalModel.isExogenousSettlement_update {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] {s : (v : V) → Flat (α v)} {p : V} (hroot : ∀ (w : V), ¬M.graph.Adj w p) (hopen : ∀ (x : α p), ¬M.CausallyEntails s p x) (x : α p) : M.IsExogenousSettlement s (Function.update s p ↑x)

Settling an open exogenous variable is an exogenous settlement.

theorem CausalModel.IsExogenousSettlement.refl {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] (s : (v : V) → Flat (α v)) : M.IsExogenousSettlement s s

Every observation is an exogenous settlement of itself.

theorem CausalModel.IsExogenousSettlement.eq_bot {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] {s s' : (v : V) → Flat (α v)} (h : M.IsExogenousSettlement s s') {v : V} (hv : s v = ⊥) (hpar : ∃ (w : V), M.graph.Adj w v) : s' v = ⊥

An exogenous settlement leaves open every variable with a parent that the observation leaves open.

theorem CausalModel.IsExogenousSettlement.trans {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] {s s' s'' : (v : V) → Flat (α v)} (h₁ : M.IsExogenousSettlement s s') (h₂ : M.IsExogenousSettlement s' s'') : M.IsExogenousSettlement s s''

Exogenous settlements compose.

Truth in the contexts of a background

A relation of causal dependence relative to a background constrains the actual world of every context where the background holds.

theorem CausalModel.CausallySufficient.solve_eq {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] [∀ (v : V), Nonempty (α v)] {s : (v : V) → Flat (α v)} {c : V} {x : α c} {e : V} {y : α e} {u : U} (h : M.CausallySufficient s c x e y) (hu : u ∈ M.contexts s) (hc : M.solve ⊥ u c = x) : M.solve ⊥ u e = y

A cause sufficient for an effect relative to a background brings the effect about in every context where the background and the cause hold.

theorem CausalModel.CausallyNecessary.solve_eq {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] [∀ (v : V), Nonempty (α v)] {s : (v : V) → Flat (α v)} {c : V} {x : α c} {e : V} {y : α e} {u : U} [M.ContextAtRoots] (h : M.CausallyNecessary M.IsExogenousSettlement s c x e y) (hu : u ∈ M.contexts s) (he : M.solve ⊥ u e = y) : M.solve ⊥ u c = x

When the context reaches the model only at its roots, a cause necessary for an effect over the exogenous settlements of a background holds in every context where the background and the effect hold. Settling every open and unsettled root at its value in the context develops to the context's actual world, so it settles the effect, and necessity makes it settle the cause.

@[instance_reducible]

instance CausalModel.instDecidableCausallySufficient {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (c : V) (x : α c) (e : V) (y : α e) : Decidable (M.CausallySufficient s c x e y)

Equations

• CausalModel.instDecidableCausallySufficient s c x e y = { decide := decide ¬M.CausallyEntails s e y && decide (M.CausallyEntails (Function.update s c ↑x) e y), reflects_decide := ⋯ }

@[instance_reducible]

instance CausalModel.instDecidableIsExogenousSettlement {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] [(v : V) → Fintype (α v)] (s s' : (v : V) → Flat (α v)) : Decidable (M.IsExogenousSettlement s s')

Equations

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

@[reducible]

def CausalModel.fintypePartialAssignment {V : Type u_2} {α : V → Type u_3} [DecidableEq V] [Fintype V] [(v : V) → Fintype (α v)] : Fintype ((v : V) → Flat (α v))

Partial assignments over finitely many variables of finite types are finitely many. Not an instance: a Fintype instance on Flat would change how decide evaluates flat-valued functions, so necessity installs this one locally.

Equations

• CausalModel.fintypePartialAssignment = { elems := CausalModel.fintypePartialAssignment._aux_1, complete := ⋯ }

@[instance_reducible]

instance CausalModel.instDecidableCausallyNecessary {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [M.IsAcyclic] [DecidableEq V] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] [(v : V) → Fintype (α v)] (r : ((v : V) → Flat (α v)) → ((v : V) → Flat (α v)) → Prop) [(s s' : (v : V) → Flat (α v)) → Decidable (r s s')] (s : (v : V) → Flat (α v)) (c : V) (x : α c) (e : V) (y : α e) : Decidable (M.CausallyNecessary r s c x e y)

Equations

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