Proof Theory and Set Theories

卡尔森建议工作的一个深远的计划集中在证明理论的系统集理论，其中包括一个语义的方法证明理论一般和一个新的方法，建设序数符号系统的理论集。要研究的集合论最初上升到并包括Zermelo-Frankel集合论与权力集公理删除，但有一定的可能性，该方法将延伸得更远。符号系统揭示了相应集合论结构的基本部分。 所提出的研究是出于自然产生的问题，从哥德尔的不完备性定理。这些定理意味着，没有一个合理的数学系统足够强大，可以为所有具体的数学问题提供解决方案，例如，确定多项式方程的自然数解的存在性或验证计算机程序的正确性。总有一些问题的解决将取决于新公理的发现--新公理的接受将由直觉决定。已经出现的可能的新公理都属于“无穷公理”一类，它们断言存在越来越大的非具体数学对象。这类公理是唯一符合我们直觉的新公理，这似乎是可能的，甚至是可能的。本研究的最终目标是为以下问题提供令人信服的答案：1。无穷公理的概念能给出一个精确的定义吗？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.