文章基本信息

标题：The Computational Strength of Extensions of Weak König’s Lemma
本地全文：下载
作者：Ulrich Kohlenbach
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1998
卷号：5
期号：41
出版社：Aarhus University
摘要：The weak König's lemma WKL is of crucial significance in the study of fragments of mathematics which on the one hand are mathematically strong but on the other hand have a low proof-theoretic and computational strength. In addition to the restriction to binary trees (or equivalently bounded trees), WKL is also `weak' in that the tree predicate is quantifier-free. Whereas in general the computational and proof-theoretic strength increases when logically more complex trees are allowed, we show that this is not the case for trees which are given by formulas in a class Phi where we allow an arbitrary function quantifier prefix over bounded functions in front of a Pi^0_1-formula. This results in a schema Phi-WKL. Another way of looking at WKL is via its equivalence to the principle For all x there exists y there exists f where A0 is a quantifier-free formula (x, y, z are natural number variables). We generalize this to Phi-formulas as well and allow function quantifiers `there exists g instead of `there exists y In the absence of functional parameters (so in particular in a second order context), the corresponding versions of Phi-WKL and Phi-b-AC^0,1 turn out to be equivalent to WKL. This changes completely in the presence of functional variables of type 2 where we get proper hierarchies of principles Phi_n-WKL and Phi_n-b-AC^0,1. Variables of type 2 however are necessary for a direct representation of analytical objects and - sometimes - for a faithful representation of such objects at all as we will show in a subsequent paper. By a reduction of Phi-WKL and Phi-b-AC^0,1 to a non-standard axiom F (introduced in a previous paper) and a new elimination result for F relative to various fragment of arithmetic in all finite types, we prove that Phi-WKL and Phi-b-AC^0,1 do neither contribute to the provably recursive functionals of these fragments nor to their proof-theoretic strength. In a subsequent paper we will illustrate the greater mathematical strength of these principles (compared to WKL).