The so-called weak König's lemma WKL asserts the existence
of an infinite path
![$b$](Abs/img1.gif)
in any infinite binary tree (given by a representing
function
![$f$](Abs/img2.gif)
). 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$](Abs/img3.gif)
-conservative over primitive recursive
arithmetic PRA (and even weaker fragments of arithmetic). In 1992 we
established such conservation results relative to finite type extensions
PRA
![$^{\omega}$](Abs/img4.gif)
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$](Abs/img5.gif)
which selects uniformly in
a given infinite binary tree
![$f$](Abs/img2.gif)
an infinite path
![$\Phi f$](Abs/img6.gif)
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 from 1992 actually can
be used to eliminate even this uniform weak König's lemma provided that
PRA
![$^{\omega}$](Abs/img4.gif)
only has a quantifier-free rule of extensionality QF-ER
instead of the full axioms
![$(E)$](Abs/img7.gif)
of extensionality for all finite types. In
this paper we show that in the presence of
![$(E)$](Abs/img7.gif)
, UWKL is much stronger than
WKL: whereas WKL remains to be
![$\Pi^0_2$](Abs/img3.gif)
-conservative over PRA,
PRA
![$^{\omega}+(E)+$](Abs/img8.gif)
UWKL contains (and is conservative over) full Peano
arithmetic PA