On uniform weak König's lemma (Q5957854)

This article contrasts the logical strength of Weak König's Lemma (WKL) with a uniform version (UWKL) which asserts the existence of a functional which selects an infinite path for each binary tree. Working in fully extensional finite type extensions of primitive recursive arithmetic (PRA), the author shows that E-PRA\(^\omega\)+QF-AC\(^{1,0}\)+QF-AC\(^{0,1}\)+UWKL contains (and is conservative over) Peano arithmetic (PA). By contrast, applying the techniques of the author's related work [J. Symb. Log. 57, 1239-1273 (1992; Zbl 0781.03051)], it is shown that E-PRA\(^\omega\)+QF-AC\(^{1,0}\)+QF-AC\(^{0,1}\)+WKL is \(\Pi^0_2\)-conservative over PRA. Working over a stronger base system, the author shows that E-PA\(^\omega\)+QF-AC\(^{1,0}\)+QF-AC\(^{0,1}\)+UWKL has the same strength as (\(\Pi^0_1\)-CA)\(_{<\epsilon_0}\). Analyses in weakly extensional and intuitionistic contexts are also included.