Do Euclidean spaces prove more statements than Euclidean geometry? Is there a statement in the language of Euclidean geometry (as defined in Hilbert's axioms) that 


*

*is undecidable by Euclidean geometry

*is provable in the Euclidean space of dimension 3


I'm trying to get an opinion about whether geometrical proofs using coordinates introduce a bias, or decisions that are absent in Euclidean geometry.
 A: By any reasonable interpretation, the answer is no.  Hilbert's axioms are categorical, meaning that you can prove that any two structures which satisfy them are isomorphic.  In particular, you can prove any structure satisfying Hilbert's axioms is isomorphic to $\mathbb{R}^3$ (with its usual geometric structure).  So any statement you can prove about $\mathbb{R}^3$ (and which involves only the structure described by Hilbert's axioms) is true of any other model of Hilbert's axioms.
(Note that in the context of Hilbert's axioms, it's not very meaningful to talk about "the language of Euclidean geometry" or statements that are "decidable in Euclidean geometry".  Hilbert's axioms are not a self-contained proof system.  Rather, they are an axiomatizaton of a structure which is intended to be interpreted within an ambient set theory.  So the language you can use when talking about Euclidean geometry via Hilbert's axioms is really your entire background set theory, or at least some big fragment of it.  A proof that uses fantastically complicated auxiliary set-theoretic constructions to reason about an arbitrary model of Hilbert's axioms is a perfectly good Euclidean geometry proof, if you define Euclidean geometry by Hilbert's axioms.)

If you instead use a first-order axiomatization like Tarski's axioms, the answer depends on what you mean by "the language of Euclidean geometry".  The most obvious meaning is the first-order language of Tarski's axioms, in which case the answer is no: Tarski's axioms generate a complete first-order theory, so the first-order statements you can prove from them are exactly the first-order statements which are true of any single model (e.g., $\mathbb{R}^3$).  But if you allow higher-order statements, then the answer is yes.  For instance, $\mathbb{R}^3$ is uncountable, but there are models of Tarski's axioms which are countable.  Or for something more classical, Archimedes' axiom is true in $\mathbb{R}^3$ but is not true in arbitrary models of Tarski's axioms.
