[FOM] Standard Language of Euclid

[Timothy Y. Chow]

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.

Note also that the problem of finding *readable* proofs for theorems in 
geometry is still alive and well.  See for example

  http://dpt-info.u-strasbg.fr/~narboux/area_method.html

The area method is powerful but still has its limits.  For example, I 
believe that the notorious Steiner-Lehmus theorem doesn't succumb to
the area method directly; a small amount of human guidance is still
needed.

Tim