Realizability with a local operator of A. M. Pitts. (English) Zbl 1418.03148
Summary: We study a notion of realizability with a local operator \(\mathcal J\) which was first considered by A. M. Pitts in his thesis [The theory of triposes. Cambridge: Cambridge Univ. (PhD Thesis) (1981)]. Using the Suslin-Kleene theorem, we show that the representable functions for this realizability are exactly the hyperarithmetical \((\Delta_1^1)\) functions.
We show that there is a realizability interpretation of nonstandard arithmetic, which, despite its classical character, lives in a very non-classical universe, where the Uniformity Principle holds and König’s Lemma fails. We conjecture that the local operator gives a useful indexing of the hyperarithmetical functions.
We show that there is a realizability interpretation of nonstandard arithmetic, which, despite its classical character, lives in a very non-classical universe, where the Uniformity Principle holds and König’s Lemma fails. We conjecture that the local operator gives a useful indexing of the hyperarithmetical functions.
MSC:
| 03C62 | Models of arithmetic and set theory |
| 03G30 | Categorical logic, topoi |
| 03H15 | Nonstandard models of arithmetic |
References:
| [1] | 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 |
| [2] | Lee, S.; van Oosten, J., Basic subtoposes of the effective topos, Ann. Pure Appl. Logic, 164, 866-883 (2013) · Zbl 1288.18001 |
| [3] | McCarty, Charles, Variations on a thesis: intuitionism and computability, Notre Dame J. Form. Log., 28, 4, 536-580 (1987) · Zbl 0644.03002 |
| [4] | Moerdijk, I., A model for intuitionistic nonstandard arithmetic, Ann. Pure Appl. Logic, 73, 37-51 (1995) · Zbl 0829.03040 |
| [5] | Moschovakis, Y., Elementary Induction on Abstract Structures, Stud. Log., vol. 77 (2008), North-Holland: North-Holland Amsterdam: Dover, reprinted by |
| [6] | Odifreddi, P., Classical Recursion Theory, Stud. Log., vol. 125 (1989), North-Holland · Zbl 0931.03057 |
| [7] | Pitts, A. M., The theory of triposes (1981), Cambridge University, available at |
| [8] | Rogers, H., Theory of Recursive Functions and Effective Computability (1987), McGraw-Hill: MIT Press: McGraw-Hill: MIT Press Cambridge, MA, reprinted by · Zbl 0183.01401 |
| [9] | Rosolini, G., Continuity and effectiveness in topoi, PhD thesis (1986), University of Oxford, available electronically at |
| [10] | Skolem, Th., Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen, Fund. Math., 23, 150-161 (1934) · Zbl 0010.04902 |
| [11] | van den Berg, Benno; van Oosten, Jaap, Arithmetic is categorical (2011), Note, available at |
| [12] | van Oosten, J., Realizability: An Introduction to Its Categorical Side, Stud. Log., vol. 152 (2008), North-Holland · Zbl 1225.03002 |
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.
