Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic

Author Satoshi Nakata

Thumbnail PDF


  • Filesize: 0.78 MB
  • 21 pages

Document Identifiers

Author Details

Satoshi Nakata
  • Research Institute for Mathematical Sciences, Kyoto University, Japan


I would like to thank my supervisor, Kazushige Terui, for careful reading and many helpful suggestions. I am also grateful to Hisashi Aratake, Yutaka Maita, Takayuki Kihara and the anonymous referees for their invaluable comments.

Cite AsGet BibTex

Satoshi Nakata. Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


There has been work on the strength of semi-classical axioms over Heyting arithmetic such as Σ_n-DNE (double negation elimination) and Π_n-LEM (law of excluded middle). Among other things, Akama et al. show that Σ_n-DNE does not imply Π_n-LEM for any n ≥ 1 by using Kleene realizability relativized to Turing degrees. These realizability notions are expressed by subtoposes of the effective topos ℰff and thus by corresponding local operators (a.k.a. Lawvere-Tierney topologies). Our purpose is to provide a topos-theoretic explanation for separation of semi-classical axioms. It consists of determining the least dense local operator of a given axiom φ in a topos ℰ, which completely characterizes the dense subtoposes of ℰ satisfying φ. This idea is motivated by Caramello’s study of intermediate propositional logics and van Oosten’s study of Lifschitz realizability. We first investigate sufficient conditions for an arithmetical formula to have a least dense operator. In particular, we show that each semi-classical axiom has a least dense operator in every elementary topos with natural number object. This is a generalization of van Oosten’s result for Π₁∨Π₁-DNE in ℰff. We next determine least dense operators of semi-classical axioms in ℰff in terms of (generalized) Turing degrees. Not only does it immediately imply some separation results of Akama et al. but also explain that realizability notions they used are optimal in the sense of minimality. We finally point out a negative consequence that Π_n-LEM, Σ_n-LEM and Σ_{n+1}-DNE are never separable by any subtopos of ℰff for any n ≥ 0.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • local operator
  • elementary topos
  • effective topos
  • realizability
  • intuitionistic arithmetic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach. An arithmetical hierarchy of the law of excluded middle and related principles. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pages 192-201, 2004. Google Scholar
  2. Stefano Berardi and Silvia Steila. Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), pages 64-83, 2014. Google Scholar
  3. Guram Bezhanishvili and Wesley H. Holiday. A semantic hierarchy for intuitionistic logic. Indagationes Mathematicae, 30(3):403-469, 2019. Google Scholar
  4. Andreas Blass and Andrej Sc̆edrov. Boolean classifying topoi. Journal of Pure and Applied Algebra, 28(1):15-30, 1983. Google Scholar
  5. Olivia Caramello. De Morgan classifying toposes. Advances in Mathematics, 222(6):2117-2144, 2009. Google Scholar
  6. Olivia Caramello. Topologies for intermediate logics. Mathematical Logic Quarterly, 60(4):335-347, 2014. Google Scholar
  7. Olivia Caramello. Theories, Sites, Toposes Relating and studying mathematical theories through topos-theoretic 'bridges'. Oxford University Press, 2018. Google Scholar
  8. Eric Faber and Jaap van Oosten. More on geometric morphisms between realizability toposes. Theory and Applications of Categories, 29:874-895, 2014. Google Scholar
  9. Makoto Fujiwara and Taishi Kurahashi. Refining the arithmetical hierarchy of classical principles. Mathematical Logic Quarterly, 68(3):318-345, 2022. Google Scholar
  10. J. M. E. Hyland. The effective topos. In The L. E. J. Brouwer Centenary Symposium, volume 110 of Stud. Logic Foundations Math. North-Holland, pages 165-216, 1982. Google Scholar
  11. J. M. E. Hyland, Peter T. Johnstone, and Andrew M. Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc., 88:205-232, 1980. Google Scholar
  12. Peter T. Johnstone. Conditions related to De Morgan’s law. Applications of sheaves, 753:479-491, 1979. Google Scholar
  13. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium, 2 vols. Oxford Logic Guides 43, 44. Clarendon Press, 2002. Google Scholar
  14. Takayuki Kihara. Lawvere-tierney topologies for computability theorists. Transactions of the American Mathematical Society, Series B, pages 48-85, 2023. Google Scholar
  15. Stephen C. Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10:109-124, 1945. Google Scholar
  16. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101-128. Amsterdam: North-Holland Pub. Co., 1959. Google Scholar
  17. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986. Google Scholar
  18. Vladimir Lifschitz. CT₀ is stronger than CT₀!. Proceedings of the American Mathematical Society, 73:101-106, 1979. Google Scholar
  19. Saunders MacLane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992. Google Scholar
  20. Wesley Phoa. Relative computability in the effective topos. Mathematical Proceedings of the Cambridge Philosophical Society, 106:419-422, 1989. Google Scholar
  21. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, Vol.I, volume 121 of Lecture Notes in Mathematics. Elsevier, 1988. Google Scholar
  22. Anne Sjerp Troelstra (ed.). Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Studies in Logic and the Foundations of Mathematics. Springer-Verlag, 1973. Google Scholar
  23. Jaap van Oosten. Two remarks on the Lifschitz realizability topos. Journal of Symbolic Logic, 61(1):70-79, 1996. Google Scholar
  24. Jaap van Oosten. The modified realizability topos. Journal of Pure and Applied Algebra, 116:273-289, 1997. Google Scholar
  25. Jaap van Oosten. Realizability: an introduction to its categorical side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2008. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail