The so-called weak Konig'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 20-conservative over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In Kohlenbach [10] (J. Symbolic Logic 57 (1992) 1239-1273) we established such conservation results relative to finite type extensions PRA of PRA (together with a quantifier-free axiom of choice schema which-relative to PRA -implies the schema of 10-induction). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional which selects uniformly in a given infinite binary tree f an infinite path 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 Kohlenbach [10] actually can be used to eliminate even this uniform weak Konig's lemma provided that PRA 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 20-conservative over PRA, PRA +(E)+UWKL contains (and is conservative over) full Peano arithmetic PA. We also investigate the proof-theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA both with and without the Markov principle.

Type:

Journal article

Language:

English

Published in:

Annals of Pure and Applied Logic, 2002, Vol 114, Issue 1, p. 103-116

Keywords:

Konig's lemma; Higher order arithmetic; Functionals of finite type; Fan rule; Explicit mathematics