pith. sign in

arxiv: 2405.11073 · v2 · pith:ORV3ISJ4new · submitted 2024-05-17 · 💻 cs.LO · math.CT· math.LO

Equivalence and Conditional Independence in Atomic Sheaf Logic

Alex Simpson This is my paper

Pith reviewed 2026-05-24 00:59 UTC · model grok-4.3

classification 💻 cs.LO math.CTmath.LO
keywords atomic sheaf toposesconditional independenceequivalence relationsindependence logicclassical logicmultiteam semanticssheaf semantics
0
0 comments X

The pith

Atomic sheaf toposes model equivalence and conditional independence inside classical logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that atomic sheaf toposes naturally represent distinctions among equality of variables, a coarser equivalence, and conditional independence between variables. Atomic equivalence, which every atomic sheaf possesses, handles the equivalence relation, while extra structure on the generating category interprets conditional independence. The resulting internal logic remains classical yet validates several fundamental reasoning principles that connect equivalence to conditional independence. Concrete cases include a category of surjections between finite sets, where the relations match multiteam semantics of independence logic but sit inside classical logic, plus probability sheaves and the Schanuel topos.

Core claim

Atomic sheaf logic is the classical logic induced by an atomic sheaf topos whose generating category carries extra structure; in this logic atomic equivalence interprets a coarser form of variable equality, conditional independence receives a direct interpretation, and the logic validates basic principles relating the two notions, with the multiteam semantics of independence logic recovered as one instance.

What carries the argument

Atomic sheaf toposes generated by a category equipped with additional structure that supports direct interpretation of conditional independence.

If this is right

  • The induced logic validates a number of fundamental reasoning principles relating equivalence and conditional independence.
  • In the running example the interpretations coincide exactly with mutual inclusion and the multiteam semantics of independence logic.
  • The same framework recovers equality-in-distribution together with ordinary probabilistic conditional independence in the category of probability sheaves.
  • In the Schanuel topos the notions become orbit equality and a relative form of separatedness.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The construction shows one way to embed independence-logic semantics inside an ambient classical logic.
  • The same pattern of additional structure on a generating category could be applied to model independence notions arising in database theory or causal graphs.
  • Further instances might be obtained by choosing other concrete categories that generate atomic toposes.

Load-bearing premise

The category that generates the atomic topos admits extra structure allowing conditional independence to be interpreted inside the topos.

What would settle it

An atomic sheaf topos equipped with the required additional structure whose internal logic fails to validate one of the fundamental reasoning principles that relate equivalence to conditional independence.

Figures

Figures reproduced from arXiv: 2405.11073 by Alex Simpson.

