Enriched Categorical Logic

Lead Research Organisation: The University of Manchester
Department Name: Mathematics

Abstract

Categorical logic concerns the link between two foundational areas of Pure Mathematics: logic and category theory. Logic is concerned with the study of language and reasoning in mathematics, with a focus on the interplay between axiomatic theories and the mathematical structures that these axioms are intended to describe. category theory, an abstract form of algebra, provides a language for describing a variety of mathematical constructions in a uniform way, and for relating different areas of mathematics in a efficient way. The relation between these two areas has given rise to the area of categorical logic, which is concerned with the study of logic using methods of category theory. Early in the development of category theory, it was realised that ordinary categories, in which one has objects and sets of morphisms between any two objects, are not sufficient to describe some important structures in mathematics, particularly in algebra and topology, and that it was necessary to develop what is now known as enriched category theory. As the name suggests, this is a more powerful version of ordinary category theory, which has important applications in many different contexts: in algebra with additive, abelian and differentially-graded categories; in topology with simplicial and topological categories; and in theoretical Computer Science with order-enriched categories. In an enriched category, one has objects, but for any two objects, morphisms between them do not form just a set but may possess additional structures or properties. For example, in the category of modules over a commutative ring R, morphisms can be added and naturally form an abelian group; while in the category of smooth manifolds and smooth functions between them, morphisms can be seen as the points of a topological space. One way to make this precise is to say that the morphisms between two objects are an object of a given category B, called the base of the enrichment. The large variety of examples, in algebra, topology, and analysis, suggests how powerful the theory of enriched categories is.

The connection between logic and ordinary category theory has long been established. Given a theory, in the sense of logic, one can consider the category of its models and vice versa, given a good enough category one can find a theory whose category of models coincides with the category we started with. Moreover, for some classes of theories one can determine the class of categories that arise as models of them in purely categorical terms. For instance, categories of models of equational theories are known as finitary varieties, categories of models of essentially algebraic theories form the locally finitely presentable categories, and regular theories correspond to the definable categories; each providing a way to go back and forth between theories and their models. These sort of dualities are helpful because they provide different points of view (logical or categorical) to attack problems. When moving to enriched category theory this connection does not exist for a very simple reason: we do not have yet an "enriched" version of categorical logic. This is the main gap that we seek to fill with this project.

This project has several concrete and precise milestones, provided by enriched counterparts of fundamental theorems of Categorical logic. This includes the introduction of enriched languages, theories, and models, as well as the construction of enriched fragments of logic and their categorical interpretations. Furthermore, a significant part of it will be devoted to applications. We envisage at least four areas of applications:
- 2-categorical, with the development of 2-dimensional logic and 2-dimensional varieties;
- abelian, with the study of additive model theory and definable additive categories;
- simplicial, with a syntactic characterisation of Riehl and Verity's infinity-cosmoi;
- metric, with connections to continuous and metric model theory.

Publications

10 25 50
publication icon
ROSICKÝ J (2025) ENRICHED CONCEPTS OF REGULAR LOGIC in The Journal of Symbolic Logic

publication icon
Rosický J. (2025) Enriched concepts of regular logic in Journal of Symbolic Logic

publication icon
Rosický J. (2024) Notions of enriched purity in Theory and Applications of Categories

 
Description Dame Kathleen Ollerenshaw Trust for the organization of a workshop
Amount £10,000 (GBP)
Organisation University of Manchester 
Sector Academic/University
Country United Kingdom
Start 12/2024 
End 01/2025
 
Description Accessible infinity cosmoi 
Organisation Max Planck Institute for Mathematics
Country Germany 
Sector Public 
PI Contribution Research project in the fruitful area of infinity-cosmoi, introduced by Riehl and Verity. The collaborators involved in the project are Yuki Maehara (Kyoto University) and Paula Verdugo (Max Planck Institute, Bonn)
Collaborator Contribution We study the virtual equipment associated to an infinity-cosmos and plan to show that this arises from a double category when the infinity-cosmos is moreover accessible.
Impact The collaboration is still in its first stages, the are no outcomes yet.
Start Year 2025
 
Description Accessible infinity cosmoi 
Organisation University of Kyoto
Country Japan 
Sector Academic/University 
PI Contribution Research project in the fruitful area of infinity-cosmoi, introduced by Riehl and Verity. The collaborators involved in the project are Yuki Maehara (Kyoto University) and Paula Verdugo (Max Planck Institute, Bonn)
Collaborator Contribution We study the virtual equipment associated to an infinity-cosmos and plan to show that this arises from a double category when the infinity-cosmos is moreover accessible.
Impact The collaboration is still in its first stages, the are no outcomes yet.
Start Year 2025
 
Description Enriched logic 
Organisation Masaryk University
Country Czech Republic 
Sector Academic/University 
PI Contribution Two of the papers I have published so fare are in collaboration with Prof Jiri Rosicky from masaryk University.
Collaborator Contribution The parteners have contributed in equal parts to the results presented in the papers.
Impact The two outcomes of this collaboration are the two journal publications "Notions of enriched purity" and "Enriched concepts of regular logic", appearing in Theory and applications of Categories and the Journal of Symbolic Logic respectively.
Start Year 2023