On uniform weak König's lemma

✍ Scribed by Ulrich Kohlenbach

• Publisher: Elsevier Science
• Year: 2002
• Tongue: English
• Weight: 121 KB
• Volume: 114
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(01)00077-x

✦ Synopsis

The so-called weak K onig's lemma WKL asserts the existence of an inÿnite path b in any inÿnite 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 0 2 -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 ÿnite type extensions PRA ! of PRA (together with a quantiÿer-free axiom of choice schema which-relative to PRA ! -implies the schema of 0 1 -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 inÿnite binary tree f an inÿnite 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 K onig's lemma provided that PRA ! only has a quantiÿer-free rule of extensionality QF-ER instead of the full axioms (E) of extensionality for all ÿnite types. In this paper we show that in the presence of (E), UWKL is much stronger than WKL: whereas WKL remains to be 0 2 -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.