Figure 1
Figure 1. Figure 1: Multiteam semantics of atomic formulas of nondeterministic variables to logic variables, and the satisfaction relation can then be rewritten as |=ρ Φ . (5) It turns out to be helpful to make the sample set Ω, that occurs implicitly within ρ, explicit in the notation, so we write Ω ⊩ρ Φ . (6) We here switch to the ‘forcing’ notation ⊩, since we view Ω as a ‘possible world’ or ‘condition’ (capturing all the … view at source ↗
Figure 2
Figure 2. Figure 2: Semantics of atomic sheaf logic Definition 4.1 (Semantic interpretation). A semantic interpretation in Shat(C) is given by a function mapping every sort A to an atomic sheaf A (i.e., to an object of Shat(C)), and a function mapping every relation symbol R of arity A1 . . . An to a subsheaf R ⊆ A1 × · · · × A1. Definition 4.2 (Sub(pre)sheaf). For P, Q ∈ Psh(C), we say that Q is a subpresheaf of P (notation … view at source ↗
Figure 3
Figure 3. Figure 3: Axioms for equivalence length and sorting with ⃗x, and hence also with ⃗y. We then write Φ(⃗x) for the substitution Φ(⃗x/⃗z), and similarly for Φ(⃗y). We call (14) the invariance principle, as it states that properties not involving extraneous variables are invariant under equivalence. Axoim (15) is called the transfer principle. If ⃗x and x⃗′ are jointly equivalent, then for any variable y there exists a … view at source ↗
Figure 4
Figure 4. Figure 4: Axioms for conditional independence We show that X ⊥⊥ Y |Z, according to Definition 2.2. Suppose we have ω ′ , ω′′ ∈ Ω such that X(ω ′ ) = a and Z(ω ′ ) = c and Y (ω ′′) = b and Z(ω ′′) = c. Then Z ′ (r(p(ω ′ ))) = Z(ω ′ ) = Z(ω ′′) = Z ′ (s(q(ω ′′))) . Since (ΩZ, r ◦ p, Z′ ) is support for Z, the function Z ′ : ΩZ → C is injective, hence r(p(ω ′ )) = s(q(ω ′′)). Since the top-left square is independent, t… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proposes modeling relations of equivalence (via atomic equivalence in sheaves) and conditional independence in atomic sheaf toposes generated by categories with additional structure. It claims the induced internal logic is classical and validates fundamental reasoning principles relating these notions. The main running example is the atomic topos over surjections between finite nonempty sets, where the interpretations recover multiteam semantics of independence logic (with mutual inclusion as equivalence) but embedded in a classical logic. Two further instances are sketched: probability sheaves (equality-in-distribution and probabilistic CI) and the Schanuel topos (orbit equality and relative separatedness).

Significance. If the constructions and validations hold, the work supplies a categorical semantic foundation that embeds non-classical independence-logic semantics inside classical logic via topos theory. The framework is versatile across examples and identifies a general mechanism (additional structure on the generating category) for interpreting conditional independence, which could connect independence logic, probabilistic reasoning, and nominal techniques in a uniform way.

minor comments (2)
  1. [Abstract] The abstract states that the atomic sheaf logic 'validates a number of fundamental reasoning principles' but does not list or derive any specific principles (e.g., axioms or rules for equivalence and CI). Adding an explicit list or reference to a later section containing the derivations would strengthen the claim.
  2. [Running example (surjections of finite nonempty sets)] The running example recovers multiteam semantics inside a classical logic, but the text does not indicate whether the surrounding classical connectives interact with the independence atoms in ways that could produce new validities or inconsistencies not present in independence logic.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our manuscript and the recommendation of minor revision. The referee's description correctly captures the core contributions: the use of atomic sheaf toposes to interpret equivalence via atomic relations and conditional independence via additional structure on the generating category, with the main example recovering multiteam semantics inside classical logic, plus the sketched extensions to probability sheaves and the Schanuel topos.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper constructs interpretations of equivalence and conditional independence inside atomic sheaf toposes by invoking the standard definition of atomic equivalence (present in every atomic sheaf) together with an explicitly identified additional structure on the generating category. These steps rest on established topos-theoretic notions rather than any self-referential definition, fitted parameter renamed as prediction, or load-bearing self-citation chain. The running example recovers multiteam semantics inside a classical logic by direct comparison of the interpretations, and the two further examples (probability sheaves, Schanuel topos) are presented as independent instances of the same framework. No equation or claim reduces to its own input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The claims rest on standard axioms of topos theory plus one domain-specific modeling assumption; no free parameters or invented entities are introduced in the abstract.

axioms (3)
  • standard math The internal logic of atomic sheaf toposes is classical.
    Standard property of toposes invoked to obtain the surrounding logic.
  • standard math Every atomic sheaf possesses a relation of atomic equivalence.
    Stated as possessed by every atomic sheaf in the abstract.
  • domain assumption Additional structure exists on the generating category that permits interpretation of conditional independence.
    Explicitly identified in the abstract as the structure needed to interpret conditional independence.

pith-pipeline@v0.9.0 · 5826 in / 1396 out tokens · 41159 ms · 2026-05-24T00:59:34.237071+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    A bunched logic for conditional independence

    Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. A bunched logic for conditional independence. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2021

    work page 2021

  2. [2]

    A probabilistic separation logic

    Gilles Barthe, Justin Hsu, and Kevin Liao. A probabilistic separation logic. Proc. ACM Program. Lang., 4(POPL), dec 2019

    work page 2019

  3. [3]

    A. P. Dawid. Conditional independence in statistical theory. Journal of the Royal Statistical Society. Series B (Methodological), 41(1):1–31, 1979

    work page 1979

  4. [4]

    A. P. Dawid. Separoids: A mathematical framework for conditional independence and irrel- evance. Annals of Mathematics and Artificial Intelligence , 32(1):335–372, 2001

    work page 2001

  5. [5]

    Construction of Biclosed Categories

    Brian Day. Construction of Biclosed Categories . PhD thesis, 1970

    work page 1970

  6. [6]

    Approx- imation and dependence via multiteam semantics

    Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, and Jonni Virtema. Approx- imation and dependence via multiteam semantics. Annals of Mathematics and Artificial Intelligence, 83(3):297–320, 2018

    work page 2018

  7. [7]

    Reflective kleisli subcategories of the category of eilenberg- moore algebras for factorization monads

    Marcelo Fiore and Mat´ ıas Menni. Reflective kleisli subcategories of the category of eilenberg- moore algebras for factorization monads. Theory and Applications of Categories [electronic only], 15:40–65, 2005

    work page 2005

  8. [8]

    Gabbay and Andrew M

    Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing , 13(3):341–363, 2002

    work page 2002

  9. [9]

    Axioms and algorithms for inferences involving probabilistic independence

    Dan Geiger, Azaria Paz, and Judea Pearl. Axioms and algorithms for inferences involving probabilistic independence. Information and Computation , 91(1):128–141, 1991

    work page 1991

  10. [10]

    Logical and Algorithmic Properties of Conditional Independence and Graphical Models

    Dan Geiger and Judea Pearl. Logical and Algorithmic Properties of Conditional Independence and Graphical Models. The Annals of Statistics , 21(4):2001 – 2021, 1993

    work page 2001

  11. [11]

    Dependence and independence.Studia Logica, 101(2):399– 410, 2013

    Erich Gr¨ adel and Jouko V¨ a¨ an¨ anen. Dependence and independence.Studia Logica, 101(2):399– 410, 2013

    work page 2013

  12. [12]

    A finite axiomatization of conditional independence and inclusion dependencies

    Miika Hannula and Juha Kontinen. A finite axiomatization of conditional independence and inclusion dependencies. Information and Computation , 249:121–137, 2016

    work page 2016

  13. [13]

    Informational independence as a semantical phe- nomenon

    Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantical phe- nomenon. In Jens Erik Fenstad, Ivan T. Frolov, and Risto Hilpinen, editors, Logic, Method- ology and Philosophy of Science VIII , volume 126 of Studies in Logic and the Foundations of Mathematics, pages 571–589. Elsevier, 1989

    work page 1989

  14. [14]

    W. Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL , 5(4):539–563, 1997

    work page 1997

  15. [15]

    Sketches of an elephant: a Topos theory compendium

    Peter T Johnstone. Sketches of an elephant: a Topos theory compendium. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. 24

    work page 2002

  16. [16]

    Foundations of Modern probability Theory

    Olav Kallenberg. Foundations of Modern probability Theory . Springer Cham, first edition edition, 1997

    work page 1997

  17. [17]

    Li, Amal Ahmed, and Steven Holtzen

    John M. Li, Amal Ahmed, and Steven Holtzen. Lilac: A modal separation logic for conditional probability. Proc. ACM Program. Lang., 7(PLDI), jun 2023

    work page 2023

  18. [18]

    Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen

    John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen. A nominal approach to probabilistic separation logic. In 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , New York, NY, USA, 2024. ACM

    work page 2024

  19. [19]

    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

    work page 1992

  20. [20]

    About N-quantifiers

    Mat´ ıas Menni. About N-quantifiers. Applied Categorical Structures, 11(5):421–445, 2003

    work page 2003

  21. [21]

    Graphoids: Graph-based logic for reasoning about relevance relations orwhen would x tell you more about y if you already know z? Probabilistic and Causal Inference, 1986

    Judea Pearl and Azaria Paz. Graphoids: Graph-based logic for reasoning about relevance relations orwhen would x tell you more about y if you already know z? Probabilistic and Causal Inference, 1986

    work page 1986

  22. [22]

    Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013

    work page 2013

  23. [23]

    Probability sheaves and the Giry monad

    Alex Simpson. Probability sheaves and the Giry monad. 2017

    work page 2017

  24. [24]

    Category-theoretic structure for independence and conditional independence

    Alex Simpson. Category-theoretic structure for independence and conditional independence. Electronic Notes in Theoretical Computer Science, 336:281–297, 2018. The Thirty-third Con- ference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)

    work page 2018

  25. [25]

    Stochastic independence, causal independence, and shieldability

    Wolfgang Spohn. Stochastic independence, causal independence, and shieldability. Journal of Philosophical Logic, 9(1):73–99, 1980

    work page 1980

  26. [26]

    Two cotensors in one: Presentations of algebraic theories for local state and fresh names

    Sam Staton. Two cotensors in one: Presentations of algebraic theories for local state and fresh names. Electronic Notes in Theoretical Computer Science, 249:471–490, 2009. Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009)

    work page 2009

  27. [27]

    Lon- don Mathematical Society Student Texts

    Jouko V¨ a¨ an¨ anen.Dependence Logic: A New Approach to Independence Friendly Logic . Lon- don Mathematical Society Student Texts. Cambridge University Press, 2007. 25

    work page 2007