Can the decision routine for Tarski's Elementary geometry be extended to decide when an existence claim in that theory can be instantiated by a compass and straightedge construction?

The answer does not follow from mere existence of Tarski's decision routine since the natural definition of constructible quantifies over "any finite number" of steps. But can the routine in fact be refined to decide constructibility?

I got this question from thinking about Mazur's comments on geometry versus arithmetic for Euclid in http://www.math.harvard.edu/~mazur/preprints/meaning_error.pdf, and I see the question occurs in discussion of Is compass and straight edge geometry complete? mixed with many more or less precise variants and calls for more precision. It is not answered there.

In case it helps I specify that I mean Tarski's first order theory of elementary geometry, not supplemented by a predicate for integer lengths or any other predicates. Since each construction is expressible in the first order theory, a construction that works in one model works in all. But is there a decision routine to tell if such a construction exists?

  • 2
    $\begingroup$ I think that Tarski has been dead long enough so we can't bring him back and ask. If you do get a message through, though, let me know. I have some questions for him... :-) $\endgroup$ – Asaf Karagila Sep 16 '13 at 14:06
  • 2
    $\begingroup$ @AsafKaragila I'm sorry to admit that every time I read a book or paper by Tarski I learn new things. Are you sure he did not answer any of your questions someplace you have not noticed? $\endgroup$ – Colin McLarty Sep 16 '13 at 14:15
  • $\begingroup$ Well, I wanted to ask him for some clarification on an old book of him... and some personal questions about his good friend Lindenbaum, who was killed by the Nazis. (Does this count as an application of Godwin's law?) $\endgroup$ – Asaf Karagila Sep 16 '13 at 14:28
  • $\begingroup$ Do the ruler-and-compass constructible reals constitute a decidable subset of the algebraic reals? Would you count this as an answer to the question? $\endgroup$ – Joel David Hamkins Sep 16 '13 at 14:30
  • 1
    $\begingroup$ No, I mean only ordinary computability. There is a computable presentation of the algebraic reals, that is, a copy of it where every algebraic real has a finite description, and we can decide the full theory in terms of those descriptions. The algebraic reals include all those that are constructible by ruler and compass (from a unit length), and I am asking whether the collection of such reals constitutes a decidable subcollection. In other words, can we decide if a given algebraic number is constructible? This is one way of thinking about your question that makes it concrete. $\endgroup$ – Joel David Hamkins Sep 16 '13 at 14:44

Here is a partial affirmative answer, where we consider existence-and-uniqueness assertions rather than just existence assertions.

Consider the collection of algebraic reals, which form a real-closed field, and give each such algebraic real a finite name, of the form, "the $k^{th}$ solution of $p(x)=0$", for a specific integer polynomial $p$ and specific number $k$. These descriptions are expressible in the language of ordered fields, and so because of Tarski's decidability result, we can decide all questions in this language about these reals under these descriptions. Thus, we have a computable presentation of the algebraic reals, in which we can decide all questions of geometry for algebraic points in Euclidean space using Tarski's algorithm.

Consider now the reals that are constructible by straightedge and compass. These are exactly those algebraic reals in the quadratic closure of $\mathbb{Q}$. I claim that we can decide which of our algebraic reals is constructible, since when we are given an algebraic real $r$, we have a description of a polynomial realizing $r$ as algebraic. Using the computable splitting algorithms (e.g. this or this), we can find a minimal polynomial for $r$ and thereby tell if $r$ is constructible or not.

Now, consider a weakening of your question, where we have not just an existence claim, but an existence-and-uniqueness claim. That is, suppose that we prove there is a unique $r$ for which $\varphi(r)$ in the theory of real-closed fields. Now, we may search in our computable model until we find the instantiating instance using our finite descriptions of the algebraic reals. And given this $r$, we can as explained above decide whether or not this $r$ is constructible. Thus, we have an algorithm to decide all such existence-and-uniqueness instances of your phenomenon, whether the instantiating point is constructible or not.

| cite | improve this answer | |
  • $\begingroup$ Okay, I see the point about uniqueness. Euclid very rarely makes existence claims that are not uniquely determined up to orientation by the data. And I doubt he makes any that could not be clarified that way. So all instances have the same degree and your algorithm will decide all his cases. $\endgroup$ – Colin McLarty Sep 16 '13 at 16:04
  • $\begingroup$ I deleted my comment about minimal degree. I agree with you that it seems to me that the existence claims of Euclid can usually be made into existence-uniqueness claims simply by adding some orientation information to the context, and this will be expressible in the language of real-closed fields. So most of the instances you may have in mind are covered by the existence-and-uniqueness argument. I'm not sure whether this requirement can be removed. $\endgroup$ – Joel David Hamkins Sep 16 '13 at 21:08
  • $\begingroup$ I'll accept this answer as suiting the problem I have. That is to explore and perhaps make more precise Mazur's fine remark that mathematicians of Euclid's time might reasonably have supposed arithmetic could have as complete a theory as Euclid's geometry but we know quite the opposite today. I will post a different question pointed at the decidability of the field of constructible numbers. $\endgroup$ – Colin McLarty Sep 17 '13 at 12:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.