Equivalence and Conditional Independence in Atomic Sheaf Logic

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 an intrinsic relation of atomic equivalence that is possessed by every atomic sheaf. We identify additional structure on the category generating the atomic topos (primarily, the existence of a system of independent pullbacks) that allows 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. At the end of the paper, we briefly outline two other instances of our framework, to demonstrate its versatility. The first of these 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 (equivalent to nominal sets) where equivalence is orbit equality and conditional independence amounts to a relative form of separatedness.