Comparing the strength of diagonally nonrecursive functions in the absence of \(\Sigma_2^0\) induction (Q2795915)

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''.NEWLINENEWLINEMore 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.NEWLINENEWLINETo 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.NEWLINENEWLINEThe paper also contains a section on connections between bounded DNR functions and graph colourings.