We propose a semantic foundation for logics for reasoning in settings that possess a distinction between equality of variables, a coarser equivalence of variables, and a notion of conditional independence between variables. We show that such relations can be modelled naturally in atomic sheaf toposes. Equivalence of variables is modelled by a relation of atomic equivalence that is possessed by every atomic sheaf. We identify additional structure on the category generating the atomic topos that allows the relation of conditional independence to be interpreted in the topos. We then study the logic of equivalence and conditional independence that is induced by the internal logic of the topos. This atomic sheaf logic is a classical logic that validates a number of fundamental reasoning principles relating equivalence and conditional independence. As a concrete example of this abstract framework, we use the atomic topos over the category of surjections between finite nonempty sets as our main running example. In this category, the interpretations of equivalence and conditional independence coincide with those given by the multiteam semantics of independence logic, in which the role of equivalence is taken by the relation of mutual inclusion. A major difference from independence logic is that, in atomic sheaf logic, the multiteam semantics of the equivalence and conditional independence relations is embedded within a classical surrounding logic. We outline two other instances of our framework, to demonstrate its versatility. The first is a category of probability sheaves, in which atomic equivalence is equality-in-distribution, and the conditional independence relation is the usual probabilistic one. Our other example is the Schanuel topos where equivalence is orbit equality and conditional independence amounts to a relative form of separatedness.
翻译:我们提出一种语义基础,用于对具有变量相等性、变量间更粗的等价性以及变量间条件独立性概念区分的情景进行推理的逻辑。我们证明此类关系可自然地在原子层拓扑斯中建模。变量等价性由每个原子层均具备的原子等价关系建模。我们进一步识别出生成原子拓扑斯的范畴上的附加结构,使得条件独立性关系可在该拓扑斯中得到解释。随后,我们研究由该拓扑斯内部逻辑导出的等价性与条件独立性逻辑。此原子层逻辑是一种经典逻辑,它验证了诸多关于等价性与条件独立性之间联系的基本推理原则。作为该抽象框架的具体实例,我们以有限非空集合之间满射范畴上的原子拓扑斯作为主要贯穿例子。在该范畴中,等价性与条件独立性的解释与独立性逻辑的多团队语义给出的解释一致,其中等价性的角色由互包含关系承担。与独立性逻辑的一个主要区别在于,在原子层逻辑中,等价性与条件独立性关系的多团队语义被嵌入到一个经典的外部逻辑之中。为展示其多样性,我们概述了该框架的另外两个实例。第一个是概率层范畴,其中原子等价性意为分布相等,条件独立性关系即通常的概率条件独立性。另一个例子是Schanuel拓扑斯,其中等价性指轨道相等,而条件独立性则相当于一种相对的分离性形式。