Constructive aspects of classical mathematics

研究者正在进行两条研究路线，与从经典数学理论中提取建设性、计算性和组合性信息的一般证明理论程序相关。第一部分涉及将语义方法扩展到有序分析的kripke - platek集合理论，并从分析中提取可构造层次结构的组合和计算原理。第二种方法是试图为非标准算术的弱理论找到尖锐的守恒结果，最好是通过在标准理论中对非标准理论的“自然”解释，并探索在这些框架中进行普通数学的方法。自20世纪初以来，两种不同的数学思维方式逐渐出现分歧。一方面，数学被视为对抽象概念的一般研究，其中许多涉及无限的对象和结构。另一方面，许多人认为数学是以具体的符号表示和计算为基础的。证明论的一个目标是通过寻找隐藏在抽象数学推理的一般形式中的具体的计算内容来调和这两种观点。研究者旨在将证明理论方法应用于非标准分析理论和片段抵消理论的研究。

The investigator is pursuing two lines of research, relevant to thegeneral proof-theoretic program of extracting constructive, computational,and combinatorial information from theories of classical mathematics. Thefirst involves extending a semantic approach to ordinal analysis toKripke-Platek set theory, and extracting combinatorial and computationalprinciples for the constructible hierarchy from the analysis. The secondinvolves trying to find sharp conservation results for weak theories ofnonstandard arithmetic, preferably via "natural" interpretations of thenonstandard theories in the standard ones, and exploring ways in whichordinary mathematics can be carried out in these frameworks.Since the beginning of the 20th century, there has been a gradualdivergence between two different ways of thinking about mathematics. Onthe one hand, mathematics is viewed as a general investigation intoabstract concepts, many of them involving infinitary objects andstructures. On the other hand, many see mathematics as grounded byconcrete symbolic representations and calculation. One goal of prooftheory is to reconcile these two viewpoints, by finding the concrete,computational content that is hidden in general forms of abstractmathematical reasoning. The investigator aims to apply proof-theoreticmethods to the study of theories of nonstandard analysis, and fragments ofset theory.