  Euclid's reasoning is essentially constructive. Tarski's elegant and concise
first-order theory of Euclidean geometry, on the other hand, is essentially
non-constructive, even if we restrict attention (as we do here) to the theory
with line-circle and circle-circle continuity in place of first-order Dedekind
completeness. Here we exhibit three constructive versions of Tarski's theory.
One, like Tarski's theory, has existential axioms and no function symbols. We
then consider a version in which function symbols are used instead of
existential quantifiers. The third version has a function symbol for the
intersection point of two non-parallel, non-coincident lines, instead of only
for intersection points produced by Pasch's axiom and the parallel axiom; this
choice of function symbols connects directly to ruler-and-compass
constructions. All three versions have this in common: the axioms have been
modified so that the points they assert to exist are unique and depend
continuously on parameters. This modification of Tarski's axioms, with
classical logic, has the same theorems as Tarski's theory, but we obtain
results connecting it with ruler-and-compass constructions as well. In
particular, points constructively proved to exist can be constructed with ruler
and compass, uniformly in parameters; the same is true with non-constructive
proofs if several constructions are allowed for different cases.
