[FOM] Standard Language of Euclid

[Andrej Bauer]

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. Some of my colleagues here at the math
department study geometric interpolation problems which often boil
down to open statements that are in principle solvable with Tarski's
decision procedure (or Collin's cyllindric algebraic decomposition).
These problems are considered mathematically interesting and
potentially have real uses in Computer Aided Geometric Design, see
e.g.:

G. Jaklič, J. Kozak, M. Krajnc, V. Vitrih, E. Žagar: Geometric
Lagrange Interpolation by Planar Cubic Pythagorean-hodograph Curves,
Comput. Aided Geom. Design 25 (9), 2008, 720-728. Available at
http://www.fmf.uni-lj.si/~krajncm/clanki/PH-cubic.pdf

Marjeta Kranjc, one of the coauthors, specifically mentioned the
following problem to me (I may have gotten the exact formulation
wrong, but you'll get the feeling for what kind of problems
expressible in the language of a real-closed field are open and
considered interesting):

Suppose T_0, T_1, T_2, T_3 are points in the plane such that they form
a non-degenerate convex quadrilateral and the cosine of the angle
between T_0T_1 and T_2T_3 is less than -1/2 (this can be expressed by
a polynomial inequality). Then there exists a _unique_ parametric
polynomial curve P(t) = (p(t), q(t)) of degree 3, a polynomial
sigma(t) of degree 2, and parameters 0 = t_0 < t_1 < t_2 < t_3 = 1,
such that P(t_i) = T_i for i = 0, 1, 2, 3, 4 and ||dP/dt|| = sigma.

The last bit ||dP/dt|| = sigma says that the norm of the derivative of
P is a polynomial, i.e., for all t, p'(t)^2 + q'(t)^2 = sigma(t)^2,
where p' amd q' are the derivatives of p and q. They are able to prove
the existence of the interpolating curve P(t) but not uniqueness.

It was interesting to talk to Marjeta about this from the "logician
meets normal mathematican" point of view. While I was asking for the
simplest possible specific open problem that is considered
interesting, she kept offering open problems that ask for _conditions_
on the points which guarantee existence of the interpolating curve. In
other words, it was implicitly assumed that, given a statement of the
form

"for all points T_0, ..., T_k in the plane there exists an
interpolating curve satisfying some condition"

the problem is not to decide whether it is true, but rather to analyze
what conditions the points must satisfy so that the statement becomes
true. When I pointed out that the "best" condition the points could
satsify is that they be interpolated by a curve, I got a feeling that
she started doubting my (mathematical) sanity :-)

With kind regards,

Andrej