Enriched Categorical Logic

范畴逻辑涉及纯数学的两个基础领域：逻辑和范畴论之间的联系。逻辑学关注数学中语言和推理的研究，重点关注公理理论和这些公理所要描述的数学结构之间的相互作用。范畴论是代数的一种抽象形式，它提供了一种以统一的方式描述各种数学结构的语言，并以一种有效的方式将不同的数学领域联系起来。这两个领域之间的关系产生了范畴逻辑领域，它涉及使用范畴论的方法研究逻辑。在范畴论发展的早期，人们意识到，普通的范畴，即对象和任意两个对象之间的态射集合，不足以描述数学中的一些重要结构，特别是代数和拓扑学，因此有必要发展现在被称为丰富的范畴论。顾名思义，这是普通范畴论的一个更强大的版本，它在许多不同的背景下都有重要的应用：在具有加性、阿贝尔和微分渐变范畴的代数中；拓扑中有简单范畴和拓扑范畴；在理论计算机科学中使用富序范畴。在一个充实的范畴中，有对象，但对于任何两个对象，它们之间的态射不仅形成一个集合，而且可能具有附加的结构或性质。例如，在可交换环R上的模范畴中，态射可以相加，自然形成一个阿贝尔群；而在光滑流形和它们之间的光滑函数的范畴中，态射可以看作是拓扑空间中的点。一种精确的说法是，两个对象之间的态射是一个给定类别B的对象，称为充实的基。在代数、拓扑和分析方面的大量例子表明，丰富范畴理论是多么强大。逻辑学与普通范畴论之间的联系由来已久。给定一个理论，在逻辑的意义上，我们可以考虑它的模型的范畴，反之亦然，给定一个足够好的范畴，我们可以找到一个理论，它的模型范畴与我们开始时的范畴一致。此外，对于某些类别的理论，人们可以确定作为它们的纯粹范畴的模型而出现的类别的类别。例如，方程理论的模型范畴被称为有限变量，本质代数理论的模型范畴形成局部有限可呈现的范畴，规则理论对应于可定义的范畴；每一种都提供了在理论和模型之间来回转换的途径。这种二元性很有帮助，因为它们为解决问题提供了不同的观点（逻辑的或分类的）。当我们转向丰富的范畴论时，这种联系并不存在，原因很简单：我们还没有一个“丰富”的范畴逻辑版本。这是我们试图用这个项目来填补的主要空白。这个项目有几个具体而精确的里程碑，由直言逻辑基本定理的丰富对应提供。这包括引入丰富的语言、理论和模型，以及构建丰富的逻辑片段及其分类解释。此外，它的很大一部分将专门用于应用程序。我们设想了至少四个应用领域：- 2-范畴，与二维逻辑和二维变种的发展；-阿贝尔，研究加性模型理论和可定义的加性范畴；-简单，具有Riehl和Verity的无限宇宙的句法特征；-度量，与连续和度量模型理论的联系。

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.