Logical systems. I: Internal calculi. (English) Zbl 1370.03086

The article is the first in a series of three, the others not yet published at the time of writing this review. The purpose of these articles is to lay down a 2-categorical approach to logical systems.
This paper, after introducing the necessary preliminaries, poses and answers two questions:
what properties a 2-category must possess to allow establishing the connection among \(\lambda\)-calculus, logic, and categorical constructions which is usually referred to as the Curry-Howard isomorphism?
what can be gained by those properties?

The key notion to answer the former question is discreteness, Definition 1.2 in the paper. By cleverly using this notion, the author extends the definition of fibred/internal connectives and polymorphism to an arbitrary 2-category with a notion of discreteness. Also, the concept of internally closed connectives is analysed and an appropriate extension of the naive approach is proposed and justified.
Then, a 2-functor realising any finitely complete 2-category \(\mathbb{C}\) with a notion of discreteness in the 2-category of the categories internal to discrete \(\mathbb{C}\)-objects is constructed so that the functor preserves internal connectives and polymorphic objects. This realisation maps \(\mathbb{C}\) to a full 2-subcategory if and only if the discrete objects are dense; it has a left adjoint if and only if \(\mathbb{C}\) has codescent objects of discrete truncated cosimplicial diagrams. Although very technical, these results generalise the more usual fibrational definitions when considered in the world of enriched categories.
Another contribution of the paper is that it shows that, when a 2-category is sufficiently rich, then its objects cannot have all the internal products unless degenerate. This result generalises Freyd’s theorem for categories internal to any tensored category.
Finally, it is proved that an object in a Cartesian 2-category is linearly complete if and only if it is linearly cocomplete. A direct consequence is that a category internal to a locally Cartesian closed category, which is worth reminding, allows to interpret dependent type theory, is internally complete if and only if it is internally cocomplete.
Despite the abundance of unavoidable technical concepts and proofs, this long and difficult article contains results, like the generalisation of Freyd’s theorem, which are worth alone the reading. And the overall picture which emerges provides a satisfying answer to the second question posed in the introduction.


03G30 Categorical logic, topoi
18A15 Foundations, relations to logic and deductive systems
18D05 Double categories, \(2\)-categories, bicategories and generalizations (MSC2010)
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
Full Text: DOI


