Can Tarski decide constructibility in elementary geometry?

Question

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?

Answer 1

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.