[FOM] Standard Language of Euclid

[Schaefer, Marcus]

> -----Original Message-----
> From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf 
> Of Ricky Pollack
> Sent: Saturday, October 03, 2009 8:01 PM
> 
> Look at many of the papers of Paul Erdos and many articles in 
> "Discrete & Computational Geometry" and you will find numerous 
> interesting problems (both solved and open) stated in the elementary 
> language of geometry.
> 
> Ricky

Here's a particular example: does every 2-coloring of the Euclidean plane contain three collinear points with unit distance between the midpoint and the endpoints so that all three points have the same color? If the answer is yes, then by compactness (using AC) there is a finite subset of points in the plane that witnesses this property and it is easy to write a sentence in the theory of the reals which expresses that there is such a witness set of n points. If one approaches this problem using solvers, there are two obstacles: there is no combinatorial upper bound on n (assuming it exists) and even for small n the formulas are large. (Soifer's Mathematical Coloring Book contains many examples in Euclidean Ramsey theory that have this flavor.)

I've tried to argue recently that the existential theory of the reals deserves its own complexity class ER: http://ovid.cs.depaul.edu/documents/convex.pdf . ER lies between NP and PSPACE and those are the best known bounds in terms of complexity. Does it contain coNP? If not, where does it lie? Does it equal NP? As far as I know, the complexity of the full theory of the reals has also never been pinned down precisely (though it is known to lie in EXPSPACE as shown by Ben-Or, Kozen and Reif).

Marcus