On the Uniform Weak König’s Lemma

Abstract

The 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 [10] 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 [10] 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.