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

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 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<=1 for all z A0(x; y; z) -> there exists f <= lambda x.1 for all x, z A0(x, fx, z);
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 <= s'
instead of `there exists y <= 1', where g <= s is defined pointwise. The resulting schema is called Phi-b-AC^0,1.
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).