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

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), WKLis 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 aregiven 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