The Pythagorean theorem and Hilbert axioms Can one state and prove the Pythagorean theorem using Hilbert's axioms of geometry, without any reference to arithmetic?
Edit: Here is a possible motivation for this question (and in particular for the "state" part of this question). It is known that the theory of Euclidean geometry is complete. Every true statement in this theory is provable. 
On the other hand, it is known that the axioms of (Peano) arithmetic cannot be proven to be consistent. So, basically, I ask if there is a reasonable theory which is known to be consistent and complete, and in which the Pythagorean theorem can be stated and proved.
In summary, I guess I am asking - can we be sure that the Pythagorean theorem is true? :)
 A: Although students are seldom aware of this fact, the Pythagorean Theorem, as described by Euclid, makes absolutely no reference to numbers.  Where students say "the square of the hypotenuse," Euclid wrote "the square on the hypotenuse."  And the assertion is that this is the same as the squares on the two sides.  Here "same" means content, and "content" is not explicated further.  Neither of the two proofs of the Pythagorean Theorem in Elements makes any reference to arithmetic.
Hilbert, in his axiomatization, did not make any reference to arithmetic either.  But Hilbert's axiomatization is really not suitable for a further discussion of the OP's question.
This is because Hilbert's axiomatization of geometry very much shows its age.  His Axiom  of Continuity (completeness) is second-order. Hilbert developed the axiomatization many years before he started to take a serious interest in Logic.
A more modern first-order axiomatization, or series of axiomatizations, is due to Tarski.  Again, the axioms do not mention or use arithmetic.  But naturally a version of the Pythagorean Theorem is derivable from the axioms.
Tarski showed that his theory is complete.  It is recursively axiomatized, and hence the theory is decidable.  
This reminds me of a famous reply that Euclid is said to have made to one of the Ptolemies, when the latter asked whether there was an easier path to geometry than pushing one's way through the thickets of Elements (I am paraphrasing).  Euclid is said to have replied something to the effect that there is no royal road to geometry.  
Presumably, the story, like most such stories, is false. For one thing, essentially the same story is told of Menaechmus and Alexander the Great.  For another, it can be unhealthy to dis a king.  Euclid would surely not risk having his grant, and perhaps other things, cut off.
Anyway, if Euclid did make that comment about geometry, he was wrong.  Any king or queen with access to sufficient computing power can sip wine while the machine crunches through a problem.
I guess I should remark that Tarski's algorithm was grossly inefficient.  But more recently there has been significant progress.
Back to numbers!  Tarski showed that any model for his geometry is isomorphic to the geometry of  $\mathbb{F}^2$, where $\mathbb{F}$ is an algebraically closed field of characteristic $0$. (Hilbert had shown, sort of, that the geometry of his synthetically defined plane was the geometry of $\mathbb{R}^2$.)
Tarski's algorithm for geometry depends on the fact (that he proved) that the theory of algebraically closed fields of characteristic $0$ is complete.   Since the theory is recursively (but not finitely) axiomatizable, it is decidable.  The decision procedure for elementary geometry involves translating a geometric problem, via coordinatization, into a sentence of "elementary algebra" and then determining whether that sentence is true in an algebraically closed field of characteristic $0$.  All such fields are elementarily equivalent, so if a sentence is true in one such field, it is true in all.  
Note that Number Theory cannot be developed within the first-order theory of fields of characteristic $0$.  There is no formula $N(x)$ in that theory such that $N(x)$ holds iff $x$ is an integer.  As we know, elementary Number Theory, as opposed to the theory of algebraically closed fields of characteristic $0$, is undecidable.
And finally, let me reassure the OP that the Pythagorean Theorem is true. And any of the usual axiomatizations of Number Theory is consistent.  We all know that, the axioms are obviously true in the non-negative integers.  We can prove that the consistency of any reasonably useful axiomatization of Number Theory cannot be proved within that theory, but that's an entirely different matter. 
