# On the Uniform Weak König’s Lemma

## DOI:

https://doi.org/10.7146/brics.v6i11.20068## Abstract

The so-called weak K¨onig's lemma WKL asserts the existence of an infinitepath 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.

## Downloads

## Published

1999-01-11

## How to Cite

*BRICS Report Series*,

*6*(11). https://doi.org/10.7146/brics.v6i11.20068

## Issue

## Section

Articles

## License

Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.