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