A topos for continuous logic. (English) Zbl 1500.03019
Continous first-order logic, reminiscent of the earlier logic introduced by C. C. Chang and H. J. Keisler [Continuous model theory. Princeton University Press, Princeton, NJ (1966; Zbl 0149.00402)], was introduced by I. Ben Yaacov and A. Usvyatsov [Trans. Am. Math. Soc. 362, No. 10, 5213–5259 (2010; Zbl 1200.03024)] studying complete metric spaces of finite diameter, say of dimension \(1\), terms being uniformly continuous functions between such metric spaces, and formulas being uniformly continuous functions into the unit interval. It allows the study of elementary classes of complete metric structures that are not elementary in classical model theory. Many concepts from classical logic such as completeness and compactness can be given continuous counterparts.
This paper analyzes continuous logic from the point of view of categorical logic. The papers [J.-M. Albert, “Bradd Hart metric logical categories and conceptual completeness for first order continuous logic”, Preprint, arXiv:1607.03068; S. Cho, J. Symb. Log. 85, No. 3, 1044–1078 (2020; Zbl 1462.03031)] are precursors, where they start by modifying the standard framework of categorical logic, putting much emphasis on F. W. Lawvere’s ideas [Rend. Semin. Mat. Fis. Milano 43, 135–166 (1974; Zbl 0335.18006); Repr. Theory Appl. Categ. 2002, No. 1, 1–37 (2002; Zbl 1078.18501)] to understand metric spaces as enriched categories. In contrast, the analysis in this paper does not rely on enriched category theory, but instead uses conventional concepts from categorical logic such as the logic of a topos and Lawvere’s notion of a hyperdoctrine [loc. cit.].
The authors start with a new hyperdoctrine, which is called CMT (continuous model theory). The principal objective in this paper is to embed this hyperdoctrine into the subobject hyperdoctrine of a Grothendieck topos. It is shown that continuous logic is subsumed by the framework for categorical logic provided by topos theory. For this embedding the authors use a simplification of the hyperdoctrine CMT, which is denoted by U. It is also shown that the category of equivalence relations over U is equivalent to the category of complete metric spaces and uniformly continuous maps.
This paper analyzes continuous logic from the point of view of categorical logic. The papers [J.-M. Albert, “Bradd Hart metric logical categories and conceptual completeness for first order continuous logic”, Preprint, arXiv:1607.03068; S. Cho, J. Symb. Log. 85, No. 3, 1044–1078 (2020; Zbl 1462.03031)] are precursors, where they start by modifying the standard framework of categorical logic, putting much emphasis on F. W. Lawvere’s ideas [Rend. Semin. Mat. Fis. Milano 43, 135–166 (1974; Zbl 0335.18006); Repr. Theory Appl. Categ. 2002, No. 1, 1–37 (2002; Zbl 1078.18501)] to understand metric spaces as enriched categories. In contrast, the analysis in this paper does not rely on enriched category theory, but instead uses conventional concepts from categorical logic such as the logic of a topos and Lawvere’s notion of a hyperdoctrine [loc. cit.].
The authors start with a new hyperdoctrine, which is called CMT (continuous model theory). The principal objective in this paper is to embed this hyperdoctrine into the subobject hyperdoctrine of a Grothendieck topos. It is shown that continuous logic is subsumed by the framework for categorical logic provided by topos theory. For this embedding the authors use a simplification of the hyperdoctrine CMT, which is denoted by U. It is also shown that the category of equivalence relations over U is equivalent to the category of complete metric spaces and uniformly continuous maps.
Reviewer: Hirokazu Nishimura (Tsukuba)
MSC:
| 03G30 | Categorical logic, topoi |
| 03C66 | Continuous model theory, model theory of metric structures |
| 18F10 | Grothendieck topologies and Grothendieck topoi |
References:
| [1] | Clearly, every member Ψ contains the diagonal. |
| [2] | If U ∈ Ψ, then U a ⊆ U for some a ∈ (0, 1] ∩ Q. From the symmetry of R, it follows that U b ⊆ U −1 a for some b ∈ (0, 1] ∩ Q, so U −1 a ∈ Ψ hence U −1 ∈ Ψ. |
| [3] | If U ∈ Ψ, then U a ⊆ U for some a ∈ (0, 1] ∩ Q. From the transitivity of R, it follows that U b • U b ⊆ U a ⊆ U for some b ∈ (0, 1] ∩ Q |
| [4] | If U, V ∈ Ψ, then U a ⊆ U and U b ⊆ V with a, b ∈ (0, 1] ∩ Q. Then U min(a,b) ⊆ U a ∩ U b ⊆ U ∩ V , so U ∩ V ∈ Ψ. |
| [5] | Clearly, if U ∈ Ψ and U ⊆ V then V ∈ Ψ. |
| [6] | To show that d is single-valued, let ε > 0. Since d induces Ψ, there exists a γ > 0 such that V γ ⊆ U ε . Let δ = 1 2 γ. If x, y and y ′ are elements of X such that max(d(x, y), d(x, y ′ )) ≤ δ, then (y, y ′ ) ∈ V γ , hence R(y, y ′ ) ≤ ε. A similar argument shows that the converse of d is single-valued as well. |
| [7] | Clearly, d is total, and the converse holds as well. |
| [8] | So G : pMet 1 → ER(U) is essentially surjective. This fact, together with Proposition 5.10 and Proposition 5.9, shows that G : cMet 1 → ER(U) is an equivalence. 5.12. Remark. The argument is the theorem above can be extended to show that there is a functor from the category ER(U) to the category of uniform spaces. It may be interesting to study this functor further: for instance, is it an embedding? the hyperdoctrine CMT into the subobject hyper-doctrine of a topos. In this section we take the first step in that direction: we will embed CMT into the subobject hyperdoctrine of a coherent category. The hyperdoctrine that we will consider is the category of partial equivalence relations (PERs) over the hyper-doctrine U. By characterising the subobjects in categories of partial equivalence relations as strict relations, we will be able to define an embedding from CMT into the subobject hyperdoctrine of PER(U). |
| [9] | Jean-Martin Albert and Bradd Hart, Metric logical categories and conceptual complete-ness for first order continuous logic. Preprint available from arXiv:1607.03068, 2016. |
| [10] | Itai Ben Yaacov, Alexander Berenstein, C. Ward Henson, and Alexander Usvyatsov, Model theory for metric structures. In: Model theory with applications to algebra and analysis, volume 2. London Math. Soc. Lecture Note Ser., Cambridge Univ. Press, Cambridge, volume 350, 2008, 315-427. · Zbl 1233.03045 |
| [11] | Itai Ben Yaacov, Itai and Alexander Usvyatsov, Alexander. Continuous first order logic and local stability, Trans. Amer. Math. Soc. 362 (10) (2010), 5213-5259. · Zbl 1200.03024 |
| [12] | Carsten Butz and Peter Johnstone, Classifying toposes for first-order theories. Ann. Pure Appl. Logic 91(1) (1998), 33-58. · Zbl 0893.03027 |
| [13] | C.C. Chang and H. Jerome Kesiler, Continuous model theory. Princeton University Press, Princeton, 1966. · Zbl 0149.00402 |
| [14] | Simon Cho, Categorical semantics of metric spaces and continuous logic. Preprint avaible from arXiv:1901.09077, 2019. · Zbl 1462.03031 |
| [15] | R. Engelking, General topology. Heldermann, Berlin, 1989. · Zbl 0684.54001 |
| [16] | Daniel Figueroa, A categorical analysis for continuous logic. MSc thesis, University of Amsterdam. Available from https://scripties.uba.uva.nl, 2020. |
| [17] | Jonas Frey, Categories of partial equivalence relations as localizations. To appear in the Journal of Pure and Applied Algebra, in press, 2022. |
| [18] | J.M.E. Hyland, P.T. Johnstone and A.M. Pitts, Tripos theory. Mathematical Proceedings of the Cambridge Philosophical Society 88 (2) (1980), 205-232. · Zbl 0451.03027 |
| [19] | Peter T. Johnsone, Sketches of an elephant: a topos theory compendium. Clarendon Press, Oxford, 2002. · Zbl 1071.18001 |
| [20] | F. William Lawvere, Adjointness in Foundations. Dialectica 23 (3-4) (1969), 281-296. · Zbl 0341.18002 |
| [21] | F. William Lawvere, Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano 43 (1973), 135-166. · Zbl 0335.18006 |
| [22] | Saunders Mac Lane and Ieke Moerdijk, Sheaves in geometry and logic -A first introduc-tion to topos theory. Corrected reprint of the 1992 edition. Universitext, Springer-Verlag, New York, 1994. · Zbl 0822.18001 |
| [23] | Maria Emilia Maietti and Giuseppe Rosolini. Unifying Exact Completions, Applied Cat-egorical Structures, 23 (2013), 43-52. · Zbl 1386.03074 |
| [24] | Andrew M. Pitts, Tripos Theory in Retrospect. Electronic Notes in Theoretical Computer Science 23 (1) (1999), 111-127. |
| [25] | Andrew M. Pitts, Categorical logic. Handbook of logic in computer science, Vol. 5, Oxford Univ. Press, New York, 2000, 39-128. |
| [26] | Walter Rudin, Principles of mathematical analysis. McGraw-Hill, New York, 1976. · Zbl 0346.26002 |
| [27] | J. van Oosten, Realizability: an Introduction to its Categorical Side. Elsevier, Amsterdam, 2008. · Zbl 1225.03002 |
| [28] | Institute for Logic, Language and Computation, Universiteit van Amsterdam, Postbus 90242, 1090 GE Amsterdam, The Netherlands Email: daefigueroa@gmail.com B.vandenBerg3@uva.nl |
| [29] | Maria Manuel Clementino, Universidade de Coimbra: mmc@mat.uc.pt Valeria de Paiva, Nuance Communications Inc: valeria.depaiva@gmail.com Richard Garner, Macquarie University: richard.garner@mq.edu.au Ezra Getzler, Northwestern University: getzler (at) northwestern(dot)edu |
| [30] | Dirk Hofmann, Universidade de Aveiro: dirk@ua.pt Joachim Kock, Universitat Autònoma de Barcelona: kock (at) mat.uab.cat Stephen Lack, Macquarie University: steve.lack@mq.edu.au Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Matias Menni, Conicet and Universidad Nacional de La Plata, Argentina: matias.menni@gmail.com Susan Niefield, Union College: niefiels@union.edu |
| [31] | Kate Ponto, University of Kentucky: kate.ponto (at) uky.edu Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca Jiří Rosický, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Michael Shulman, University of San Diego: shulman@sandiego.edu Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu |
| [32] | Tim Van der Linden, Université catholique de Louvain: tim.vanderlinden@uclouvain.be |
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.
