Mathematical Sciences: Topics in Logic and Set Theory

数学科学：逻辑和集合论主题

• 批准号: 9505118
• 负责人: Andreas Blass
• 金额: $ 11.49万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-07-01 至 1999-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9505118&HistoricalAwards=false
• 关键词: Mathematical; Sciences; Topics; Logic; Set

9505118 Blass The research project of Andreas Blass is in four areas: (1) Cardinal characteristics of the continuum, including both the general theory of such characteristics (involving Galois-Tukey connections) and the detailed study of particular characteristics, especially the recently introduced evasion and prediction numbers. (2) Applications of set theory, especially in the theory of abelian groups. (3) Semantics of linear logic, especially game semantics and its variants. (4) Logic of topoi, particularly the logical properties of geometric morphisms. The research project of Glen Whitney concerns interpreting general recursive definitions, especially in non-determinisitic and concurrent contexts. Specific questions include: (1) Finding a universal class of structures with a recursion operation, so that every structure will be contained in one from this class. (2) Comparing proposals for the semantics of concurrent programming languages. (3) Seeking connections with fixpoint logics used in finite model theory. (4) Extending the current theory to allow more detailed modelings of parameter and message passing between subprograms. Both the formal language of recursion FLR, which Whitney will study, and Girard's linear logic LL, one of Blass' research topics, can serve as mathematical models of certain aspects of computing. FLR models recursion, i.e., programs using subroutines identical to the programs themselves. Whitney's project is directed toward improved understanding of recursion in the context of parallel computing, i.e. computations done collaboratively by many machines operating simultaneously. LL models data types; its game semantics models the situation where accessing data involves more of an interaction (access protocol) between the provider and the user of the data than mere transmission of data. Both theories are currently at the stage of mathematical exploration, but it is hoped that the information obtained w ill be of use in the design of future programming languages and in the formal verification of correctness of programs. Cardinal characteristics of the continuum are a way to exhibit and clarify the combinatorial content of difficult problems from various areas of mathematics -- originally topology and analysis, more recently algebra as well. They provide connections between these different areas and thus allow progress on a problem in one area to be applied in another. In addition, they make these problems amenable to treatment by the methods of modern set theory. The final topic in Blass' proposed research, topos theory, also serves to connect apparently disparate areas, mostly within mathematical logic. The particular topic of geometric morphisms of topoi combines ideas from set theory, from information systems (introduced as a model of computation), from sheaf theory (a part of topology), and from constructive logic. ***

9505118 Blass安德烈亚斯·布拉斯的研究项目有四个方面：(1)连续体的基本特征，包括这种特征的一般理论(涉及伽罗瓦-图基联系)和对特定特征的详细研究，特别是最近引入的回避和预测数字。(2)集合论的应用，特别是在交换群论中的应用。(3)线性逻辑的语义学，特别是博弈语义学及其变体。(4)拓扑逻辑，特别是几何态射的逻辑性质。Glen Whitney的研究项目涉及解释一般的递归定义，特别是在不确定的和并发的上下文中。具体问题包括：(1)找到一个带有递归运算的通用结构类，使每个结构都包含在这个类中的一个结构类中。(2)对并发程序设计语言的语义方案进行比较。(3)寻求与有限模型理论中的不动点逻辑的联系。(4)扩展现有理论，允许对子程序之间的参数和消息传递进行更详细的建模。惠特尼将学习的递归FLR的形式语言和Blass研究的主题之一Girard的线性逻辑LL都可以作为计算某些方面的数学模型。FLR为递归建模，即使用与程序本身相同的子例程的程序。惠特尼的项目旨在改善对并行计算环境中递归的理解，即由多台机器同时运行的协作计算。LL对数据类型进行建模；它的游戏语义对访问数据涉及数据提供者和用户之间的交互(访问协议)而不仅仅是数据传输的情况进行了建模。这两种理论目前都处于数学探索阶段，但希望所获得的信息将用于未来程序设计语言的设计和程序正确性的形式化验证。连续体的基本特征是展示和阐明数学各个领域中困难问题的组合内容的一种方式--最初是拓扑学和分析，最近是代数。它们提供了这些不同领域之间的联系，从而允许在一个领域的问题上取得的进展应用于另一个领域。此外，它们使这些问题易于用现代集合论的方法来处理。布拉斯提出的研究的最后一个主题--拓朴理论，也用来连接明显不同的领域，主要是在数理逻辑范围内。Topoi的几何态射这一特殊主题结合了集合论、信息系统(作为计算模型引入)、束层理论(拓扑学的一部分)和构造性逻辑的思想。***