Proof Theory and Set Theories

卡尔森提出了一个以集合论系统的证明理论为中心的影响深远的计划，其中包括一般证明理论的语义方法和构造集合论的有序符号系统的新方法。最初要研究的集合理论包括去掉幂集公理的Zermelo-Frankel集合理论，但这些方法有可能扩展得更远。符号系统揭示了相应集合论结构的基本部分。提出的研究是由哥德尔不完备定理自然产生的问题所驱动的。这些定理意味着，没有一个合理的数学系统强大到足以为所有具体的数学问题提供解决方案，例如，确定多项式方程的自然数解的存在性或验证计算机程序的正确性。总会有一些问题，它们的解决取决于新公理的发现——新公理的接受与否取决于直觉。已经出现的可能的新公理都属于“无限公理”一类，它断言存在着越来越大的非具体的数学对象。这类公理是我们的直觉所能接受的唯一新公理，这似乎是可能的，甚至是可能的。拟议研究的最终目标是为以下问题提供令人信服的答案：无限公理的概念能否给一个精确的定义？2. 所有有意义的具体数学问题都可以用无穷公理来解决吗？3. 哪些无穷公理对于解决有意义的具体数学问题是必要的？虽然这些问题的答案似乎不太可能在不久的将来得到解答，尤其是前两个问题，但这里提出的计划的成功完成将是向前迈出的重要一步。

Carlson proposes to work on a far reaching program centering on the proof theory of systems of set theory which includes a semantic approach to proof theory in general and a new method for constructing ordinal notation systems for theories of sets. The set theories to be studied initially go up to and include Zermelo-Frankel set theory with the power set axiom removed but there is some likelihood that the methods will extend much farther. The notation systems lay bare a fundamental part of the structures for the corresponding set theories. The proposed research is motivated by questions which arise naturally from Godel's incompleteness theorems. These theorems imply that no reasonable mathematical system is strong enough to provide solutions to all concrete mathematical problems, e.g., determining the existence of solutions in the natural numbers to polynomial equations or verifying the correctness of computer programs. There will always be questions whose solution will hinge on the discovery of new axioms- new axioms whose acceptance will be determined by intuition. The possible new axioms which have emerged all fall into the class of "axioms of infinity" which assert the existence of larger and larger nonconcrete mathematical objects. That axioms of this sort are the only new axioms amenable to our intuition seems possible, even probable. The ultimate goal of the proposed research would be to provide convincing answers to the following questions: 1. Can the notion of axiom of infinity be given a precise definition? 2. Can all meaningful concrete mathematical problems be resolved by axioms of infinity? 3. Which axioms of infinity are necessary for the solution of meaningful concrete mathematical questions? While answers to these questions seem unlikely in the near future, especially for the first two, the successful completion of the program proposed here would be a significant step forward.