Enriched Categorical Logic

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

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.