Causal Closure Operator

@cite{nadathur-lauer-2020}

The algebraic root of causal reasoning: for positive dynamics, normalDevelopment is a closure operator on (Situation, trueLE).

The Three Axioms

For positive dynamics dyn with fuel f:

1. Extensive: s ≤ cl(s) — development only adds truths
2. Monotone: s₁ ≤ s₂ → cl(s₁) ≤ cl(s₂) — more input, more output
3. Idempotent: cl(cl(s)) = cl(s) — fixpoint stability

Why This Matters

Causal sufficiency IS closure membership: causallySufficient dyn s t c iff c = true ∈ cl(s + {t = true}). This single observation unifies ability modals (be able), implicative verbs (manage), and degree constructions (enough/too) — all are membership tests in different closures with different triggers.

Levels of Abstraction

• Level 1 (this file): ClosureOperator Situation for positive dynamics
• Level 2 (future): Galois connection (cl, ι) decomposing cl = ι ∘ l
• Level 3 (future): Scott Information System unifying all situation-like objects in linglib (causal, dynamic, modal, presuppositional)

instance Core.CausalClosure.instPreorderSituation : Preorder StructuralEquationModel.Situation

The true-content preorder on Situation: s₁ ≤ s₂ iff every variable that is true in s₁ is also true in s₂.

This is NOT antisymmetric: two situations can agree on all true values while differing on false/undetermined assignments. Hence Preorder, not PartialOrder.

Equations

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

structure Core.CausalClosure.PositiveDynamics : Type

A PositiveDynamics bundles causal dynamics with:

• A proof that all laws have positive preconditions and effects (no inhibitory connections)
• A fuel budget for fixpoint iteration
• A proof that fuel is sufficient to always reach a fixpoint

Positive dynamics are the structural condition under which normalDevelopment forms a closure operator. The reachesFP field guarantees that fuel is enough for the dynamics to converge from any starting situation — without this, idempotency of the closure operator cannot be proved.

• dynamics : StructuralEquationModel.CausalDynamics

  The underlying causal dynamics

• positive : StructuralEquationModel.isPositiveDynamics self.dynamics = true

  Proof of positivity

• fuel : ℕ

  Fuel for fixpoint iteration (default: 100)

• reachesFP (s : StructuralEquationModel.Situation) : StructuralEquationModel.isFixpoint self.dynamics (StructuralEquationModel.normalDevelopment self.dynamics s self.fuel) = true

  Fuel is sufficient: normalDevelopment always reaches a fixpoint.

def Core.CausalClosure.PositiveDynamics.cl (pd : PositiveDynamics) : StructuralEquationModel.Situation →o StructuralEquationModel.Situation

The closure function as a monotone map on (Situation, trueLE).

pd.cl s = normalDevelopment pd.dynamics s pd.fuel

Monotonicity: if s₁ ≤ s₂ then cl(s₁) ≤ cl(s₂). This follows from the fact that positive dynamics only have positive preconditions, so more true values in the input means more law firings.

Equations

• pd.cl = { toFun := fun (s : Core.StructuralEquationModel.Situation) => Core.StructuralEquationModel.normalDevelopment pd.dynamics s pd.fuel, monotone' := ⋯ }

def Core.CausalClosure.PositiveDynamics.closureOp (pd : PositiveDynamics) : ClosureOperator StructuralEquationModel.Situation

normalDevelopment for positive dynamics is a closure operator.

• Extensive (proved): s ≤ cl(s) — causal development only adds truths.
• Monotone (proved): more input → more output.
• Idempotent (proved): cl(cl(s)) = cl(s) — the result of development is itself a fixpoint and further development is a no-op.

Idempotency follows from the reachesFP field of PositiveDynamics: the first application reaches a fixpoint, and normalDevelopment_of_fixpoint shows that running from a fixpoint is a no-op.

Equations

• pd.closureOp = { toOrderHom := pd.cl, le_closure' := ⋯, idempotent' := ⋯, IsClosed := fun (x : Core.StructuralEquationModel.Situation) => pd.cl.toFun x = x, isClosed_iff := ⋯ }

theorem Core.CausalClosure.sufficiency_as_closure_membership (dyn : StructuralEquationModel.CausalDynamics) (s : StructuralEquationModel.Situation) (trigger complement : StructuralEquationModel.Variable) : StructuralEquationModel.causallySufficient dyn s trigger complement = (StructuralEquationModel.normalDevelopment dyn (s.extend trigger true)).hasValue complement true

Causal sufficiency is closure membership.

causallySufficient dyn s trigger complement holds iff complement = true ∈ cl(s ⊕ {trigger = true}).

This is the deep structural reason that ability modals, implicative verbs, and degree constructions all work the same way: they all reduce to asking whether a complement variable is in the closure of a background situation extended with a trigger.

def Core.CausalClosure.IsCausalFixpoint (pd : PositiveDynamics) (s : StructuralEquationModel.Situation) : Prop

A situation is causally closed under pd if it is a fixed point of the closure operator: no further causal development changes it.

These are the situations where all consequences of all present causes have already been computed.

Equations

• Core.CausalClosure.IsCausalFixpoint pd s = (pd.closureOp s = s)