Enriched Categorical Logic

丰富的分类逻辑

• 批准号: EP/X027139/1
• 金额: $ 38.92万
• 依托单位: University of Manchester
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2024
• 资助国家: 英国
• 起止时间: 2024 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FX027139%2F1
• 关键词: 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.

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