Basic subtoposes of the effective topos. (English) Zbl 1288.18001
This article studies the lattice of local operators in M. Hyland’s effective topos. Reminding that subtoposes of a topos \(\varepsilon\) are in 1-1 correspondence with local operators in \(\varepsilon\), and that local operators are some endomaps on the subobject classifier of \(\varepsilon\), since many variations on realizability arise as the internal logic of subtoposes of the effective topos, the motivation of the paper is clear: to provide instruments and insight on realizability models in toposes.
The first technical contribution of the work is to show that every local operator is the internal join of a family of subsets of \(\mathbb{N}\) (Theorem 2.4 in the article). But the main innovation presented here is the technical notion of sight, a tool by which it becomes viable to study inequalities between basic local operators. Sights are then used to present a concrete definition of truth for first-order arithmetic in subtoposes corresponding to local operators.
The paper is very technical and the reader must be well acquainted with topos theory in general, and the construction and the properties of the effective topos in particular. Nevertheless, the conceptual width and depth of the paper is of interest for any researcher wishing to study realizability, and how it connects to topos theory, providing essential instruments to study effectiveness in a completely abstract way.
The first technical contribution of the work is to show that every local operator is the internal join of a family of subsets of \(\mathbb{N}\) (Theorem 2.4 in the article). But the main innovation presented here is the technical notion of sight, a tool by which it becomes viable to study inequalities between basic local operators. Sights are then used to present a concrete definition of truth for first-order arithmetic in subtoposes corresponding to local operators.
The paper is very technical and the reader must be well acquainted with topos theory in general, and the construction and the properties of the effective topos in particular. Nevertheless, the conceptual width and depth of the paper is of interest for any researcher wishing to study realizability, and how it connects to topos theory, providing essential instruments to study effectiveness in a completely abstract way.
Reviewer: Marco Benini (Buccinasco)
MSC:
| 18B25 | Topoi |
| 03G30 | Categorical logic, topoi |
| 03D80 | Applications of computability and recursion theory |
References:
| [1] | Brattka, V.; Gherardi, G., Weihrauch degrees, omniscience principles and weak computability, J. Symbolic Logic, 76, 1, 143-176 (2011) · Zbl 1222.03071 |
| [2] | Hyland, J. M.E., The effective topos, (Troelstra, A. S.; Van Dalen, D., The L.E.J. Brouwer Centenary Symposium (1982), North-Holland Publishing Company), 165-216 · Zbl 0522.03055 |
| [3] | Ishihara, H., An omniscience principle, the König lemma and the Hahn-Banach theorem, MLQ Math. Log. Q., 36, 3, 237-240 (1990) · Zbl 0684.03024 |
| [4] | Johnstone, P. T., Sketches of an Elephant, Oxford Logic Guides, vol. 43 (2002), Clarendon Press: Clarendon Press Oxford, (2 vols.) · Zbl 1071.18001 |
| [5] | Lambek, J.; Scott, P. J., Introduction to Higher Order Categorical Logic (1986), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0596.03002 |
| [6] | Mac Lane, S.; Moerdijk, I., Sheaves in Geometry and Logic (1992), Springer-Verlag · Zbl 0822.18001 |
| [7] | McCarty, Charles, Variations on a thesis: intuitionism and computability, Notre Dame J. Form. Log., 28, 4, 536-580 (1987) · Zbl 0644.03002 |
| [8] | Medvedev, Yu. T., Degrees of difficulty of the mass problems, Dokl. Akad. Nauk. SSSR, 140, 4, 501-504 (1955) · Zbl 0065.00301 |
| [9] | Menni, M., Closure operators in exact completions, Theory Appl. Categ., 8, 21, 522-540 (2001) · Zbl 1005.18004 |
| [10] | Moerdijk, I., A model for intuitionistic nonstandard arithmetic, Ann. Pure Appl. Logic, 73, 37-51 (1995) · Zbl 0829.03040 |
| [11] | Moerdijk, I.; Palmgren, E., Minimal models of Heyting arithmetic, J. Symbolic Logic, 62, 4, 1448-1460 (1997) · Zbl 0899.03044 |
| [12] | Phoa, W., Relative computability in the effective topos, Math. Proc. Cambridge Philos. Soc., 106, 419-422 (1989) · Zbl 0694.18004 |
| [13] | Pitts, A. M., The theory of triposes (1981), Cambridge University, available at: |
| [14] | Simpson, Stephen G., Mass problems, Slides of invited plenary talk given at Logic Colloquium, Bern 2008, available at: · Zbl 1141.03018 |
| [15] | Sorbi, A., Some remarks on the structure of the Medvedev lattice, J. Symbolic Logic, 55, 2, 831-853 (1990) · Zbl 0703.03022 |
| [16] | Terwijn, S., Constructive logic and the Medvedev lattice, Notre Dame J. Form. Log., 47, 1, 73-82 (2006) · Zbl 1107.03024 |
| [17] | Terwijn, S., The Medvedev lattice of computably closed sets, Arch. Math. Logic, 45, 2, 179-190 (2006) · Zbl 1090.03010 |
| [18] | van den Berg, Benno; van Oosten, Jaap, Arithmetic is categorical (2011), Note, available at: |
| [19] | van Oosten, J., Extension of Lifschitzʼ realizability to higher order arithmetic, and a solution to a problem of F. Richman, J. Symbolic Logic, 56, 964-973 (1991) · Zbl 0743.03036 |
| [20] | van Oosten, J., Two remarks on the Lifschitz realizability topos, J. Symbolic Logic, 61, 70-79 (1996) · Zbl 0854.03059 |
| [21] | van Oosten, J., Realizability: An Introduction to its Categorical Side, Stud. Log., vol. 152 (2008), North-Holland · Zbl 1225.03002 |
| [22] | van Oosten, J., Realizability with a local operator of A.M. Pitts, Theoret. Comput. Sci. (2013), in press, available electronically at: |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
