×

zbMATH — the first resource for mathematics

Comparing the strength of diagonally nonrecursive functions in the absence of \(\Sigma_2^0\) induction. (English) Zbl 1373.03016
It is well-known that provably in the theory \(\mathrm{RCA}_0\), the statement “for every set \(X\) there is a \(2\)-bounded diagonally nonrecursive function relative to \(X\)” is equivalent to weak König’s lemma. Moreover, it is known that for any \(k \geq 2\), a DNR function that is \(k\)-bounded computes one that is \(2\)-bounded. Stephen Simpson had asked whether the latter result is also provable in \(\mathrm{RCA}_0\). The authors of the present paper show that the usual proof goes through in \(\mathsf{RCA}_0\) extended by the \(\Sigma^0_2\) induction axiom. On the other hand, in the absence of \(\Sigma^0_2\) induction, “all standard \(k\) are alike, but each nonstandard \(k\) is nonstandard in its own unique way”.
More precisely, the paper contains two main results. Firstly, the statement “there exists \(k\) such that for every \(X\) there is a \(k\)-bounded DNR function relative to \(X\)” does not imply \(\mathrm{WKL}\) over \(\mathrm{RCA}_0\), even in the presence of the \(\Sigma^0_2\) collection axiom. Secondly, the statement “for every \(X\) there is a bounded DNR function relative to \(X\)” is even weaker, and cannot be used to obtain a bound independent of \(X\) within \(\mathrm{RCA}_0\) + \(\Sigma^0_2\) collection.
To prove these theorems, the authors refine a known construction of an (unbounded) DNR function \(g\) that does not compute any \(2\)-bounded DNR function, in a technically nontrivial way. Taking advantage of the failure of \(\Sigma^0_2\) induction, they are able to implement the construction in a \(\Sigma^0_2\) -definable proper cut, thus making the DNR function \(g\) bounded. The main results are obtained by iterating this basic construction.
The paper also contains a section on connections between bounded DNR functions and graph colourings.

MSC:
03B30 Foundations of classical theories (including reverse mathematics)
03F35 Second- and higher-order arithmetic and fragments
03D30 Other degrees and reducibilities in computability and recursion theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1007/BF01621469 · Zbl 0718.03043 · doi:10.1007/BF01621469
[2] Logic, Methodology and Philosophy of Science VIII pp 191– (1989)
[3] Metamathematics of First-Order Arithmetic (1998) · Zbl 0889.03053
[4] On Turing reducibility (1994)
[5] DOI: 10.1002/malq.19980440405 · Zbl 0919.03045 · doi:10.1002/malq.19980440405
[6] Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, pp 235– (1975)
[7] DOI: 10.1090/S0894-0347-2014-00789-X · Zbl 1341.03015 · doi:10.1090/S0894-0347-2014-00789-X
[8] DOI: 10.1016/j.aim.2012.02.025 · Zbl 1255.03025 · doi:10.1016/j.aim.2012.02.025
[9] DOI: 10.1007/BF02802493 · Zbl 0976.03049 · doi:10.1007/BF02802493
[10] Transactions of the American Mathematical Society 334 pp 349– (1992)
[11] DOI: 10.1016/0168-0072(96)00028-0 · Zbl 0881.03023 · doi:10.1016/0168-0072(96)00028-0
[12] DOI: 10.1017/bsl.2014.14 · Zbl 1341.03098 · doi:10.1017/bsl.2014.14
[13] Pride and Prejudice (1813)
[14] Mathematical logic and applications pp 178– (1989)
[15] DOI: 10.1090/S0002-9939-04-07294-6 · Zbl 1053.03034 · doi:10.1090/S0002-9939-04-07294-6
[16] Subsystems of Second Order Arithmetic (2009) · Zbl 1181.03001
[17] Reverse mathematics 2001 pp 331– (2005)
[18] DOI: 10.1002/1521-3870(200010)46:4&lt;543::AID-MALQ543&gt;3.0.CO;2-E · Zbl 0963.03079 · doi:10.1002/1521-3870(200010)46:4<543::AID-MALQ543>3.0.CO;2-E
[19] Transactions of the American Mathematical Society 173 pp 33– (1972) · Zbl 0247.00014
[20] Recursively Enumerable Sets and Degrees (1987)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.