A note on uniform density in weak arithmetical theories (Q2219096)

\textit{V. Yu. Shavrukov} and \textit{A. Visser} [Notre Dame J. Formal Logic 55, No. 4, 569--582 (2014; Zbl 1339.03056)] asked whether the (pre-)lattice \(L_{\exists \Sigma^b_1/S^1_2}\) of \(\exists \Sigma^b_1\) sentences over Buss' theory \(S^1_2\) is uniformly dense. In other words, the question was whether there exists a computable procedure which, given \(\exists \Sigma^b_1\) sentences \(\varphi\), \(\psi\) such that \(\varphi\) implies \(\psi\) over \(S^1_2\) but not vice versa, outputs a third \(\exists \Sigma^b_1\) sentence which is strictly intermediate between \(\varphi\) and \(\psi\) in terms of implication over \(S^1_2\); the procedure is also required to respect equivalence over \(S^1_2\). The authors obtain a positive answer, which generalizes to any consistent c.e. extension of \(S^1_2\). In fact, they show that \(L_{\exists \Sigma^b_1/S^1_2}\) is effectively inseparable, in the sense that there is a computable procedure which, given indices \(x,y\) of disjoint c.e. sets \(W_x\), \(W_y\) such that \(W_x\) contains all the (Gödel numbers of) \(S^1_2\)-provable \(\exists \Sigma^b_1\) sentences and \(W_y\) contains all the \(S^1_2\)-disprovable ones, finds a number not contained in \(W_x \cup W_y\). It then follows from earlier work of \textit{U. Andrews} and the second author [``Effective inseparability, lattices, and pre-ordering relations'', Rev. Symb. Log. 14, No. 4, 838--865 (2021, \url{doi:10.1017/S1755020319000273}] that \(L_{\exists \Sigma^b_1/S^1_2}\) is uniformly dense and has an additional property called local universality. To prove effective inseparability, the authors use a witness comparison argument, taking advantage of the \(\exists \Sigma^b_1\)-completeness of \(S^1_2\) and the fact that the property of being a computation of a given Turing machine is \(\Delta^b_1\)-definable. In the second part of the paper, analogous results are proved for the lattice of all arithmetical sentences over \(iR\) and \(iQ\), the intuitionistic counterparts of Robinson's arithmetic theories \(R\) and \(Q\). A careful analysis reveals that effective inseparability and its consequences still hold if one restricts the lattice of all sentences to one of Burr's intuitionistic formula complexity classes \(\Phi_3\) or \(\Theta_2\). The arguments are similar in spirit to those for \(S^1_2\), but additionally invoke Matiyasevich's Theorem.