The Computational Strength of Extensions of Weak König's Lemma

Ulrich Kohlenbach

December 1998


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 tex2html_wrap_inline38 where we allow an arbitrary function quantifier prefix over bounded functions in front of a tex2html_wrap_inline40-formula. This results in a schema tex2html_wrap_inline38-WKL.
Another way of looking at WKL is via its equivalence to the principle
where tex2html_wrap_inline44 is a quantifier-free formula (x,y,z are natural number variables). We generalize this to tex2html_wrap_inline38-formulas as well and allow function quantifiers `tex2html_wrap_inline50' instead of `tex2html_wrap_inline52', where tex2html_wrap_inline54 is defined pointwise. The resulting schema is called tex2html_wrap_inline38-b-ACtex2html_wrap_inline58.
In the absence of functional parameters (so in particular in a second order context), the corresponding versions of tex2html_wrap_inline38-WKL and tex2html_wrap_inline38-b-ACtex2html_wrap_inline58 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 tex2html_wrap_inline68-WKL and tex2html_wrap_inline68-b-ACtex2html_wrap_inline58. 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 tex2html_wrap_inline38-WKL and tex2html_wrap_inline38-b-ACtex2html_wrap_inline58 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 tex2html_wrap_inline38-WKL and tex2html_wrap_inline38-b-ACtex2html_wrap_inline58 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)

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.