Hilbert's axioms predate the development (or at least the wide adoption) of fully symbolic logic, so they are expressed in partially informal language -- though Hilbert strove to make them as precise as he could.
They include the Axiom of Archimedes, formulated in language that presupposes that the natural numbers are already known. As such, if we want to formalize the system in a modern sense, we'd need to add in some machinery for talking about integers, and it would be somewhat hard to avoid making that machinery powerful enough that Gödel's theorem would apply to it.
Furthermore, there's also an Axiom of Completeness which attempts to claim directly that the structure we're speaking about is maximal in a certain technical sense. In the modern view of formal theories, this hardly qualifies as an "axiom" at all, because it doesn't assert the truth of any formula interpreted inside the language of the theory itself. In modern terms, it appears to try to say that every existential formula of a certain shape that is true in some model of the other axioms must itself be elevated to axiomatic status.
However, it is not clear that "formulas that are true in some model of the other axioms" are even recursively enumerable -- which means that Hilbert's axioms, interpreted in this way, are not effective. In other words there's no systematic way to check whether a purported proof is valid or not. Therefore Gödel's incompleteness theorem does not apply to Hilbert's axioms. It seems at least plausible that if we interpret them inside set theory in the above sense, they do have $\mathbb R^3$ as their only model up to isomorphism. (That is, whatever the set theory in question considers $\mathbb R^3$ to be).
Tarski's axioms for geometry were created after formal logic was better developed. They form a genuine, effectively axiomatized, first-order theory, with no ad-hoc appeals to integers, sets, or model theory. They manage to be a complete theory because they are not strong enough to express or simulate arithmetic.
The price paid for the completeness in Tarski's case is that the language the axioms are formulated in is not expressive enough to speak of even finite sets of points, or for example general polygons. Every theorem has to be proved separately for triangles, quadrilaterals, pentagons, and so forth.
This restriction is unavoidable for a complete theory, because as soon as we extend the language with a way to speak of finite sets of points and lines in a reasonable way, we can use those sets as proxies for natural numbers (each set representing the number of points in it) and begin to speak about enough arithmetic that Gödel's incompleteness theorem will apply to it.
Later, Tarski gave his own axiomatization of Euclidean geometry that is entirely in first order logic so by Gödel's completeness theorem, it can demonstrate its consistency, it is decidable and complete.
As mentioned in the comments, this is a complete misunderstanding of what the completeness theorem says. Tarski's geometry cannot even speak about its own consistency, much less prove it.
I would like a proof that first order logic is undecidable, but without using arithmetic
But hold on! The proposition "first order logic is undecidable" is, when unpacked, just a proposition of the form "there is no computable function which does so-and-so". So of course a proof of this proposition is going to have to come from an application of the general theory of computable functions. (We might only need a naive ability to recognise a computation when we see it to establish the positive claim that some function can be computed: but to establish a negative, that there is no computable function which does so-and-so, we do need some general theory which can enable us to talk about the limits of the computable).
Now, the relevant computations here are over finite strings that constitute wffs and proofs, so the background theory we need in fact is or is tantamount to the theory of arithmetical computable functions (for you can code finite strings by numbers in familiar ways; or indeed we can go in the opposite direction and reconstruct arithmetic in the theory of finite strings). So the natural lines of proof that first order logic is undecidable will come from the theory of computable arithmetical functions (perhaps in slight disguise). In sum, broadly arithmetical considerations (far from being extraneous, a "tortuous" diversion) are exactly what we would expect to use here.
Added: What I wrote above was [at least intended to be] consistent with the sort of points Carl Mummert's makes in his typically elegant answer. It is the theory of computability that needs to be invoked: but the point at which it gets applied doesn't have to be to a formal arithmetic. As Carl very nicely points out, we could go instead via Tarksi's proof about groups. However, I was taking it that that sort of thing would seem to the OP even more "tortuous" a route to the undecidability result; and we are still applying the theory of computable numerical functions.
That's the main point to be made, but I can perhaps add a subsidiary comment on the remark
We cannot construct a model of ϕ just because it requires an infinite domain.
Well, by any ordinary constructive standards the wff you describe (losing the unintended negation) has a constructively acceptable model -- the natural numbers in their natural order! What is wrong with that?
Best Answer
The completeness theorem - also due to Godel! - says that this always happens, at least for first-order theories:
This does not contradict the incompleteness theorem. That result says that $PA_1$ is not a complete theory: there is a sentence (indeed, lots of sentences) $\sigma$ such that $PA_1\not\vdash\sigma$ and $PA_1\not\vdash\neg\sigma$, or equivalently by the completeness theorem $PA_1\not\models\sigma$ and $PA\not\models\neg\sigma$. The term "(in)complete" is being overloaded here:
A theory is complete if it proves or disproves each sentence.
A proof system $P$ is (sound and) complete with respect to an existing semantics if $P$-provability coincides with entailment in the sense of that semantics.