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<br />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<br />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.<br />Another way of looking at WKL is via its equivalence to the principle<br /> For all x there exists y<=1 for all z A0(x; y; z) -> there exists f <= lambda x.1 for all x, z A0(x, fx, z);<br />where A0 is a quantifier-free formula (x, y, z are natural number variables). <br /> We generalize this to Phi-formulas as well and allow function quantifiers `there exists g <= s'<br />instead of `there exists y <= 1', where g <= s is defined pointwise. The resulting schema is called Phi-b-AC^0,1.<br />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<br />be equivalent to WKL. This changes completely in the presence of functional<br />variables of type 2 where we get proper hierarchies of principles Phi_n-WKL and<br />Phi_n-b-AC^0,1. Variables of type 2 however are necessary for a direct representation<br />of analytical objects and - sometimes - for a faithful representation of<br />such objects at all as we will show in a subsequent paper. By a reduction of<br />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<br />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).
A criterion for differentiability
