Elementary doctrines as coalgebras. (English) Zbl 1469.18008
Hyperdoctrines were introduced by Lawvere as a categorical way to study logic and in particular first order theories [F. W. Lawvere, Dialectica 23, 281–296 (1969; Zbl 0341.18002)]. The relation was made precise by Seely, who proved there is an equivalence between categories of first order theories and hyperdoctrines [R. A. G. Seely, Z. Math. Logik Grundlagen Math. 29, 505–542 (1983; Zbl 0565.03032)].
Motivated by the desire to present a theory of equivalence relations, Maietti and Rosolini generalized hyperdoctrines to primary doctrines, which correspond to first-order theories with binary conjunctions and a true constant, and also introduced the particular case of elementary doctrines, which correspond to the aforementioned first order theories with an additional equality predicate [M. E. Maietti and G. Rosolini, Log. Univers. 7, No. 3, 371–402 (2013; Zbl 1288.03049)]. For example, in [M. E. Maietti and G. Rosolini, Theory Appl. Categ. 27, 445–463 (2013; Zbl 1288.03048)] Maietti and Rosolini show how to construct an elementary quotient completion out of every elementary doctrine.
D. Trotta [Existential completion and pseudo-distributive laws: an algebraic approach to the completion of doctrines. Università degli Studi di Trento. 89–119 (PhD Thesis) (2019)] showed that that this construction is in fact left adjoint to the inclusion of quotient complete elementary doctrines into elementary doctrines. Trotta also showed the adjunction is pseudo-monadic, deducing that elementary doctrines with quotients are pseudo-algebras over elementary doctrines, giving us an elegant application of categorical methods (monads and algebras) to logic (the relation between elementary doctrines and elementary doctrines with quotients).
Going in the other direction in [F. Pasquali, Appl. Categ. Struct. 23, No. 1, 29–41 (2015; Zbl 1305.03064)] the second author builds on the construction of the elementary quotient completion to construct a cofree elementary doctrine out of a primary doctrine by proving it is a right adjoint to the inclusion of elementary doctrines in primary doctrines. The construction of a right adjoint and the pseudo-monadic adjunction by Trotta suggests analyzing the comonadic properties of this adjunction, which is precisely the aim of this paper.
In this paper, the authors first prove that the adjunction constructed by the second author is in fact a \(2\)-adjunction between the \(2\)-categories of elementary doctrines and primary doctrines (Proposition \(3.1\)) and then show that this \(2\)-adjunction is \(2\)-comonadic (Theorem \(3.2\)), implying that elementary doctrines are simply \(2\)-coalgebras over primary doctrines, opening up the possibility of applying categorical methods (comonads) to the study of elementary doctrines and logic.
As a first application the authors prove in Section \(4\) that the cofree elementary doctrine construction can be used to transform every intuitionistic first order theory into one that has uniform elimination of imaginaries (Theorem \(4.2\)) as defined in [B. Poizat, J. Symb. Log. 48, 1151–1170 (1983; Zbl 0537.03023)] in such a way that every model of the original theory can be turned functorially into a model of the new theory that has uniform elimination of imaginaries (Proposition \(4.3\)).
In the final section (Section \(5\)) the results of Section \(4\) are applied to gain a better understanding of Shelah’s construction [S. Shelah, Classification theory and the number of non-isomorphic models. Amsterdam etc.: North-Holland (1990; Zbl 0713.03013)], which in [V. Harnik, in: Models, logics, and higher-dimensional categories: A tribute to the work of Mihály Makkai. Proceedings of a conference, CRM, Montréal, Canada, June 18–20, 2009. Providence, RI: American Mathematical Society (AMS). 79–106 (2011; Zbl 1243.03080)] was proven by Harnik to correspond to pretopos completion. In fact in Proposition \(5.1\) (which is proven in Appendix \(A\)) the authors give an alternative characterization of the pretopos completion and then apply that to the results of Section \(4\) to get Shelah’s construction for general intuitionistic first order theories.
Motivated by the desire to present a theory of equivalence relations, Maietti and Rosolini generalized hyperdoctrines to primary doctrines, which correspond to first-order theories with binary conjunctions and a true constant, and also introduced the particular case of elementary doctrines, which correspond to the aforementioned first order theories with an additional equality predicate [M. E. Maietti and G. Rosolini, Log. Univers. 7, No. 3, 371–402 (2013; Zbl 1288.03049)]. For example, in [M. E. Maietti and G. Rosolini, Theory Appl. Categ. 27, 445–463 (2013; Zbl 1288.03048)] Maietti and Rosolini show how to construct an elementary quotient completion out of every elementary doctrine.
D. Trotta [Existential completion and pseudo-distributive laws: an algebraic approach to the completion of doctrines. Università degli Studi di Trento. 89–119 (PhD Thesis) (2019)] showed that that this construction is in fact left adjoint to the inclusion of quotient complete elementary doctrines into elementary doctrines. Trotta also showed the adjunction is pseudo-monadic, deducing that elementary doctrines with quotients are pseudo-algebras over elementary doctrines, giving us an elegant application of categorical methods (monads and algebras) to logic (the relation between elementary doctrines and elementary doctrines with quotients).
Going in the other direction in [F. Pasquali, Appl. Categ. Struct. 23, No. 1, 29–41 (2015; Zbl 1305.03064)] the second author builds on the construction of the elementary quotient completion to construct a cofree elementary doctrine out of a primary doctrine by proving it is a right adjoint to the inclusion of elementary doctrines in primary doctrines. The construction of a right adjoint and the pseudo-monadic adjunction by Trotta suggests analyzing the comonadic properties of this adjunction, which is precisely the aim of this paper.
In this paper, the authors first prove that the adjunction constructed by the second author is in fact a \(2\)-adjunction between the \(2\)-categories of elementary doctrines and primary doctrines (Proposition \(3.1\)) and then show that this \(2\)-adjunction is \(2\)-comonadic (Theorem \(3.2\)), implying that elementary doctrines are simply \(2\)-coalgebras over primary doctrines, opening up the possibility of applying categorical methods (comonads) to the study of elementary doctrines and logic.
As a first application the authors prove in Section \(4\) that the cofree elementary doctrine construction can be used to transform every intuitionistic first order theory into one that has uniform elimination of imaginaries (Theorem \(4.2\)) as defined in [B. Poizat, J. Symb. Log. 48, 1151–1170 (1983; Zbl 0537.03023)] in such a way that every model of the original theory can be turned functorially into a model of the new theory that has uniform elimination of imaginaries (Proposition \(4.3\)).
In the final section (Section \(5\)) the results of Section \(4\) are applied to gain a better understanding of Shelah’s construction [S. Shelah, Classification theory and the number of non-isomorphic models. Amsterdam etc.: North-Holland (1990; Zbl 0713.03013)], which in [V. Harnik, in: Models, logics, and higher-dimensional categories: A tribute to the work of Mihály Makkai. Proceedings of a conference, CRM, Montréal, Canada, June 18–20, 2009. Providence, RI: American Mathematical Society (AMS). 79–106 (2011; Zbl 1243.03080)] was proven by Harnik to correspond to pretopos completion. In fact in Proposition \(5.1\) (which is proven in Appendix \(A\)) the authors give an alternative characterization of the pretopos completion and then apply that to the results of Section \(4\) to get Shelah’s construction for general intuitionistic first order theories.
Reviewer: Nima Rasekh (Lausanne)
MSC:
| 18C50 | Categorical semantics of formal languages |
| 03G30 | Categorical logic, topoi |
| 18C20 | Eilenberg-Moore and Kleisli constructions for monads |
| 03B10 | Classical first-order logic |
| 03B20 | Subsystems of classical logic (including intuitionistic logic) |
| 03C45 | Classification theory, stability, and related concepts in model theory |
Citations:
Zbl 0341.18002; Zbl 0565.03032; Zbl 1288.03049; Zbl 1288.03048; Zbl 1305.03064; Zbl 0537.03023; Zbl 0713.03013; Zbl 1243.03080References:
| [1] | Carboni, A., Some free constructions in realizability and proof theory, J. Pure Appl. Algebra, 103, 117-148 (1995) · Zbl 0839.18002 |
| [2] | Carboni, A.; Lack, S.; Walters, R., Introduction to extensive and distributive categories, J. Pure Appl. Algebra, 84, 145-158 (1993) · Zbl 0784.18001 |
| [3] | Carboni, A.; Vitale, E., Regular and exact completions, J. Pure Appl. Algebra, 125, 79-117 (1998) · Zbl 0891.18002 |
| [4] | Cori, R.; Lascar, D., Mathematical Logic (2001), Oxford Univ. Press: Oxford Univ. Press Oxford |
| [5] | Harnik, V., Model theory vs. categorical logic: two approaches to pretopos completion, (Hart, B.; Kucera, T.; Pillay, A.; Scott, P.; Seely, R., Models, Logics, and Higher-Dimensional Categories: a Tribute to the Work of Mihaly Makkai. Models, Logics, and Higher-Dimensional Categories: a Tribute to the Work of Mihaly Makkai, CRM Proceedings and Lecture Notes, vol. 53 (2011), Amer. Math. Soc.: Amer. Math. Soc. Providence), 79-106 · Zbl 1243.03080 |
| [6] | Hodges, W., Model Theory, Encyclopedia Math. Appl., vol. 42 (1993) · Zbl 0789.03031 |
| [7] | Jacobs, B., Categorical Logic and Type Theory, Stud. Logic Found. Math., vol. 141 (1999) · Zbl 0911.03001 |
| [8] | Johnstone, P., Sketches of an Elephant: A Topos Theory Compendium, Oxford Logic Guides, vol. 43 (2002), The Clarendon Press, Oxford Univ. Press: The Clarendon Press, Oxford Univ. Press New York · Zbl 1071.18001 |
| [9] | Kock, A., Monads for which structures are adjoint to units, J. Pure Appl. Algebra, 104, 41-59 (1995) · Zbl 0849.18008 |
| [10] | Lawvere, F. W., Equality in hyperdoctrines and comprehension schema as an adjoint functor, (Heller, A., Proc. New York Symposium on Application of Categorical Algebra (1970), Amer. Math. Soc.), 1-14 · Zbl 0234.18002 |
| [11] | Lawvere, F. W., Metric spaces, generalized logic, and closed categories, Rend. Semin. Mat. Fis. Milano. Rend. Semin. Mat. Fis. Milano, Theory Appl. Categ., 1, 1-37 (2002), also available as · Zbl 1078.18501 |
| [12] | Lawvere, F. W., Adjointness in foundations, Dialectica, 23, 281-296 (1969) · Zbl 0341.18002 |
| [13] | Maietti, M.; Pasquali, F.; Rosolini, G., Triposes, exact completions, and Hilbert’s ε-operator, Tbil. Math. J., 10, 141-166 (2017) · Zbl 1401.03109 |
| [14] | Maietti, M.; Rosolini, G., Elementary quotient completion, Theory Appl. Categ., 27, 445-463 (2013) · Zbl 1288.03048 |
| [15] | Maietti, M.; Rosolini, G., Quotient completion for the foundation of constructive mathematics, Log. Univers., 7, 371-402 (2013) · Zbl 1288.03049 |
| [16] | Maietti, M.; Rosolini, G., Unifying exact completions, Appl. Categ. Struct., 23, 43-52 (2015) · Zbl 1386.03074 |
| [17] | Maietti, M.; Rosolini, G., Relating quotient completions via categorical logic, (Probst, D.; Schuster, P., Concepts of Proof in Mathematics, Philosophy, and Computer Science (2016), De Gruyter), 229-250 · Zbl 1433.03164 |
| [18] | Makkai, M.; Reyes, G., First Order Categorical Logic, Lecture Notes in Math., vol. 611 (1977) · Zbl 0357.18002 |
| [19] | Pasquali, F., A co-free construction for elementary doctrines, Appl. Categ. Struct., 23, 29-41 (2015) · Zbl 1305.03064 |
| [20] | Pitts, A., Categorical logic, (Abramsky, S.; Gabbay, D.; Maibaum, T., Algebraic and Logical Structures. Algebraic and Logical Structures, Handbook of Logic in Computer Science, vol. 5 (2000), Oxford Univ. Press: Oxford Univ. Press New York), 39-128, Chapter 2 · Zbl 1035.03001 |
| [21] | Pitts, A., Tripos theory in retrospect, Math. Struct. Comput. Sci., 12, 265-279 (2002) · Zbl 1005.18005 |
| [22] | Poizat, B., Une théorie de Galois imaginaire, J. Symb. Log., 48, 1151-1170 (1983) · Zbl 0537.03023 |
| [23] | Rutten, J., Elements of generalized ultrametric domain theory, Theor. Comput. Sci., 170, 349-381 (1996) · Zbl 0874.68189 |
| [24] | Shelah, S., Classification Theory and the Number of Nonisomorphic Models, Stud. Logic Found. Math., vol. 92 (1990) · Zbl 0713.03013 |
| [25] | Streicher, T., Fibred categories (2019), available at |
| [26] | Trotta, D., Existential completion and pseudo-distributive laws: an algebraic approach to the completion of doctrines, 89-119 (2019), Università degli Studi di Trento, Doctoral thesis in Mathematics |
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.
