Abstract

Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any sentence A containing only bounded quantifiers and functions in F, and any positive rational number delta, decides either “A is true”, or “a delta-strengthening of A is false”. Moreover, if F can be computed in complexity class C, then under mild assumptions, this “delta-decision problem” for bounded Sigma k-sentences resides in Sigma k. The results stand in sharp contrast to the well-known undecidability of the general first-order theories with these functions, and serve as a theoretical basis for the use of numerical methods in decision procedures for formulas over the reals