NATURAL LIMITATIONS OF DECISION PROCEDURES FOR ARITHMETIC WITH BOUNDED QUANTIFIERS

We study the complexity of the decision problem of a variant of arithmetic with bounded quantifiers. By contrast with the usual asymptotic complexity results, where one only deals with suitably long sentences, our limitative results have a concrete character, so as to find application in physics. We develop the mathematical framework for our lower bounds up to the point where their physical meaning is evident. Imagining that Turing machine M materializes as a real computer M′, we give a rigorous formulation of the simplest space-time features of M′, by essentially requiring that (i) each state of M occupies some space, (ii) no signal between states and scanning head can travel at infinite speed. When M provides a decision procedure for arithmetic with bounded quantifiers, there exist stringent lower bounds for the "time"t(j) needed by M′ to solve the hardest problems of length smaller than j, no matter the number of states of M. We discuss several applications of our results.