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 的无限宇宙；- 度量，与连续和度量模型理论的联系。