[FOM] Standard Language of Euclid

[joeshipman@aol.com]

I agree that my original surmise was wrong; what I should have asked is 
whether there is an interesting open question which can be stated in 
the language of elementary algebra and geometry without any increase in 
its complexity. It's clear that the question whether 41 disjoint open 
unit balls in R^5 can touch the standard unit ball (the first open 
"kissing number" problem) can be stated in the language of real algebra 
with 205 variables, but I don't want to count a question with that kind 
of blowup.

A related question: is it known whether the pure first-order theory of 
fields is undecidable? (By Tarski, if you add infinitely axioms to 
ensure characteristic 0 and infinitely many axioms to ensure 
real-closedness, the resulting theory is complete and decidable,but I 
am interested in the statements that must be true in all fields.)

-- JS

-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>

Andrej Bauer <andrej.bauer at andrej.com> wrote:
> On Sun, Sep 27, 2009 at 9:16 PM,  <joeshipman at aol.com> wrote:
> > Of course we know that some decidable theories still have open
> > questions (for example, nobody knows whether there exists a 
projective
> > plane of order 12). Am I correct in surmising that there is no 
question
> > that can be stated in the language of elementary algebra and 
geometry
> > which is currently regarded as both open and interesting?
>
> Alas, you are not correct.

One could have conjectured this on general principles.  The existence
of a decision algorithm for a theory is rarely the end of the story.
Computational tractability is still an issue.  And once your computers
and algorithms get fast enough to decide all interesting questions with,
say, 3 quantifiers, people immediately start thinking about 4 
quantifiers.