拓扑斯因果模型的立方体形式化：干预、层胶合与直觉主义do-演算
A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction
浏览论文内容
中文总结 AI 辅助
研究在拓扑斯中重塑因果推理，核心方法是在立方体Agda中基于概率单子和do-演算对其1-拓扑斯核心形式化，主要贡献包括构建分类器、证明层胶合、修复模态层漏洞、添加上下文障碍等。
中文摘要 AI 辅助
拓扑斯因果模型在拓扑斯内部重塑因果推理：因果世界是一个预层，干预是到子对象分类器的特征映射，推理在直觉主义内部语言中进行。我们首次在立方体Agda中对这个1-拓扑斯核心进行了机器检查，基于先前验证的概率单子和do-演算。我们构建了筛子的分类器并通过其分类定理将干预$\mathrm{do}(X:= x_0)$实现为特征映射；证明了独立机制的层胶合，这是原文献断言但未证明的；并机器检查了内部语言的克里普克-乔亚尔强制条款。在模态层我们发现并修复了一个漏洞：三个标准的劳威尔-蒂尔尼公理并不强制一个闭包算子。恢复缺失的定律后，可以展示双重否定拓扑作为一个具体实例，并表明干预和珀尔规则在每个拓扑下都是稳定的。跨覆盖区域的反事实的可迁移性与这种$j$-稳定性一致，理解为跨覆盖的不变性。我们进一步添加了该程序未考虑的一种现象：一个机器检查的上下文障碍，即成对一致的局部数据不存在全局模型。该开发不假设任何公理，并在Agda的--safe标志下进行类型检查，有序域具体在$\mathbb{Q}$处解除；范围是预层（1-拓扑斯）片段，类型级别的层化和定向提升留待未来工作。
英文摘要
Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a sub-model named by a characteristic map into the subobject classifier $\Om$, and reasoning is Kripke-Joyal forcing in an intuitionistic internal language. We give the first axiom-free machine-checked account of this 1-topos core, in Cubical Agda over a previously verified probability monad and do-calculus; the framework is otherwise developed on paper, with central claims stated rather than proved. Three of our results go beyond faithful transcription. We exhibit a contextuality obstruction the programme does not treat: pairwise-consistent local causal data with no global model, detected by a degree-one holonomy class. We delimit the claim that interventions are modelled by the subobject classifier: an intervention and an observation name the same subobject, so $\Om$ fixes the target of a do-operation but not the operation itself, which is surgery on the kernels --- where, on a confounder, the interventional and observational laws differ. And we settle the modal unit --- inflationarity is derivable from $j\top = \top$ and naturality, not a fourth axiom. We also machine-check the classifier of sieves with its classification theorem, the pullback collating local mechanisms, and the Kripke-Joyal forcing clauses. The development assumes no axioms and typechecks under Agda's \texttt{--safe} flag, with the ordered field discharged at $\mathbb{Q}$; type-level sheafification and a directed do-calculus are future work.
发表机构
- Institute of Chemistry, Academia Sinica, Taipei, Taiwan（中国科学院化学研究所）
机构由 AI 辅助整理，请以论文原文为准。
