Logical systems. I: Internal calculi.

*(English)*Zbl 1370.03086The 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:

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.

This paper, after introducing the necessary preliminaries, poses and answers two questions:

- (1)
- 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?
- (2)
- 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.

Reviewer: Marco Benini (Buccinasco)

##### MSC:

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.) |

PDF
BibTeX
XML
Cite

\textit{M. R. Przybylek}, J. Pure Appl. Algebra 221, No. 2, 449--489 (2017; Zbl 1370.03086)

Full Text:
DOI

##### References:

[1] | Sannella, D.; Tarlecki, A., Foundations of algebraic specification and formal software development, (2012), Springer Berlin, Heidelberg · Zbl 1237.68129 |

[2] | Lambek, J.; Scott, P. J., Introduction to higher order categorical logic, (1986), Cambridge University Press New York, NY, USA · Zbl 0596.03002 |

[3] | Goguen, J. A.; Burstall, R. M., Introducing institutions, (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) |

[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 |

[10] | M.R. Przybylek, Logical systems II: KZ-categories, 2015, in preparation. |

[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 · 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, NJ · Zbl 1175.18001 |

[15] | Barr, M.; Wells, C., Toposes, triples, and theories, Grundlehren der Mathematischen Wissenschaften, (1985), 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) |

[18] | Isbell, J., General function spaces, products and continuous lattices, Math. Proc. Camb. Philos. Soc., 100, 193-205, (September 1986) |

[19] | Steenrod, N. E., A convenient category of topological spaces, Mich. Math. J., 14, 2, 133-152, (May 1967) |

[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, 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) |

[26] | Johnstone, P., Sketches of an elephant: A topos theory compendium, Oxford Logic Guides, (2002), Clarendon Press Oxford · Zbl 1071.18002 |

[27] | Pitts, A. M., Polymorphism is set theoretic, constructively, (Category Theory and Computer Science, (1987), 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 |

[30] | Kelly, G. M.; Street, R., Review of the elements of 2-categories, (Kelly, G. M., Category Seminar, Lecture Notes in Mathematics, vol. 420, (1974), 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 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 |

[35] | R. Street, Categories in categories, and size matters, 2010. · Zbl 1411.18013 |

[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, 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.