[1] Sannella, D.; Tarlecki, A., Foundations of Algebraic Specification and Formal Software Development (2012), Springer: Springer Berlin, Heidelberg · Zbl 1237.68129
[2] Lambek, J.; Scott, P. J., Introduction to Higher Order Categorical Logic (1986), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 0596.03002
[3] Goguen, J. A.; Burstall, R. M., Introducing institutions, (Logics of Programs. Logics of Programs, Proceedings, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983 (1983)), 221-256 · Zbl 1288.03001
[4] Goguen, J. A.; Burstall, R. M., Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146 (January 1992) · Zbl 0799.68134
[5] Goguen, J. A.; Rosu, G., Institution morphisms, Form. Asp. Comput., 13, 3-5, 274-307 (2002) · Zbl 1001.68019
[6] Goguen, J. A., Data, schema, ontology and logic integration, Log. J. IGPL, 13, 6, 685-715 (2005) · Zbl 1094.68018
[7] Goguen, J. A., Three perspectives on information integration, (Semantic Interoperability and Integration (2005))
[8] Tarlecki, A., Quasi-varieties in abstract algebraic institutions, J. Comput. Syst. Sci., 33, 3, 333-360 (1986) · Zbl 0622.68033
[9] Gâinâ, G.; Popescu, A., An institution-independent generalization of Tarski’s elementary chain theorem, J. Log. Comput., 16, 6, 713-735 (2006) · Zbl 1123.03058
[11] Przybylek, M. R., Logical systems III: free semantics, preliminary draft (2014)
[12] Leinster, T., Higher Operads, Higher Categories, London Mathematical Society Lecture Note Series (2004), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1160.18001
[13] Bénabou, J., Introduction to Bicategories (1967), University of Chicago · Zbl 1375.18001
[14] Lurie, J., Higher Topos Theory, Annals of Mathematics Studies (2009), Princeton University Press: Princeton University Press Princeton, NJ · Zbl 1175.18001
[15] Barr, M.; Wells, C., Toposes, Triples, and Theories, Grundlehren der Mathematischen Wissenschaften (1985), Springer-Verlag: Springer-Verlag New York · Zbl 0567.18001
[16] Weber, M., Yoneda structures from 2-toposes, Appl. Categ. Struct., 15, 3, 259-323 (2007) · Zbl 1125.18001
[17] Jacobs, B., Comprehension categories and the semantics of type dependency, Theor. Comput. Sci., 107, 2, 169-207 (January 1993) · Zbl 0804.18007
[18] Isbell, J., General function spaces, products and continuous lattices, Math. Proc. Camb. Philos. Soc., 100, 193-205 (September 1986) · Zbl 0609.54010
[19] Steenrod, N. E., A convenient category of topological spaces, Mich. Math. J., 14, 2, 133-152 (May 1967) · Zbl 0145.43002
[20] Escardó, M.; Lawson, J.; Simpson, A., Comparing cartesian closed categories of (core) compactly generated spaces, Topol. Appl., 143, 1-3, 105-145 (2004) · Zbl 1066.54028
[21] Gordon, R.; Power, A. J.; Street, R., Coherence for Tricategories, Memoirs of the American Mathematical Society, vol. 117 (1995) · Zbl 0836.18001
[22] Kelly, M., Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Notes, vol. 64 (1982), Cambridge University Press · Zbl 0478.18005
[23] Reynolds, J. C., Types, abstraction and parametric polymorphism, (IFIP Congress (1983)), 513-523
[24] Abadi, M.; Plotkin, G. D., A per model of polymorphism and recursive types, (Proc. of the Fifth Annual IEEE Symposium on Logic in Computer Science. Proc. of the Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA (1990)), 355-365
[25] Seely, R. A.G., Categorical semantics for higher order polymorphic lambda calculus, J. Symb. Log., 52, 969-989 (December 1987) · Zbl 0642.03007
[26] Johnstone, P., Sketches of an Elephant: A Topos Theory Compendium, Oxford Logic Guides (2002), Clarendon Press: Clarendon Press Oxford · Zbl 1071.18002
[27] Pitts, A. M., Polymorphism is set theoretic, constructively, (Category Theory and Computer Science (1987), Springer-Verlag: Springer-Verlag London, UK), 12-39 · Zbl 0644.18003
[28] Hyland, J. M.E., A small complete category, Ann. Pure Appl. Log., 40, 2, 135-165 (1988) · Zbl 0659.18007
[29] Borceux, F., Handbook of Categorical Algebra, vols. 1, 2, 3 (1994), Cambridge University Press, Cambridge Books Online · Zbl 0803.18001
[30] Kelly, G. M.; Street, R., Review of the elements of 2-categories, (Kelly, G. M., Category Seminar. Category Seminar, Lecture Notes in Mathematics, vol. 420 (1974), Springer: Springer Berlin, Heidelberg), 75-103 · Zbl 0334.18016
[31] Ehresmann, C., Catégories structurées, Ann. Sci. Ec. Norm. Super., 80, 4, 349-426 (1963) · Zbl 0128.02002
[32] Jacobs, B., Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141 (1999), North Holland: North Holland Amsterdam · Zbl 0911.03001
[33] Phoa, W., An introduction to fibrations, topos theory, the effective topos, and modest sets (1992), Department of Computer Science, University of Edinburgh, Technical report
[34] Street, R., Fibrations in bicategories, Cah. Topol. Géom. Différ. Catég., 21, 2, 111-160 (1980) · Zbl 0436.18005
[36] Lack, S., Codescent objects and coherence, J. Pure Appl. Algebra, 175, 1-3, 223-241 (2002) · Zbl 1142.18301
[37] Mac Lane, S., Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5 (1978), Springer-Verlag · Zbl 0906.18001
[38] Street, R., Categorical and combinatorial aspects of descent theory, Appl. Categ. Struct., 12, 5-6, 537-576 (2004) · Zbl 1082.18011
[39] Pavlović, D., On completeness and cocompleteness in and around small categories, Ann. Pure Appl. Log., 74, 2, 121-152 (1995) · Zbl 0829.18001
[40] Reynolds, J. C., Polymorphism is not set-theoretic, (Kahn, Gilles; MacQueen, David B.; Plotkin, Gordon D., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, vol. 173 (1984), Springer), 145-156 · Zbl 0554.03012
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.