It is a well-known result that the first-order theory of the real numbers is decidable. However the decision algorithm for this language is in double exponential time, so such an algorithm cannot be practically applied. It then seems perfectly consistent that there is some open problem expressible in the first-order theory of the reals, which the decision algorithm could solve if given enough time.

Does anyone know of any such problem?

If not, as a softer question, does anyone know of a simple statement in the first-order theory of the real numbers that is difficult to prove?

  • 5
    $\begingroup$ This list of open problems in Euclidean geometry may be relevant: mathoverflow.net/questions/53797/… $\endgroup$ Oct 4 '20 at 2:20
  • 2
    $\begingroup$ Most (maybe even all?) of those problems are not first-order, though. $\endgroup$ Oct 4 '20 at 3:47
  • 1
    $\begingroup$ Yeah, none of these seem obviously (or even likely) FO to me, there are of course open questions in higher order theories of reals (I'm pretty sure the naturals are second order definable over the reals so that'd include all the open problems expressible in PA for example) $\endgroup$ Oct 4 '20 at 3:57

By some wonderful coincidence this was just covered unprompted in a lecture I attented, where it was mentioned the kissing number problem in, say, 5 dimensions is an open problem equivalent to a first order sentence in the language of the reals and hence decidable by an algorithm given enough time.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.