论文标题
证明理论和逆向数学的井井原则
Well-Ordering Principles in Proof Theory and Reverse Mathematics
论文作者
论文摘要
关于熟悉的反向数学理论与某些良好井的等效理论的几种理论已通过递归理论和组合方法证明了（Friedman，Marcone，Montalban等），并通过证明的实验性结果通过证明的结果（Afshari，Freund，Greund，Gerund，Girard，Girard，rathjen，rathjen，therans vizia et ii viz can），培训。在后一种情况下，扣除搜索树和剪切的无限逻辑中的消除定理。在类型的第一级时，良好的顺序原理是形式（*）“如果x有序良好，则f（x）是井井有序的“ F（x），其中f是从序数到序数的标准证明理论函数（这样的f总是扩张器）。本文的一个目的是提出这些结果的基础方法，使人们能够从（*）中构建特定理论的欧米茄模型，甚至可以从（*）的类型2版本中构造beta模型。 由于（*）是复杂性pi-1-2这样的原理，因此无法表征PI-1-1概论水平上更强大的理解。这需要（*）的更高级版本，该版本采用了序数表示系统中的想法，具有崩溃的功能，在不可思议的证明理论中使用。最简单的是巴赫曼建筑。将后者的结构相对与任何扩张器F相对，并断言这总是产生良好的井井有条，这相当于Pi-1-1-1的理解。这一结果已被猜想，大约在10年前进行了证明策略，但近年来才进行了证明。
Several theorems about the equivalence of familiar theories of reverse mathematics with certain well-ordering principles have been proved by recursion-theoretic and combinatorial methods (Friedman, Marcone, Montalban et al.) and with far-reaching results by proof-theoretic technology (Afshari, Freund, Girard, Rathjen, Thomson, Valencia Vizcano, Weiermann et al.), employing deduction search trees and cut elimination theorems in infinitary logics with ordinal bounds in the latter case. At type level one, the well-ordering principles are of the form (*) "if X is well-ordered then f(X) is well-ordered" where f is a standard proof theoretic function from ordinals to ordinals (such f's are always dilators). One aim of the paper is to present a general methodology underlying these results that enables one to construct omega-models of particular theories from (*) and even beta-models from the type 2 version of (*). As (*) is of complexity Pi-1-2 such a principle cannot characterize stronger comprehensions at the level of Pi-1-1-comprehension. This requires a higher order version of (*) that employs ideas from ordinal representation systems with collapsing functions used in impredicative proof theory. The simplest one is the Bachmann construction. Relativizing the latter construction to any dilator f and asserting that this always yields a well-ordering turns out to be equivalent to Pi-1-1-comprehension. This result has been conjectured and a proof strategy adumbrated roughly 10 years ago, but the proof has only been worked out in recent years.
