Recent Advances in Ordinal Analysis: Π1 2 — CA and Related Systems
Recent Advances in Ordinal Analysis: Π1 2 — CA and Related Systems
复制标题
序数分析的最新进展：Π1 2 — CA 和相关系统
DOI：
10.2307/421132
复制
发表时间：
1995
影响因子：
0.6
通讯作者：
M. Rathjen
中科院分区：
文献类型：
--
作者：
M. Rathjen
第1节。导论.本文的目的是，在一般情况下，报告的艺术状态的序数分析，特别是最近成功地获得了序数分析系统的分析，这是子系统的正式二阶算术，Z2，理解局限于公式。相同的技术可以用于为可还原为迭代理解的理论提供序数分析，例如，- 理解。详情将在[28]中列出。序理论的证明理论于1936年问世，从根岑的头脑中冒出来，在他的一致性证明算术的过程中。根岑希望有足够大的建设性序数，人们可以建立分析的一致性，即，Z2自从1945年8月4日根森不幸去世以来，证明理论已经取得了相当大的进展，但是对Z2的序数分析仍然是一个有待探索的问题。然而，由于无法在这里解释的原因，-理解似乎是理解完全理解的道路上的主要绊脚石，在可预见的将来对Z2进行序数分析带来了希望。粗略地说，序数信息证明理论将递归表示系统中的序数与给定形式系统中的证明联系起来;证明到某些标准形式的转换则部分地反映在相关序数上的操作上。除其他事项外，正式系统的序数分析服务于表征其可证明递归序数，函数和泛函，并可以产生守恒和组合独立的结果。
§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28]. Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2 is still something to be sought. However, for reasons that cannot be explained here, -comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2 in the foreseeable future. Roughly speaking, ordinally informative proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results.