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
翻译:本文中,我们将Pearl的do-演算推广至直觉主义框架,称为层拓扑斯内的$j$-稳定因果推断。我们的框架是对近期提出的拓扑斯因果模型(TCMs)框架的精细化发展,其中因果干预被定义为子对象。我们利用由子对象分类器$\Omega$上的模态算子$j$定义的Lawvere-Tierney拓扑,对原始TCM设置进行了推广。我们引入$j$-do-演算,其中用Kripke-Joyal语义定义的局部真值取代全局真值,并将因果推理形式化为沿$j$-覆盖保持稳定的结构保持态射。$j$-do-演算是一个可靠规则系统,其前提与结论均为因果拓扑斯内部直觉主义逻辑的公式。我们将条件独立性与干预性主张的$j$-稳定性定义为因果拓扑斯内部逻辑中的局部真值。我们给出了三条推理规则,分别对应Pearl的插入/删除规则与行动/观测交换规则,并在Kripke-Joyal语义中证明了其可靠性。正在撰写的姊妹篇将阐述如何从数据中估计所需实体,并通过标准发现流程(例如基于评分和基于约束的方法)实例化$j$-do,同时包含以下实验研究:(i)如何构建数据驱动的$j$-覆盖(通过机制/截面构造),(ii)如何在图手术后计算图表层面的条件独立性,(iii)如何在实践中通过粘合操作验证$j$-do规则的前提条件