REVIEW 4 major objections 5 minor 4 cited by
Intuitionistic $j$-Do-Calculus in Topos Causal Models
T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash
Pith's one-line read Classical do-calculus generalizes to intuitionistic sheaf logic: the paper's j-do-calculus derives three inference rules that stay sound when truth is local, and collapse back to the classical rules under the trivial topology.
desk verdict The central j-stability definition rests on a false sieve lemma, so the soundness claim does not hold; an interesting but not yet valid draft. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the Lawvere-Tierney topology j on the subobject classifier Ω of the presheaf topos, which selects which sieves of refinements count as covers, together with the Kripke-Joyal forcing relation U⊩jφ. j-stability of a conditional independence φ at U is defined as: the sieve S_φ(U) of all refinements V→U that validate φ is a J-cover of U. The rules J1–J3 operate by turning local d-separation premises, evaluated after the corresponding graph surgeries on a cover, into internal equalities between interventional conditional distributions.
What would settle it
On the Earthquake DAG B→A←E with A a collider, take U with no conditioning: B⊥E holds. The refinement V→U that conditions on A opens the path B→A←E, so V does not validate B⊥E. Thus S_{B⊥E}(U) is not closed under precomposition, disproving the sieve lemma and breaking monotonicity of the proposed forcing relation.
Extended reading notes
Core claim
The paper's central claim is that the three rules of do-calculus remain sound when all causal assertions are read internally in the topos of sheaves over a site of regimes: the premises and conclusions are formulas of the internal intuitionistic logic, and a premise like 'Y⊥Z|X,W after cutting arrows into X' means that this conditional independence holds on every chart of some J-cover of the stage U. The rules are stated as equalities of internal interventional conditional distributions, and soundness is proved by Kripke-Joyal induction over covers. The trivial topology recovers the classical Boolean rules; other topologies let identification proceed from a cover of observational and interve
Load-bearing premise
The claim that refining a stage can only block additional paths — so the set of refinements validating a conditional independence is a sieve — is the load-bearing premise; refinements that condition on colliders open paths instead of blocking them.
Editorial extensions
If this is right
- If the soundness theorems hold, causal identification can be certified locally on admissible regimes and glued to conclusions at the ambient stage.
- Classical do-calculus is the special case of the trivial topology, so the framework strictly generalizes the classical rules.
- Choosing a topology that encodes experimental covers yields regime-aware identification, where a claim is accepted only if it persists across the charts deemed legitimate.
- The internal intuitionistic logic makes the rules constructive: equalities are verified stagewise, which may support reasoning about partial information and higher-order causal policies.
- The universal property of the topos causal model construction extends to the j-sheaf subtopos, so any colimit-preserving causal semantics factors through the sheafified topos.
Reading between the lines
- The 'sieve lemma' in Section 3.4 is load-bearing: it claims refinements only block paths, but a refinement that conditions on a collider opens paths (e.g., in the Earthquake DAG, B⊥E holds at U but fails after conditioning on A). If this lemma fails, the definition of j-stability as 'S_φ(U) is a J-cover' is not well-formed and Kripke-Joyal forcing is not monotone; the soundness proofs need a repai
- I infer that the framework's practical value depends on finding topologies whose covers are both semantically legitimate and algorithmically constructible; the companion paper is expected to provide this, but the current text does not.
- The exchangeable j-stable causality section is programmatic: it sketches how permutation invariance interacts with j-covers, but does not prove a full de Finetti theorem internally; a testable extension would be to instantiate the j-de Finetti principle on panel data and verify orbit-type dependence of estimated effects.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes an intuitionistic generalization of Pearl's do-calculus, called j-do-calculus, inside the topos of sheaves Sh_J(C). The central claim is that three rules J1–J3 are sound in the internal intuitionistic logic of the causal topos, specialize to classical do-calculus when J is the trivial topology, and support regime-aware causal inference. The paper defines j-stability of conditional independence statements via Kripke–Joyal forcing, illustrates the framework on Earthquake and Pollution DAGs, develops the internal logic and distribution-monad semantics of Topos Causal Models, and sketches extensions to exchangeable causality.
Significance. A correct version of this framework could be valuable: it would give a category-theoretic account of context-dependent causal reasoning, unify d-separation with sheaf-theoretic gluing, and provide a conservative extension of Pearl's calculus. The paper has genuine strengths: it gives concrete running examples with explicit charts and covers, includes a detailed translation table between classical and topos-theoretic notions, and correctly identifies the relevant standard machinery (Grothendieck topologies, Lawvere–Tierney topologies, Kripke–Joyal semantics, distribution monads). However, the central mathematical definition of j-stability is invalid as stated, an auxiliary monotonicity claim is false, and the soundness proofs are sketches rather than proofs. The central contribution is therefore not established in this version.
major comments (4)
- [§3.4, Lemma (sieve) and 'Forcing semantics (j-stability)'] The asserted lemma that S_φ(U) = {u: V→U | V |= φ} is a sieve is false. In the Earthquake DAG B→A←E, A→C, take U = (G,σ_∅) and φ = (B⊥E). Then id_U ∈ S_φ(U), because the collider A is unconditioned. Let w: W→U be a refinement that adds A to the conditioning set. In W, B and E are no longer independent, since conditioning on the collider A opens the path B–A–E. Thus id_U ∘ w = w ∉ S_φ(U), so S_φ(U) is not closed under precomposition. Since J(U) consists of sieves, the definition 'U ⊩_J φ iff S_φ(U) is a J-cover' is ill-formed. Moreover, Kripke–Joyal forcing is monotone under refinement, so the d-separation predicate cannot be a formula of the internal language unless its extension is pullback-stable. This is not a local typo: the same S_φ(U) definition is used in the worked examples and in the proof of 'soundness of j-stability', and the absence of a valid j-stability notion undermines Th
- [§8, Proposition 5] Proposition 5 states that if X ⊥_U^j Y | Z and Z ⊆ Z′, then X ⊥_U^j Y | Z′. This is false for ordinary d-separation: in the DAG X→C←Y, with Z = ∅ and Z′ = {C}, we have X and Y d-separated given Z, but conditioning on the collider C opens the path, so X and Y are not d-separated given Z′. By Proposition 3, when J is the trivial topology j-d-separation coincides with classical d-separation. Thus Proposition 5 would force classical d-separation to be monotone in the conditioning set, which it is not. The proposition must be deleted or replaced with a correct statement, and any later use of it needs revision.
- [§10, Theorem 11 (J2)] Theorem 11 does not match Pearl's Rule 2 as stated in Figure 1. The theorem asserts: if E ⊨ (Y⊥Z|X), then E ⊨ (P(Y|Do(X),Z) ≡ P(Y|X,Z)). But the Rule 2 in Figure 1 has premise (Y⊥Z|X,W) in G_{X,Z} on a J-cover and conclusion P(y|do(x),do(z),w) = P(y|do(x),z,w). The theorem exchanges X rather than Z, drops W, and omits the graph surgery. Section 10.2 gives yet another variant, P(Y|do(Z),do(W),X)=P(Y|do(W),X), which is also not the statement in Figure 1. This inconsistency makes the claimed generalization of Pearl's Rule 2 impossible to verify and is load-bearing for the central claim that J1–J3 mirror the classical rules.
- [§10, Theorems 10–12 and Remark 2] The soundness of j-do-calculus is asserted rather than proved. Theorems 10–12 are stated without proofs; Figure 1 labels soundness as '(sketch)'; Remark 2 says the proof is by 'Kripke–Joyal induction over J-covers' but no such induction is given. The computations in §10.2–10.3 verify equalities in a special kernel model where conditional independence is defined as factorization k=k_0∘π_Γ and interventions as integration against a policy. Under those definitions the rules reduce to unpacking the definitions, so they do not establish soundness for the general sheaf-theoretic j-do-calculus stated in Section 8. The Introduction itself says the paper will be revised into 'a more rigorous categorical presentation in future work.' As submitted, the central soundness claim lacks the required proof.
minor comments (5)
- [§6.2, Theorem 2] The Kripke–Joyal clauses are garbled: the disjunction clause uses p+q:N+O→M with the wrong domain/codomain, the implication clause repeats φ instead of switching to ψ, the negation clause has m:p:M→N in the wrong direction, and clause 6 uses an undefined V. These should be corrected to the standard Mitchell–Bénabou semantics.
- [Notation] The notation for mutilated graphs is inconsistent: G_X vs. \bar G, G_{X,Z} vs. \underline Z, and Z(W) are used with different definitions in §2.1, §8, and §10.2. This makes it very difficult to check Theorem 11 against Pearl's original Rule 2.
- [§3.4] The 'Slogan' defining j-stability ('the sieve of all refinements validating φ is a J-cover') conflicts with the earlier Kripke–Joyal clause requiring only existence of a covering sieve whose members force φ. The manuscript cannot have both; the first version is the one that fails.
- [References] There are repeated typos in the bibliography and citations: 'MacLane and leke Moerdijk' should be 'Mac Lane and Ieke Moerdijk'; some equation references are also imprecise.
- [Abstract / Introduction] The paper repeatedly defers algorithmic and experimental content to a 'companion paper in preparation.' This is acceptable for a theory paper, but the framing in the abstract and introduction overstates what the current manuscript establishes.
Circularity Check
The 'soundness' of j-do-calculus is built into the semantics: conditional independence is defined as kernel factorization and interventions as integration, so the rules hold by unpacking definitions.
-
self definitional
[§10.2, Eq. (2), Lemma 6, Theorem 15; Fig. 1 j-Rule 1]
"Independence Y⊥Z|Γ in M_Z is the internal factorization k=k0◦πΓ : Γ×Z→Dist(Y), (2), i.e. k ignores its Z-argument. ... if k is independent of Z in M_Z (i.e. k=k0◦πΓ), then Do_Z(k;µ)=k0 for every µ."
The premise of j-Rule 1 is defined to be the factorization k=k0∘πΓ; the conclusion is Do_Z(k;µ)=k0. Since Do_Z is defined as integration of k against µ, substituting the premise into the definition yields the conclusion in one line. Thus the 'soundness' of the rule is equivalent to the definition of conditional independence; the do-calculus equality is the premise rewritten under the intervention semantics. The same reduction applies to J2 and J3 (Theorems 11/12 and 16/17), whose proofs conclude by 'erasing the z-argument' from a kernel already assumed not to depend on z.
full rationale
The paper's central claim that j-do-calculus is sound reduces to the chosen semantics. Conditional independence is defined internally as kernel factorization (k=k0∘πΓ), and intervention is defined as integration against a policy (Do_Z(k;µ)=∫k dµ). Under these definitions, J1–J3 are one-line consequences: integrating a kernel that ignores Z yields the same kernel. The Kripke–Joyal cover machinery only glues these pointwise equalities; it does not add independent content to the rule soundness. This is a genuine self-definitional pattern, though no data are fitted and no empirical prediction is made. Self-citations to TCM (Mahadevan 2025a) are frequent but not load-bearing for the soundness proof, which uses standard topos semantics and the distribution monad. Separately, the §3.4 'Lemma (sieve)' is false—refinements can condition on colliders and open paths, as the paper's own non-example states ('conditioning on the collider A opens the path'). This is a serious correctness flaw, not a circularity, but it means the definition of j-stability as 'S_φ(U) is a J-cover' is not well-founded. Score 6 reflects the definitional reduction of the central soundness claim, not the self-citations or the correctness error.
Assumptions & free parameters
assumptions (4)
- ad hoc to paper S_φ(U) is a sieve (refinement monotonicity of CI)
- domain assumption Existence of internal interventional distribution P_int
- domain assumption Fiberwise global-Markov property of internal models
- domain assumption Site (C,J) supports pullback along arbitrary refinements for monotonicity
Cite this review
Pith. "Pith review of Intuitionistic $j$-Do-Calculus in Topos Causal Models." pith.science (2026). https://pith.science/paper/CHP44ZJH
@misc{pith2026251017944,
author = {Pith},
title = {Pith review of: Intuitionistic $j$-Do-Calculus in Topos Causal Models},
year = {2026},
howpublished = {\url{https://pith.science/paper/CHP44ZJH}},
note = {Machine review of arXiv:2510.17944}
}
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 $\Omega$. 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
Figures from the paper (10 more)
Forward citations
Cited by 4 Pith papers
-
A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction
A machine-checked Cubical Agda formalisation of topos causal models proves the intervention classifier, sheaf gluing, forcing clauses, and a corrected Lawvere-Tierney do-calculus, and adds a verified contextuality obs...
-
A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness
In Cubical Agda, conditional independence is formalized as paths between kernels, Bayesian conditioning is made total on a full-support fragment, and Pearl's d-separation soundness is verified for finite DAGs, using a...
-
Causal Density Functions
Causal density functions are Radon-Nikodym derivatives serving as local density ratios between do and obs distributions, allowing observational expectations reweighted by the ratio to reproduce interventional ones.
-
Decentralized Causal Discovery using Judo Calculus
Running standard causal-discovery methods per regime and keeping only edges that persist across regimes ('j-stable aggregation') improves precision and parallelism over pooled fits.
Reference graph
Works this paper leans on
-
[1]
J. L. Bell. Toposes and Local Set Theories. Dover, 1988
1988
-
[2]
Disintegration and bayesian inversion via string diagrams
Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29 0 (7): 0 938–971, March 2019. ISSN 1469-8072. doi:10.1017/s0960129518000488. URL http://dx.doi.org/10.1017/S0960129518000488
-
[3]
Causal theories: A categorical perspective on bayesian networks
Brendan Fong. Causal theories: A categorical perspective on bayesian networks. Master's thesis, Oxford University, 2012
2012
-
[4]
Patrick Forré and Joris M. Mooij. Markov properties for graphical models with cycles and latent variables, 2017
2017
-
[5]
Tobias Fritz. A synthetic approach to markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370: 0 107239, August 2020. ISSN 0001-8708. doi:10.1016/j.aim.2020.107239. URL http://dx.doi.org/10.1016/j.aim.2020.107239
arXiv 2020
-
[6]
The d-separation criterion in categorical probability
Tobias Fritz and Andreas Klingler. The d-separation criterion in categorical probability. Journal of Machine Learning Research, 24 0 (46): 0 1--49, 2023. URL http://jmlr.org/papers/v24/22-0916.html
2023
-
[7]
An axiomatic theory of counterfactuals
David Galles and Judea Pearl. An axiomatic theory of counterfactuals. Foundations of Science, 3: 0 151--182, 1988
1988
-
[8]
A categorical approach to probability theory
Mich \`e le Giry. A categorical approach to probability theory. In B. Banaschewski, editor, Categorical Aspects of Topology and Analysis, pages 68--85, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. ISBN 978-3-540-39041-1
1982
Show all 25 references
-
[9]
Topoi: The Categorial Analysis of Logic
Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Dover Press, 2006
2006
-
[10]
Causal de finetti: on the identification of invariant causal structure in exchangeable data
Siyuan Guo, Viktor T\' o th, Bernhard Sch\" o lkopf, and Ferenc Husz\' a r. Causal de finetti: on the identification of invariant causal structure in exchangeable data. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS '23, Red ...
2023
-
[11]
Imbens and Donald B
Guido W. Imbens and Donald B. Rubin. Causal Inference for Statistics, Social, and Biomedical Sciences: An Introduction. Cambridge University Press, USA, 2015. ISBN 0521885884
2015
-
[12]
Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science
Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. ISBN 9781316823187. doi:10.1017/CBO9781316823187. URL https://doi.org/10.1017/CBO9781316823187
2016 doi
-
[13]
Causal inference by string diagram surgery, 2018
Bart Jacobs, Aleks Kissinger, and Fabio Zanasi. Causal inference by string diagram surgery, 2018. URL https://arxiv.org/abs/1811.08338
2018 arXiv
-
[14]
Sheaves in Geometry and Logic a First Introduction to Topos Theory
Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic a First Introduction to Topos Theory. Springer New York, New York, NY, 1992. ISBN 9781461209270 1461209277. URL http://link.springer.com/book/10.1007/978-1-4612-0927-0
1992 doi
-
[15]
Categories for the Working Mathematician
Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, New York, 1971. Graduate Texts in Mathematics, Vol. 5
1971
-
[16]
Sheaves in Geometry and Logic: A First Introduction to Topos Theory
Saunders MacLane and leke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1994
1994
-
[17]
Universal causality
Sridhar Mahadevan. Universal causality. Entropy, 25 0 (4): 0 574, 2023. doi:10.3390/E25040574. URL https://doi.org/10.3390/e25040574
2023 doi
-
[18]
Universal causal inference in a topos
Sridhar Mahadevan. Universal causal inference in a topos. In Advances in Neural Information Processing Systems, Proceedings of the Thirty Ninth Annual Conference on Neural Information Processing Systems, San Diego, California, December 2-7, 2025, 2025 a
2025
-
[19]
Higher algebraic k-theory of causality
Sridhar Mahadevan. Higher algebraic k-theory of causality. Entropy, 27 0 (5), 2025 b . ISSN 1099-4300. doi:10.3390/e27050531. URL https://www.mdpi.com/1099-4300/27/5/531
2025 doi
-
[20]
Learning independent causal mechanisms
Giambattista Parascandolo, Mateo Rojas - Carulla, Niki Kilbertus, and Bernhard Sch \" o lkopf. Learning independent causal mechanisms. CoRR, abs/1712.00961, 2017. URL http://arxiv.org/abs/1712.00961
2017 arXiv
-
[21]
Probabilistic reasoning in intelligent systems - networks of plausible inference
Judea Pearl. Probabilistic reasoning in intelligent systems - networks of plausible inference. Morgan Kaufmann series in representation and reasoning. Morgan Kaufmann, 1989
1989
-
[22]
Causality: Models, Reasoning and Inference
Judea Pearl. Causality: Models, Reasoning and Inference. Cambridge University Press, USA, 2nd edition, 2009. ISBN 052189560X
2009
-
[23]
E. Riehl. Category Theory in Context. Aurora: Dover Modern Math Originals. Dover Publications, 2017. ISBN 9780486820804. URL https://books.google.com/books?id=6B9MDgAAQBAJ
2017
-
[24]
Causation, Prediction, and Search, Second Edition
Peter Spirtes, Clark Glymour, and Richard Scheines. Causation, Prediction, and Search, Second Edition. Adaptive computation and machine learning. MIT Press, 2000. ISBN 978-0-262-19440-2
2000
-
[25]
A survey on causal discovery: Theory and practice, 2023
Alessio Zanga and Fabio Stella. A survey on causal discovery: Theory and practice, 2023. URL https://arxiv.org/abs/2305.10032
2023 arXiv
Reviewed August 4, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.