The computational strength of extensions of weak König's lemma
by
Ulrich Kohlenbach
BRICS, Department of Computer Science, University of Aarhus, Denmark

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 thereby allowing the extraction of constructive numerical data from given proofs in such fragments.
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 G_\infty where we allow an arbitrary function quantifier prefix over bounded functions in front of a \Pi⁰₁-formula. This results in a schema G_\infty-WKL.
In the absence of functional parameters (so in particular in a second-order context), the corresponding version of G_\infty-WKL turns out to be equivalent to WKL. This changes completely in the presence of functional variables of type 2 where we get proper a hierarchy of principles G_n-WKL. 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 indicate exhibiting the greater mathematical strength of G_\infty-WKL compared to WKL. We prove that, nevertheless, G_\infty-WKL does not contribute to the provably recursive functionals of the underlying fragments of arithmetic in all finite types.

Finally, we consider a uniform version UWKL of WKL which asserts the existence of a functional F which selects uniformly in a given infinite binary tree f an infinite path F(f) of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The computational strength of UWKL depends on the amount of extensionality available. In the presence of a quantifier-free rule of extensionality, UWKL has the same strength than WKL. However, in the presence of the full axiom of extensionality, UWKL is much stronger than WKL as we will show.

My homepage

Date received: February 25, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-06.