Enriched Categorical Logic

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.