Causal Reasoning & Deontic Logic
Formal frameworks for reasoning about causes, effects, counterfactuals, and normative obligations.
Routing
- USE FOR: Causal reasoning, counterfactual analysis, and deontic logic for AI systems. Use for formalizing cause-effect relationships (Pearl's hierarchy), interventional reasoning, structural causal models, counterfactual simulation, obligation/permission/prohibition reasoning, normative systems, and legal/ethical rule formalization in Lean 4.
- DO NOT USE FOR: formalising those models in Lean (use @lean-causal-reasoning); agentic AI behaviour (use @ai-agentic-evolving); commonsense reasoning (use @ai-commonsense-reasoning).
- TRIGGERS: causal, counterfactual, Pearl hierarchy, deontic, obligation, permission, structural causal model.
Workflow
- Classify the question: causal-effect identification, counterfactual evaluation, deontic-norm modelling, or legal-deontic encoding.
- Pick the matching framework from the body (Pearl's do-calculus, structural causal model, standard deontic logic, dyadic deontic logic).
- Apply the framework to the concrete scenario; document identifiability conditions and norm interactions.
- Hand off: to
@lean-causal-reasoning for Lean encoding, to @applied-legal-reasoning for legal-policy mapping, to @lean-zettelkasten.
Recovery & STOP
- STOP if the question is about Lean formalisation — delegate to
@lean-causal-reasoning.
- STOP if the question is purely legal (not deontic-logic) — delegate to
@applied-legal-reasoning.
- STOP if a causal-effect identifiability claim cannot be established from the body — escalate to
@research-council.
Handoffs
- Predecessors:
agent:gateway, skill:lean-research.
- Successors:
skill:lean-causal-reasoning, skill:lean-knowledge-formalization, skill:lean-zettelkasten.
Part 1 — Pearl's Causal Hierarchy
1.1 Three Levels of Causal Reasoning
| Level |
Name |
Typical Query |
Operator |
Formalization |
| 1 |
Association |
$P(y \mid x)$ |
Conditioning |
Standard probability |
| 2 |
Intervention |
$P(y \mid do(x))$ |
do-calculus |
Truncated factorization |
| 3 |
Counterfactual |
$P(y_x \mid x', y')$ |
Structural equations |
Twin network / abduction |
1.2 Structural Causal Models (SCM)
An SCM $\mathcal{M} = \langle U, V, F, P(U) \rangle$ where:
- $U$: Exogenous (background) variables
- $V$: Endogenous variables
- $F$: Structural equations $V_i = f_i(\text{pa}_i, U_i)$
- $P(U)$: Distribution over exogenous variables
Lean formalization pattern:
structure CausalModel where
vars : Type
exogenous : Type
structural : vars → (vars → Prop) → exogenous → Prop
acyclicity : WellFounded (influences structural)
1.3 do-Calculus
Three rules for identifying causal effects from observational data:
| Rule |
Description |
Condition |
| Rule 1 (Insertion/deletion of observations) |
$P(y \mid do(x), z, w) = P(y \mid do(x), w)$ |
$(Y \perp!!!\perp Z \mid X, W){G{\overline{X}}}$ |
| Rule 2 (Action/observation exchange) |
$P(y \mid do(x), do(z), w) = P(y \mid do(x), z, w)$ |
$(Y \perp!!!\perp Z \mid X, W){G{\overline{X}\underline{Z}}}$ |
| Rule 3 (Insertion/deletion of actions) |
$P(y \mid do(x), do(z), w) = P(y \mid do(x), w)$ |
$(Y \perp!!!\perp Z \mid X, W){G{\overline{X}\overline{Z(W)}}}$ |
1.4 Identifiability Criteria
| Criterion |
Description |
Applicability |
| Back-door |
Adjust for confounders blocking back-door paths |
Common, simple |
| Front-door |
Mediate through intermediate variable |
When no valid adjustment set |
| Instrumental variable |
Exploit exogenous variation |
Econometrics, natural experiments |
| General ID algorithm |
Complete identification algorithm |
Any semi-Markovian model |
Part 2 — Counterfactual Reasoning
2.1 Counterfactual Computation (3 Steps)
- Abduction: Given evidence, infer $P(U \mid \text{evidence})$
- Action: Modify structural equations (intervention)
- Prediction: Compute outcome under modified model
2.2 Potential Outcomes Framework
- Rubin causal model: $Y_i(1), Y_i(0)$ — potential outcomes under treatment/control
- ATE: $\mathbb{E}[Y(1) - Y(0)]$ — average treatment effect
- CATE: $\mathbb{E}[Y(1) - Y(0) \mid X = x]$ — conditional on covariates
- Pipeline mapping: phase transitions as "treatment" effects on quality or safety outcomes
2.3 Counterfactual Stability
When is a counterfactual claim robust?
- Monotonicity: Outcome monotonic in treatment
- Counterfactual stability: Small perturbations in $U$ → small perturbations in counterfactual outcome
- Pipeline example: phase transitions can exhibit threshold or bifurcation-like counterfactual behavior (sudden jumps)
Part 3 — Causal Discovery
3.1 Methods
| Method |
Type |
Assumptions |
Output |
| PC algorithm |
Constraint-based |
Faithfulness, no latent confounders |
CPDAG |
| FCI |
Constraint-based |
Allows latent confounders |
PAG |
| GES |
Score-based |
BIC score, decomposable |
CPDAG |
| NOTEARS |
Continuous optimization |
Acyclicity constraint |
DAG |
| Causal transformers |
Deep learning |
Large observational data |
DAG |
3.2 Causal Graphs in a Verification Pipeline
Example causal DAG:
Stakeholder → Requirements → Phase classification
Phase classification → Quality thresholds → Gate decisions
Gate decisions → Knowledge state → Phase transitions
Phase transitions → System trajectory → Final quality
Part 4 — Deontic Logic
4.1 Standard Deontic Logic (SDL)
| Operator |
Symbol |
Reading |
Formal |
| Obligation |
$O(p)$ |
"It ought to be that $p$" |
$O(p) \equiv \neg P(\neg p)$ |
| Permission |
$P(p)$ |
"It is permitted that $p$" |
$P(p) \equiv \neg O(\neg p)$ |
| Prohibition |
$F(p)$ |
"It is forbidden that $p$" |
$F(p) \equiv O(\neg p)$ |
4.2 Paradoxes and Extensions
| Paradox |
Description |
Resolution |
| Ross's paradox |
$O(p) \to O(p \lor q)$ — obliged to mail → obliged to mail or burn |
Input/output logic |
| Contrary-to-duty |
What obligations apply when one is violated? |
Defeasible deontic logic |
| Free choice |
$P(p \lor q)$ doesn't entail $P(p) \land P(q)$ |
Bilateral norms |
| Chisholm |
Nested conditional obligations conflict |
Dyadic deontic logic |
4.3 Deontic Logic for AI Governance
| Governance Rule |
Deontic Formalization |
| Gate must be passed before advancement |
$O(\text{pass}(g_i) \to \text{before}(\text{phase}_{i+1}))$ |
| Safety envelope must be maintained |
$F(\text{violate}(\text{safety_envelope}))$ |
| Trust must converge |
$O(\text{eventually}(\text{converged}(\tau)))$ |
| Provenance must be recorded |
$O(\text{record}(\text{provenance}(a)))$ for all actions $a$ |
4.4 Input/Output Logic (Makinson & van der Torre)
Input/Output pairs: (a, x) meaning "given input a, output x"
Four operators: out_1 (simple), out_2 (+SI), out_3 (+CT), out_4 (+SI+CT)
Permission: negative (not forbidden) vs positive (explicitly permitted)
Common application: quality gates as I/O norms mapping observation states to action obligations.
Part 5 — Normative Multi-Agent Systems
5.1 Norm Types
| Norm Type |
Example in a verification pipeline |
| Regulative |
"Agents SHALL pass quality gate" |
| Constitutive |
"Meeting threshold counts as passing" |
| Procedural |
"Review must precede approval" |
| Institutional |
"Council member has assessment authority" |
5.2 Norm Compliance
- Regimented: System physically prevents violations (hard constraints)
- Regulated: System detects and sanctions violations (soft constraints with enforcement)
- Example: quality gates can be regimented while trust scores or review confidence are regulated
5.3 Norm Conflict Resolution
| Strategy |
Description |
Common approach |
| Priority ordering |
Higher-priority norm wins |
Safety > quality > efficiency |
| Specificity |
More specific norm overrides general |
Phase-specific thresholds override defaults |
| Temporal |
Later norm supersedes earlier |
RETRO audit can update gates |
Part 6 — Host-Repository Lean Extension Points
Do not assume repository-local Lean modules, tactics, or namespaces exist unless the host repository explicitly provides them. When local modules exist, map them by role:
| Local extension point |
Causal/deontic aspect |
| Provenance / audit trail module |
causal DAG of evidence, intervention tracking |
| Quality-gate module |
deontic obligations and gate-passage requirements |
| Safety module |
safety obligations and prohibited envelope violations |
| Classification module |
causal model of classification → gate → transition |
| Tactic-helper module |
reasoning automation for causal/deontic proofs |
| Dynamics module |
causal dynamics of phase transitions |
Part 7 — Epistemic Mapping
| KK |
KU |
UU |
| SCM theory well-established |
Full do-calculus in Lean 4 |
Causal reasoning under deep uncertainty |
| SDL axiomatized |
I/O logic Lean formalization |
Emergent norms in multi-agent systems |
| Back-door criterion proven |
Automated causal discovery verification |
Counterfactual stability for chaotic systems |
| Pipeline causal DAG identified |
GAI causal reasoning regulation |
Ethical AI as deontic system |
1---2name: ai-causal-deontic3description: USE FOR: Causal reasoning, counterfactual analysis, and deontic logic for AI systems. Use for formalizing cause-effect relationships (Pearl's hierarchy), interventional reasoning, structural causal models, counterfactual simulation, obligation/permission/prohibition reasoning, normative systems, and legal/ethical rule formalization in Lean 4. DO NOT USE FOR: formalising those models in Lean (use @lean-causal-reasoning); agentic AI behaviour (use @ai-agentic-evolving); commonsense reasoning (use @ai-commonsense-reasoning). TRIGGERS: causal, counterfactual, Pearl hierarchy, deontic, obligation, permission, structural causal model.4---567# Causal Reasoning & Deontic Logic89Formal frameworks for reasoning about causes, effects, counterfactuals, and normative obligations.1011---1213## Routing1415- **USE FOR:** Causal reasoning, counterfactual analysis, and deontic logic for AI systems. Use for formalizing cause-effect relationships (Pearl's hierarchy), interventional reasoning, structural causal models, counterfactual simulation, obligation/permission/prohibition reasoning, normative systems, and legal/ethical rule formalization in Lean 4.16- **DO NOT USE FOR:** formalising those models in Lean (use @lean-causal-reasoning); agentic AI behaviour (use @ai-agentic-evolving); commonsense reasoning (use @ai-commonsense-reasoning).17- **TRIGGERS:** causal, counterfactual, Pearl hierarchy, deontic, obligation, permission, structural causal model.1819## Workflow20211. Classify the question: causal-effect identification, counterfactual evaluation, deontic-norm modelling, or legal-deontic encoding.222. Pick the matching framework from the body (Pearl's do-calculus, structural causal model, standard deontic logic, dyadic deontic logic).233. Apply the framework to the concrete scenario; document identifiability conditions and norm interactions.244. Hand off: to `@lean-causal-reasoning` for Lean encoding, to `@applied-legal-reasoning` for legal-policy mapping, to `@lean-zettelkasten`.2526## Recovery & STOP2728- STOP if the question is about Lean formalisation — delegate to `@lean-causal-reasoning`.29- STOP if the question is purely legal (not deontic-logic) — delegate to `@applied-legal-reasoning`.30- STOP if a causal-effect identifiability claim cannot be established from the body — escalate to `@research-council`.3132## Handoffs3334- **Predecessors:** `agent:gateway`, `skill:lean-research`.35- **Successors:** `skill:lean-causal-reasoning`, `skill:lean-knowledge-formalization`, `skill:lean-zettelkasten`.3637---3839## Part 1 — Pearl's Causal Hierarchy4041### 1.1 Three Levels of Causal Reasoning4243| Level | Name | Typical Query | Operator | Formalization |44|---|---|---|---|---|45| 1 | Association | $P(y \mid x)$ | Conditioning | Standard probability |46| 2 | Intervention | $P(y \mid do(x))$ | do-calculus | Truncated factorization |47| 3 | Counterfactual | $P(y_x \mid x', y')$ | Structural equations | Twin network / abduction |4849### 1.2 Structural Causal Models (SCM)5051An SCM $\mathcal{M} = \langle U, V, F, P(U) \rangle$ where:52- $U$: Exogenous (background) variables53- $V$: Endogenous variables54- $F$: Structural equations $V_i = f_i(\text{pa}_i, U_i)$55- $P(U)$: Distribution over exogenous variables5657**Lean formalization pattern:**58```59structure CausalModel where60 vars : Type61 exogenous : Type62 structural : vars → (vars → Prop) → exogenous → Prop63 acyclicity : WellFounded (influences structural)64```6566### 1.3 do-Calculus6768Three rules for identifying causal effects from observational data:6970| Rule | Description | Condition |71|---|---|---|72| Rule 1 (Insertion/deletion of observations) | $P(y \mid do(x), z, w) = P(y \mid do(x), w)$ | $(Y \perp\!\!\!\perp Z \mid X, W)_{G_{\overline{X}}}$ |73| Rule 2 (Action/observation exchange) | $P(y \mid do(x), do(z), w) = P(y \mid do(x), z, w)$ | $(Y \perp\!\!\!\perp Z \mid X, W)_{G_{\overline{X}\underline{Z}}}$ |74| Rule 3 (Insertion/deletion of actions) | $P(y \mid do(x), do(z), w) = P(y \mid do(x), w)$ | $(Y \perp\!\!\!\perp Z \mid X, W)_{G_{\overline{X}\overline{Z(W)}}}$ |7576### 1.4 Identifiability Criteria7778| Criterion | Description | Applicability |79|---|---|---|80| Back-door | Adjust for confounders blocking back-door paths | Common, simple |81| Front-door | Mediate through intermediate variable | When no valid adjustment set |82| Instrumental variable | Exploit exogenous variation | Econometrics, natural experiments |83| General ID algorithm | Complete identification algorithm | Any semi-Markovian model |8485---8687## Part 2 — Counterfactual Reasoning8889### 2.1 Counterfactual Computation (3 Steps)90911. **Abduction**: Given evidence, infer $P(U \mid \text{evidence})$922. **Action**: Modify structural equations (intervention)933. **Prediction**: Compute outcome under modified model9495### 2.2 Potential Outcomes Framework9697- **Rubin causal model**: $Y_i(1), Y_i(0)$ — potential outcomes under treatment/control98- **ATE**: $\mathbb{E}[Y(1) - Y(0)]$ — average treatment effect99- **CATE**: $\mathbb{E}[Y(1) - Y(0) \mid X = x]$ — conditional on covariates100- **Pipeline mapping**: phase transitions as "treatment" effects on quality or safety outcomes101102### 2.3 Counterfactual Stability103104When is a counterfactual claim robust?105- **Monotonicity**: Outcome monotonic in treatment106- **Counterfactual stability**: Small perturbations in $U$ → small perturbations in counterfactual outcome107- **Pipeline example**: phase transitions can exhibit threshold or bifurcation-like counterfactual behavior (sudden jumps)108109---110111## Part 3 — Causal Discovery112113### 3.1 Methods114115| Method | Type | Assumptions | Output |116|---|---|---|---|117| PC algorithm | Constraint-based | Faithfulness, no latent confounders | CPDAG |118| FCI | Constraint-based | Allows latent confounders | PAG |119| GES | Score-based | BIC score, decomposable | CPDAG |120| NOTEARS | Continuous optimization | Acyclicity constraint | DAG |121| Causal transformers | Deep learning | Large observational data | DAG |122123### 3.2 Causal Graphs in a Verification Pipeline124125```126Example causal DAG:127 Stakeholder → Requirements → Phase classification128 Phase classification → Quality thresholds → Gate decisions129 Gate decisions → Knowledge state → Phase transitions130 Phase transitions → System trajectory → Final quality131```132133---134135## Part 4 — Deontic Logic136137### 4.1 Standard Deontic Logic (SDL)138139| Operator | Symbol | Reading | Formal |140|---|---|---|---|141| Obligation | $O(p)$ | "It ought to be that $p$" | $O(p) \equiv \neg P(\neg p)$ |142| Permission | $P(p)$ | "It is permitted that $p$" | $P(p) \equiv \neg O(\neg p)$ |143| Prohibition | $F(p)$ | "It is forbidden that $p$" | $F(p) \equiv O(\neg p)$ |144145### 4.2 Paradoxes and Extensions146147| Paradox | Description | Resolution |148|---|---|---|149| Ross's paradox | $O(p) \to O(p \lor q)$ — obliged to mail → obliged to mail or burn | Input/output logic |150| Contrary-to-duty | What obligations apply when one is violated? | Defeasible deontic logic |151| Free choice | $P(p \lor q)$ doesn't entail $P(p) \land P(q)$ | Bilateral norms |152| Chisholm | Nested conditional obligations conflict | Dyadic deontic logic |153154### 4.3 Deontic Logic for AI Governance155156| Governance Rule | Deontic Formalization |157|---|---|158| Gate must be passed before advancement | $O(\text{pass}(g_i) \to \text{before}(\text{phase}_{i+1}))$ |159| Safety envelope must be maintained | $F(\text{violate}(\text{safety\_envelope}))$ |160| Trust must converge | $O(\text{eventually}(\text{converged}(\tau)))$ |161| Provenance must be recorded | $O(\text{record}(\text{provenance}(a)))$ for all actions $a$ |162163### 4.4 Input/Output Logic (Makinson & van der Torre)164165```166Input/Output pairs: (a, x) meaning "given input a, output x"167Four operators: out_1 (simple), out_2 (+SI), out_3 (+CT), out_4 (+SI+CT)168Permission: negative (not forbidden) vs positive (explicitly permitted)169```170171Common application: quality gates as I/O norms mapping observation states to action obligations.172173---174175## Part 5 — Normative Multi-Agent Systems176177### 5.1 Norm Types178179| Norm Type | Example in a verification pipeline |180|---|---|181| Regulative | "Agents SHALL pass quality gate" |182| Constitutive | "Meeting threshold counts as passing" |183| Procedural | "Review must precede approval" |184| Institutional | "Council member has assessment authority" |185186### 5.2 Norm Compliance187188- **Regimented**: System physically prevents violations (hard constraints)189- **Regulated**: System detects and sanctions violations (soft constraints with enforcement)190- **Example**: quality gates can be regimented while trust scores or review confidence are regulated191192### 5.3 Norm Conflict Resolution193194| Strategy | Description | Common approach |195|---|---|---|196| Priority ordering | Higher-priority norm wins | Safety > quality > efficiency |197| Specificity | More specific norm overrides general | Phase-specific thresholds override defaults |198| Temporal | Later norm supersedes earlier | RETRO audit can update gates |199200---201202## Part 6 — Host-Repository Lean Extension Points203204Do not assume repository-local Lean modules, tactics, or namespaces exist unless the host repository explicitly provides them. When local modules exist, map them by role:205206| Local extension point | Causal/deontic aspect |207|---|---|208| Provenance / audit trail module | causal DAG of evidence, intervention tracking |209| Quality-gate module | deontic obligations and gate-passage requirements |210| Safety module | safety obligations and prohibited envelope violations |211| Classification module | causal model of classification → gate → transition |212| Tactic-helper module | reasoning automation for causal/deontic proofs |213| Dynamics module | causal dynamics of phase transitions |214215---216217## Part 7 — Epistemic Mapping218219| KK | KU | UU |220|---|---|---|221| SCM theory well-established | Full do-calculus in Lean 4 | Causal reasoning under deep uncertainty |222| SDL axiomatized | I/O logic Lean formalization | Emergent norms in multi-agent systems |223| Back-door criterion proven | Automated causal discovery verification | Counterfactual stability for chaotic systems |224| Pipeline causal DAG identified | GAI causal reasoning regulation | Ethical AI as deontic system |
r-irbe