Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
复制标题
数学上强大的分析子系统，可证明递归泛函的增长率较低
DOI：
--
复制
发表时间：
1996
影响因子：
0.3
通讯作者：
U. Kohlenbach
中科院分区：
文献类型：
--
作者：
U. Kohlenbach
这篇论文是作者Habilitationsschrift[22]发表的一系列论文中的第一篇，这些论文致力于确定分析的标准部分的证明的增长。引入了所有有限类型算术系统的一个层次(GNA)n∈IN，它的类型1=0(0)的可定义对象对应于本原递归函数的Grzegorczyk层次。我们通过无量词选择AC-QF和形式为∀x∃y≤ρSx∀z F0(也包括一个在完全集合论模型中不成立但在强可优化泛函中不成立的‘非标准’公理F)的解析公理Γ为GNA∃的扩展建立以下提取规则：从证明GNA+AC-QF+Γ⊢∀u，k∀v≤τ突克∃w A0(u，k，v，w)可以提取一个一致的界Φ，使得∀u，k∀v≤τ突克∃w≤ΦukA0(u，k，v，w)W)保持全集合论类型结构。如果n=2(分别为N=3)ΦUK是多项式(分别为一个初等递归函数)in k，u：=λx.max(u0，.。。，UX)。在本文中，我们证明了对于n≥2，GNA+AC-QF+F证明了二元Konig引理的推广，从而得到了新的守恒结果，因为上述规则的结论在这种情况下可以在Gmax(3，n)Aω中得到验证。在接下来的文章中，我们将证明许多重要的无效分析原理和定理已经在G2a+AC-QF+Γ中被证明，以获得合适的Γ。
This paper is the first one in a sequel of papers resulting from the authors Habilitationsschrift [22] which are devoted to determine the growth in proofs of standard parts of analysis. A hierarchy (GnA )n∈IN of systems of arithmetic in all finite types is introduced whose definable objects of type 1 = 0(0) correspond to the Grzegorczyk hierarchy of primitive recursive functions. We establish the following extraction rule for an extension of GnA ω by quantifier–free choice AC–qf and analytical axioms Γ having the form ∀x∃y ≤ρ sx∀z F0 (including also a ‘non– standard’ axiom F which does not hold in the full set–theoretic model but in the strongly majorizable functionals): From a proof GnA +AC–qf + Γ ⊢ ∀u, k∀v ≤τ tuk∃w A0(u, k, v, w) one can extract a uniform bound Φ such that ∀u, k∀v ≤τ tuk∃w ≤ ΦukA0(u, k, v, w) holds in the full set–theoretic type structure. In case n = 2 (resp. n = 3) Φuk is a polynomial (resp. an elementary recursive function) in k, u := λx.max(u0, . . . , ux). In the present paper we show that for n ≥ 2, GnA +AC–qf+F proves a generalization of the binary Konig’s lemma yielding new conservation results since the conclusion of the above rule can be verified in Gmax(3,n)A ω in this case. In a subsequent paper we will show that many important ineffective analytical principles and theorems can be proved already in G2A +AC–qf+Γ for suitable Γ.