On the Uniform Weak König’s Lemma
AbstractThe so-called weak K¨onig's lemma WKL asserts the existence of an infinite
path b in any infinite binary tree (given by a representing function f). Based on
this principle one can formulate subsystems of higher-order arithmetic which
allow to carry out very substantial parts of classical mathematics but are PI^0_2-conservative
over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In  we established such conservation results relative to finite type extensions PRA^omega of PRA (together with a quantifier-free axiom of choice schema). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional Phi which selects uniformly in a given infinite binary tree f an infinite path Phi f of that tree.
This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in  actually can be used to eliminate even this uniform weak K¨onig's lemma provided that PRA^omega only has a quantifier-free rule of extensionality QF-ER instead of the full axioms (E) of extensionality for all finite types. In this paper we show that in the presence of (E), UWKL is much stronger than WKL: whereas WKL remains to be Pi^0_2 -conservative over PRA, PRA^omega +(E)+UWKL contains (and is conservative over) full Peano arithmetic PA.
How to Cite
Kohlenbach, U. (1999). On the Uniform Weak König’s Lemma. BRICS Report Series, 6(11). https://doi.org/10.7146/brics.v6i11.20068
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.