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?