Program extraction for 2-random reals (Q365682)

The main theorem of this paper states that \(\text{WKL}^\omega_0 + \Pi^0_1\text{-CP} + \text{CAC}+ 2\text{-RAN}\) is conservative over \(\text{RCA}_0^\omega\) for sentences of the form \(\forall f \exists x A_{qf}(f,x)\), and that from any proof of such a sentence one can extract a primitive recursive realizer \(t[f]\) for \(x\). Here \(\text{WKL}^\omega_0\) denotes the extension of the usual \(\text{WKL}_0\) subsystem of reverse mathematics to all finite types. \( \Pi^0_1\text{-CP}\) denotes the \(\Pi^0_1\) collection scheme, sometimes called \(\text{B}\Pi^0_1\) by other authors. \(\text{CAC}\) is the chain anti-chain principle and \(2\text{-RAN}\) asserts the existence of a \(2\)-random real relative to any given set. The subscript \(qf\) indicates that \(A_{qf}\) is quantifier free. An immediate corollary in second-order arithmetic is that \(\text{WKL}_0 + \Pi^0_1\text{-CP}+\text{CAC}+2\text{-RAN}\) is conservative over \(\text{RCA}_0\) for sentences of the form \(\forall X A(X)\) where \(A\) is \(\Pi^0_3\). The proof of the main theorem is based on the proof extraction techniques developed in work of \textit{U. Kohlenbach} and \textit{A. P. Kreuzer} [J. Symb. Log. 77, No. 3, 853--895 (2012; Zbl 1254.03112)] and \textit{A. P. Kreuzer} [Notre Dame J. Formal Logic 53, No. 2, 245--265 (2012; Zbl 1253.03090)]. A different proof technique was used by \textit{C. J. Conidis} and \textit{T. A. Slaman} [J. Symb. Log. 78, No. 1, 195--206 (2013; Zbl 1305.03055)] to prove that \(2\text{-RAN}\) is \(\Pi^1_1\)-conservative over \(\text{RCA}_0 + \Pi^0_1\text{-CP}\). For alternative principles equivalent to \(2\text{-RAN}\), see the work of \textit{J. Avigad} et al. [Ann. Pure Appl. Logic 163, No. 12, 1854--1864 (2012; Zbl 1259.03021)].