Decidability in elementary analysis. I (Q1823233)

The authors consider sentences of the form (\(\forall f\in {\mathcal F})\phi\), where \({\mathcal F}\) is a family of functions from R into R or from \(I=[0,1]\) into I, and \(\phi\) is a sentence in the first order language with predicates \(<\), \(>\), \(=\), and with unary function symbol f. If \(\phi\) is \(\Sigma_ 1\) or \(\Pi_ 1\) and \({\mathcal F}\) is either the family of continuous, differentiable, infinitely differentiable, or real analytic functions, then the truth of (\(\forall f\in {\mathcal F})\phi\) is decidable (in fact by PSPACE procedures). These results are extended to a class of \(\phi\) 's called \(\Pi_ 2\) separated. The set of all first order \(\phi\) true in \((R,<,F)\), where F is continuous and strictly monotone, is shown to be decidable. Finally, it is shown that the set of true sentences (\(\forall f\in {\mathcal F})\phi\), where \(\phi\) is a \(\Sigma_ 4\) separated sentence and \({\mathcal F}\) is the set of continuous functions from R into R (or I into I) is undecidable.