Coalgebras, Modal Logic, Stone Duality

计算机编程的核心问题之一是，编写正确的程序或说服自己相信某些程序的正确性是非常困难的。解决这个问题的一种方法是使用逻辑。让我们首先简要地看看逻辑。我们可以使用逻辑来(1)做出关于世界的陈述，(2)定义一种陈述在世界上成立或不成立，(3)使用推理规则从给定的陈述中推导出新的陈述。‘World’可以意味着我们生活的世界，逻辑最初是为了对日常问题进行推理而发展起来的。在数学中，一个原因是关于数学对象的世界。数学世界足够丰富，可以对不同的计算概念进行建模。因此，数理逻辑允许我们为不同的计算模型设计不同的逻辑。与这一建议相关的逻辑称为模式逻辑。这一努力的结果应该是使关于计算的推理完全精确，从而消除人们在对程序进行推理时往往会犯的错误。2.在我的项目中，我将研究称为转换系统的特定计算模型。过渡系统由国家和国家之间的关系组成。其思想是，每个状态代表给定的计算时刻，这些关系描述计算如何从一个状态进行到另一个状态。该项目旨在为过渡系统提供一个通用的逻辑理论。它将通过下面的绕道建立逻辑和过渡系统之间的关系，允许我们使用某种数学理论，即斯通对偶性。最近的发展建议使用余代数来表示变迁系统。余代数与代数有一种特殊的关系-称为对偶性。就像在学校里解方程一样，代数可以用来表述推理原理。尤其是，这项建议的目的如下。将适当的逻辑与任何类型的过渡系统相关联。以显示如何将这些逻辑应用于验证有关程序的语句。研究数理逻辑的某些概念和工具如何适用于余代数及其逻辑。III.该项目将有助于将余代数理论作为过渡系统的一般理论，该理论是由许多研究人员在20世纪90年代发展起来的。这也将是对最近关于(模态)逻辑和余代数之间联系的工作的一个重要贡献。余代数和模态逻辑受到了数学和计算机科学领域不同领域的研究人员的关注，这项研究将揭示它们之间的新联系。在更广泛的背景下，该项目一方面关注计算模型的基础关系，另一方面关注逻辑的基本关系。余代数理论的发展为整合已有的见解和探索新的方向提供了可能。

I.One of the central problems of programming computers is that it isvery difficult to write correct programs or to convince yourself ofthe correctness of some program. One way to tackle this problem is theuse of logic.Let us first take a brief look at logic. We can use logic to (1) make statements about the world, (2) define when a statement holds or does not hold in the world, (3) deduce new statements from given ones using rules of reasoning.`World' can mean the world we live in and logic was originally indeeddeveloped to reason about everyday problems. In mathematics, the worldone reasons about is the world of mathematical objects. Themathematical world is rich enough to model different notions ofcomputation. Mathematical logic thus allows us to devise differentlogics for different models of computation. The logics relevant forthis proposal are known as modal logics.The upshot of this effort should be to make reasoning aboutcomputations completely precise and thus to eliminate the errorshumans tend to make when reasoning about programs.II.In my project I will look at particular models of computation whichare called transition systems. Transition systems consist of statesand relations between states. The idea is that each state representsa given moment of the computation and the relations describe how thecomputation proceeds from on state to another.The project aims at a general theory of logics for transitionsystems. It will establish the relationship between logics andtransition systems via the following detour that allows us to use acertain mathematical theory known as Stone duality. Recent developments suggest using co-algebras to represent transitionsystems. Coalgebras are in a special relationship---calledduality---to algebras. In a similar way as known from solvingequations in school, algebra can be used to formulate reasoningprinciples.In particular, the aims of this proposal are the following. Toassociate to any type of transition system an appropriate logic. Toshow how these logics can be applied to the verification of statementsabout programs. To investigate how certain concepts and tools ofmathematical logic can be adapted to coalgebras and their logics.III.The project will contribute to the theory of coalgebras as a generaltheory of transition systems as developed in the 1990s by manyresearchers. It will also be an important contribution to the recentworks on the connections between (modal) logic andcoalgebras. Coalgebras and modal logic have received attention fromresearchers in different areas of mathematics and computer science andthis research will bring to light new connections them.In a wider context, the project concerns the fundamental relationshipunderlying models of computation on the one hand and logic on theother hand. The development of the theory of coalgebras opens up thepossibility of integrating existing insights and to explore newdirections.