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

Ulrich Kohlenbach

December 1998

Abstract:

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
displaymath36
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.