First-order Euclidean Geometry I gather that the axiomatisation of Euclidean Geometry, e.g., by Hilbert, can be used with First-order Logic and has good properties.  Is it fairly complete in the sense, say, that it proves everything Euclid did? E.g., Eudoxus' theory of the reals and the area of the circle....
 A: Hilbert's axiomatization is second-order. However, there is a first-order axiomatization by Tarski, which is complete. (And because the theory is recursively axiomatized, it is decidable.)
We cannot develop the full second-order theory of real numbers within the Tarski geometry. For instance, the "plane" $\mathbb{A}^2$, where $\mathbb{A}$ is the field of real algebraic numbers, is a model of Tarski's geometry.  The Eudoxean theory of equality of ratios, which comes so strikingly close to the modern definition of real number, cannot be developed within Tarski's geometry, for the set of integers is not definable in that geometry.
However, for example all of Book I consists of theorems of Tarski's geometry. 
For a complete list of Tarski's axioms, with additional information and references, please see this.
A: No, Pythagorean planes, i.e. planes satisfying Hilbert's fourteen axioms up through the Archimedian axiom), form a strictly weaker geometry than Euclidean planes.
Hilbert planes correspond to constructions with straightedge and "segment transporter," which almost but can't quite do the job of a straightedge and a compass. Because of this, I get the impression that you cannot do as much with circles as you can in Euclidean geometry. You'll notice a distinct absence of circles in Hilbert's Foundations of geometry.
Old and New Results... by Greenberg gives a particularly helpful summary of how they are related. 
