Intuitionistic $j$-Do-Calculus in Topos Causal Models

TL;DR

This work generalizes Pearl's do-calculus to an intuitionistic, topos-based setting by introducing j-stability, where truth is local and interventions are modeled as subobjects within a site $( ext{C},J)$. It defines three j-do rules (J1–J3) and proves their soundness under Kripke–Joyal semantics, showing that classical do-calculus is recovered when $J$ is trivial and enabling regime-aware identification via appropriate covers. The framework uses Lawvere–Tierney topologies on the subobject classifier, a distribution monad internal to the topos, and the co-Kleisli category to model stochastic kernels, interventions, and their composition, thereby yielding an internal, compositional theory of causal reasoning in sites. A companion paper is promised to address data-driven estimation, regime construction, and practical deployment of j-do with standard discovery tools, along with experiments on how to form $j$-covers, compute chartwise CI after surgeries, and certify premises of the j-do rules in practice. The approach unifies categorical causality with internal logic in a universal, cocomplete setting, providing a principled route to local-to-global causal inference under partial observability and regime changes.

Abstract

In this paper, we generalize Pearl's do-calculus to an Intuitionistic setting called $j$-stable causal inference inside a topos of sheaves. Our framework is an elaboration of the recently proposed framework of Topos Causal Models (TCMs), where causal interventions are defined as subobjects. We generalize the original setting of TCM using the Lawvere-Tierney topology on a topos, defined by a modal operator $j$ on the subobject classifier $Ω$. We introduce $j$-do-calculus, where we replace global truth with local truth defined by Kripke-Joyal semantics, and formalize causal reasoning as structure-preserving morphisms that are stable along $j$-covers. $j$-do-calculus is a sound rule system whose premises and conclusions are formulas of the internal Intuitionistic logic of the causal topos. We define $j$-stability for conditional independences and interventional claims as local truth in the internal logic of the causal topos. We give three inference rules that mirror Pearl's insertion/deletion and action/observation exchange, and we prove soundness in the Kripke-Joyal semantics. A companion paper in preparation will describe how to estimate the required entities from data and instantiate $j$-do with standard discovery procedures (e.g., score-based and constraint-based methods), and will include experimental results on how to (i) form data-driven $j$-covers (via regime/section constructions), (ii) compute chartwise conditional independences after graph surgeries, and (iii) glue them to certify the premises of the $j$-do rules in practice

Figures (13)

• Figure 1: The Rules of $j$-do-calculus.
• Figure 2: External Grothendieck topology $J$ and internal Lawvere–Tierney topology $j$ both induce subtopoi embedded in the presheaf topos $[\mathcal{C}^{\mathrm{op}},\mathrm{Set}]$.
• Figure 3: A simple causal model of pollution in New Delhi, India sm:neurips_tcmDBLP:journals/entropy/Mahadevan23.
• Figure 4: From classical to TCM view of causal do-calculus interventions $do(X)$. (a) In the DAG, incoming edges to $X$ are cut and replaced by a fixed policy. (b) In the TCM, this is expressed by replacing the kernel $k_X:Z\to\mathsf{Dist}(X)$ with a chosen $\mu_X$ and composing via the monadic integration law. Both yield the equality $P(Y\mid do(X),Z)=\int_X P(Y\mid X,Z)\,d\mu_X(X)$, which in the internal logic reads $Z\vdash P(Y\mid do(X),Z)=P(Y\mid Z)$ whenever $Y\!\perp\! X\mid Z$ in the cut model.
• Figure 5: Side-by-side correspondence between the classical DAG view (left) and the TCM categorical view (right). Each DAG operation (conditioning, edge deletion, independence) maps to a categorical construction: comprehension subobject $+$ normalization, kernel replacement $+$ integration, and factorization in $\mathcal{E}$.

Theorems & Definitions (59)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Definition 7
• Lemma 1: Families vs. sieves
• Definition 8
• Definition 9