[FOM] Standard Language of Euclid

[Grant Olney Passmore]

Dear Andrej and Joe --

Thank you for this interesting thread.  I serendipitously write now a few
hours after the ending of SYNASC-2009 in Timisoara, Romania, which has
involved much spirited conversation on RCF matters.

Andrej: The problem you mention is fascinating; I will email you
separately to learn more.

Joe: Thank you for that interesting reference.  W.r.t. your question, here
are two follow-up examples:

(i) The family of kissing problems for n-dimensional hyperspheres contains
a sequence of interesting open problems each expressible as Tarski
formulas.  In particular, the statement F(m,n) stating ``there exist m
n-dimensional unit hyperspheres, each kissing a unit hypersphere centered
at the origin, and none overlapping'' is easily expressed as a (very
large) formula in the purely existential fragment of the theory of real
closed fields.

To obtain k(n), the kissing number for R^n, one could in principle iterate
the operation of testing the validity of F(m,n) from below until the first
m is reached s.t. F(m,n) is false.  Then, k(n) = m-1.  While qe over RCF
is asymptotically doubly exponential in dimension (number of variables),
due to Renegar and others, it is known that the existential fragment of
RCF can be decided in time singly exponential in dimension (it is in fact
PSPACE-complete).  This marvelous fact hasn't yet* had any practical
bearing on decision methods as analysis by Hong in the early 90s at RISC
Linz suggested that while the known singly exponential procedures offer a
theoretical exponential speed-up over full RCF qe methods (e.g., CAD), the
constant factors involved (and ignored in the asymptotic analyses) make
the procedures intractible for even extremely small existential formulae. 
Moreover, reconnecting to the kissing problem, the naive encoding of even
the statement F(13,3) (whose falsity would show that k(3)<=12 as was the
subject of a great debate between Newton and Gregory), requires so many
variables as to make any general decision method look completely hopeless
in the fact of such problems.

* I say ``hasn't yet'' as Galen Huntington in his beautiful 2008 PhD
dissertation under Branden Fitelson at Berkeley showed that Canny's singly
exponential procedure could in fact be implemented and made to solve a
number of small existential problems for which Hong's analysis suggested
other singly exponential procedures (Renegar, Grigor'ev-Vorobjnov) would
fail (where ``fail'' means ``not terminate for millions of years'').


(ii) While no longer open (though its special status through Hales's
Flyspeck Project as the source of perhaps the largest formal verification
effort in the history of formalised mathematics is leading to much
advances in proof checking technology, including RCF decision techniques
for special classes of formulae), the Kepler conjecture can itself be
expressed as an optimization problem in a finite number of variables, as
shown by L. Fejes Toth.  This can be expressed as a Tarski formula.  In
addition, Hales has organized a selection of some 200 elementary geometry
theorems (all Tarski formulas) whose truths are relied upon in the course
of his proof.  These all need to be formalized in the process of verifying
his proof, and many are in so many variables as to be beyond the reach of
available decision methods.  Many people are taking different approaches
to working on these (let me know if you want more details), and Hales has
even written a paper on geometric techniques he thinks might lead to new
algorithms for routinely proving the types of problems in the collection. 
All of this is pushing the field of RCF decision methods forward at an
inspiring pace.

Also, returning to the subject of (almost) open problems, I remember
Warren Hunt once telling me when I was an undergraduate that during the
time of his Ph.D. in the 1980s he shared an office with Chou (who was Wu's
student before being Boyer's), and Chou's decision method based on Wu's
elimination methods was regularly able to prove theorems that Chou would
find by reading abstracts and announcements in geometry journals (without
seeing their proof).

I imagine that Chou, Dongming Wang, and Tetsuo Ida would have much more to
say on the topic as well.

OK, I will stop here.  I look forward to more discussion.

Grant
--
Grant Olney Passmore
LFCS, University of Edinburgh


On Tue, September 29, 2009 08:26, Andrej Bauer 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. 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
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>


-- 
Simplify, simplify, simplify. -- Henry David Thoreau
Simplify.                     -- Wendy McElroy