Paper detail

Delta-Decidability over the Reals

Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence φcontaining only bounded quantifiers, and any positive rational number δ, decides either "φis true", or "a δ-strengthening of φis false". Under mild assumptions, for a C-computable signature F, the δ-decision problem for bounded Σ_k-sentences in L_F resides in (Σ_k^P)^C. The results stand in sharp contrast to the well-known undecidability results, and serve as a theoretical basis for the use of numerical methods in decision procedures for nonlinear first-order theories over the reals.