Program extraction for 2-random reals

Archive for Mathematical Logic 52 (5-6):659-666 (2013)
  Copy   BIBTEX

Abstract

Let ${2-\textsf{RAN}}$ be the statement that for each real X a real 2-random relative to X exists. We apply program extraction techniques we developed in Kreuzer and Kohlenbach (J. Symb. Log. 77(3):853–895, 2012. doi:10.2178/jsl/1344862165), Kreuzer (Notre Dame J. Formal Log. 53(2):245–265, 2012. doi:10.1215/00294527-1715716) to this principle. Let ${{\textsf{WKL}_0^\omega}}$ be the finite type extension of ${\textsf{WKL}_0}$ . We obtain that one can extract primitive recursive realizers from proofs in ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN}}$ , i.e., if ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN} \, {\vdash} \, \forall{f}\, {\exists}{x} A_{qf}(f,x)}$ then one can extract from the proof a primitive recursive term t(f) such that ${A_{qf}(f,t(f))}$ . As a consequence, we obtain that ${{\textsf{WKL}_0}+ \Pi^0_1 - {\textsf{CP}} + 2-\textsf{RAN}}$ is ${\Pi^0_3}$ -conservative over ${\textsf{RCA}_0}$

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 76,297

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Primitive Recursion and the Chain Antichain Principle.Alexander P. Kreuzer - 2012 - Notre Dame Journal of Formal Logic 53 (2):245-265.
Weak König's Lemma Implies Brouwer's Fan Theorem: A Direct Proof.Hajime Ishihara - 2006 - Notre Dame Journal of Formal Logic 47 (2):249-252.
Subclasses of the Weakly Random Reals.Johanna N. Y. Franklin - 2010 - Notre Dame Journal of Formal Logic 51 (4):417-426.
Light monotone Dialectica methods for proof mining.Mircea-Dan Hernest - 2009 - Mathematical Logic Quarterly 55 (5):551-561.
Reverse mathematics and a Ramsey-type König's Lemma.Stephen Flood - 2012 - Journal of Symbolic Logic 77 (4):1272-1280.
Elimination of Skolem functions for monotone formulas in analysis.Ulrich Kohlenbach - 1998 - Archive for Mathematical Logic 37 (5-6):363-390.
Measure theory and weak König's lemma.Xiaokang Yu & Stephen G. Simpson - 1990 - Archive for Mathematical Logic 30 (3):171-180.
On some formalized conservation results in arithmetic.P. Clote, P. Hájek & J. Paris - 1990 - Archive for Mathematical Logic 30 (4):201-218.

Analytics

Added to PP
2013-11-23

Downloads
19 (#589,316)

6 months
1 (#450,425)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Measure theory and weak König's lemma.Xiaokang Yu & Stephen G. Simpson - 1990 - Archive for Mathematical Logic 30 (3):171-180.
Primitive Recursion and the Chain Antichain Principle.Alexander P. Kreuzer - 2012 - Notre Dame Journal of Formal Logic 53 (2):245-265.
Elimination of Skolem functions for monotone formulas in analysis.Ulrich Kohlenbach - 1998 - Archive for Mathematical Logic 37 (5-6):363-390.

View all 6 references / Add more references