A sharp version of the bounded Matijasevich conjecture and the end-extension problem (Q4032645)

The bounded Matijasevich conjecture (BMC) asserts that the \(\Delta_ 0\) hierarchy collapses provably in \(I\Delta_ 0\), i.e. for every \(\Delta_ 0\) formula \(\theta\) there is a \(\exists_ 1\) formula \(\theta'\) equivalent to \(\theta\) in every model of \(I\Delta_ 0\). The author considers a version of the conjecture (SBMC), where the translation function \(f(\theta)= \theta'\) is recursive and the bound on the quantifiers of \(\theta'\), given by \(f\), is fixed for all \(\theta\). The author shows that SBMC is a consequence of \(I\Delta_ 0+\exp\), and further motivates the conjecture by arguments provided by the proof of the Matijasevich theorem in \(I\Delta_ 0+\exp+B\Sigma_ 1\) due to Dimitracopoulos and Gaifman. Wilkie and Paris used BMC to characterize models of \(I\Delta_ 0+ B\Sigma_ 1\) that have end extensions to models of \(I\Delta_ 0\), under an additional structural assumption on the model. The author uses SBMC to give a similar characterization without this special assumption. The main part of the proof is a construction, in \(I\Delta_ 0+\text{SBMC}\), of a \(\Sigma_ 1\) universal satisfaction formula for \(\Sigma_ 1\) formulas.