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 prooftheoretic 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
quantifierfree. Whereas in general the computational and prooftheoretic
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
quantifierfree 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 bAC. In
the absence of functional parameters (so in particular in a second order
context), the corresponding versions of WKL and
bAC 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 bAC.
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 bAC to a nonstandard 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 bAC do neither contribute to
the provably recursive functionals of these fragments nor to their
prooftheoretic strength. In a subsequent paper we will illustrate the
greater mathematical strength of these principles (compared to
WKL)
Available as PostScript,
PDF,
DVI.
