Published
Tripos models of Internal Set Theory
Keywords:
topos theory, tripos theory, internal set theory, hyperdoctrine, nonstandard analysis (en)Teoría de topos, hiperdoctrina (es)
Downloads
We introduce a categorical approach to nonstandard methods, loosely inspired on Internal Set Theory (IST) and reliant on the rich notions of hyperdoctrine and tripos from categorical logic. A different point of view is adopted: the axioms of IST should be expressed in terms of interactions between doctrines, which can be thought of as saying that instead of adding a new predicate we only add new quantifiers. Moreover, it differs from the typical approaches in that the foremost axiom is Standardisation rather than Transfer, all of which can be expressed in a point-free way. This opens the way to the usage of nonstandard proofs methods in the internal language of a doctrine.
References
J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts, Tripos theory, Mathematical Proceedings of the Cambridge Philosophical Society 88 (1980), no. 2, 205-232.
Anders Kock and Chr. Juul Mikkelsen, Topos-theoretic factorization of non-standard extensions, Victoria Symposium on Nonstandard Analysis (Berlin, Heidelberg) (Albert Hurd and Peter Loeb, eds.), Springer Berlin Heidelberg, 1974, pp. 122-143.
J. Lambek and P. J. Scott, Introduction to higher-order categorical logic, Cambridge University Press, 1988.
F. W. Lawvere, Quantifiers and sheaves, Actes, Congrès intern, math., 1, 1970, pp. 329-334.
Ieke Moerdijk, A model for intuitionistic non-standard arithmetic, Annals of Pure and Applied Logic 73 (1995), no. 1, 37-51, A Tribute to Dirk van Dalen.
Edward Nelson, Internal set theory: A new approach to nonstandard analysis, Bull. Amer. Math. Soc. 83 (1977), no. 6, 1165-1198.
José Vitor Paiva Miranda De Siqueira, Tripos models of internal set theory,(2022).
Erik Palmgren, A constructive approach to nonstandard analysis, Annals of Pure and Applied Logic 73 (1995), no. 3, 297-325.
Erik Palmgren, Developments in constructive nonstandard analysis, Bull. Symbolic Logic 4 (1998), no. 3, 233-272.
Erik Palmgren, Real numbers in the topos of sheaves over the category of filters, Journal of Pure and Applied Algebra 160 (2001), no. 2, 275-284.
A. M. Pitts, The theory of triposes, Ph.D. thesis, University of Cambridge, 1981.
Michael Shulman, Comparing material and structural set theories, Annals of Pure and Applied Logic 170 (2019), no. 4, 465-504.
José Siqueira, Nonstandard proof methods in toposes, arXiv:2308.16030.
J. van Oosten, Realizability: An introduction to its categorical side, ISSN, Elsevier Science, 2008.