Complete geometry theory other than Tarski? It is well known that Tarski's axioms for Euclidean geometry is recursively axiomatizable and complete, and hence also decidable. Basically it is because the theory of real closed field has these properties. Does there exist other Euclidean or non-Euclidean geometry theory, that extends Hilbert's axioms and share these properties?
Regarding Euclidean geometry, since models of Hilbert's axioms plus parallel axiom are exactly cartesian products over ordered Pythagorean fields, the question is, as I understand, the same as asking for complete extension of theory of ordered Pythagorean field. I know very little about model theory but it seems there are not many theories known to be decidable.
I know even less about models of non-Euclidean geometry. I just learned that (to my surprise) the theory of hyperbolic geometry is decidable. I could not find the reference. Does this refer to the finite theory consisting of Hilbert's axioms plus a suitable hyperbolic axiom, or some infinite theory that resembles Tarski's axioms?
 A: Simone Ramello is correct in identifying Schwabhäuser's Metamathematische Methoden in Der Geometrie as the proper reference for this subject, but as he suggests this book has not been translated into English.
That said, you only need translations from two pages. I omit a discussion of Tarski's axioms, which can be found on Wikipedia or, in a more digestible form, from section 4 of this paper by Beeson et al. When looking at Beeson's list, note that the circle axiom CA is actually a restricted special case of the continuity axiom A11 and does not need to be counted separately. (The distinction here is that the more general continuity axiom A11 allows you to find a point between any pair of sets, whereas the circle axiom only allows you to locate the point of intersection between a circle and a straight line. On an intuitive level, it's something like the difference between extending the rational numbers to the reals by either providing the fully-general least upper bound axiom, or just asserting the existence of square roots.) In Beeson's list, A10 is equivalent to Euclid's parallel axiom.
Schwäbhauser in Part II, section 2.1(i)(1) and 2.1(iii) defines $n$-dimensional absolute geometry as absolute geometry with continuity essentially by taking axioms A1-A7 from Beeson's list and calling them "dimension-free absolute geometry," then replaces A8 and A9 with lower- and upper-dimensional axioms (though you can keep A8 and A9 as written if you are interested in 2-dimensional geometry) to get $n$-dimensional absolute geometry. In 2.1(i)(5) he defines "full n-dimensional absolute geometry" by adding axiom A11.
So for 2-dimensional geometry we basically have all of Beeson's axioms (A1 through A11) except A10, which is the Euclidean parallel postulate. In section 2.4 Schwabhäuser replaces it with Hilbert's Axiom of Hyperbolic Parallels to get what he would call "full n-dimensional hyperbolic geometry." The formula for this new axiom (called HP in the book) is a symbolic rendition of this large expression, which can be expressed entirely in terms of collinearity and betweenness (where collinearity can itself be defined in terms of betweenness:
If points $a$, $c$, and $d$ are not collinear, then there exist points $b_1$ and b_2$ such that the following three things are true:

*

*$a$, $b_1$, and $b_2$ are not collinear,

*For all $u$, if $u$ is between $b_1$ and $b_2$ and the three points $u$, $b_1$, and $b_2$, are distinct (unequal to each other), then there exists an $x$ collinear with $c$ and $d$ such that $u$ is between $a$ and $x$.

*There is no $x$ collinear with $c$ and $d$ for which either $b_1$ or $b_2$ is between $a$ and $x$.

(End of the HP axiom.)
He goes on to explain the axiom intuitively: "For any non-collinear points $a$, $c$, $d$ there are always two rays $\overrightarrow{ab_1}$, $\overrightarrow{ab_2}$ starting from $a$, which are not contained in a line [that is, they're not exactly opposite to each other] and which do not intersect the line $\overleftrightarrow{cd}$, while every other ray emitted from $a$ within the angle $\angle b_1ab_2$ and starting from $a$ intersects the line $L(ad)$" and he provides a figure that alas, I cannot reproduce here.
So the axiomatization you seek would comprise:

*

*Axioms A1 through A7 from Beeson's list (dimension-free absolute geometry)

*A lower- and upper-dimensional axiom (A8 and A9 from Beeson's list will suffice if you are working in two dimensions; otherwise you have to use the axioms from PlanetMath)

*Hilbert's Axiom of Hyperbolic Parallels. This replaces axiom A10, which is explicitly Euclidean.

*The continuity axiom A11.

Schwabhäuser calls that collection of axioms $H^2_n$, where the $2$ means that the full second-order axiom of continuity is being used, and the $n$ tells the dimensionality of the axioms you're using to replace A8 and A9.
In section 2.5, Schwabhäuser asserts that a structure is a model of axioms $H_n$ if and only if it's isomorphic to the $n$-dimensional Klein space over the real numbers. The Klein space is essentially the Klein-Beltrami model from Wikipedia: the points are  $n$-dimensional vectors of real numbers whose lengths [the usual vector norm] are less than 1, where $y$ is between $x$ and $z$ iff there's a real number $\lambda$ between $0$ and $1$ for which ${\bf y}-{\bf x}=\lambda({\bf z}-{\bf x})$ [this is the same definition of "betweenness" that you would use for ordinary vectors in ordinary models], and $xy\equiv uv$ iff the distance $(1-{\bf x}\cdot{\bf y})^2\over(1-|{\bf x}|^2)(1-|{\bf y}|^2)$ equals the similarly-defined distance for $u$ and $v$.
What he means in 2.5 is that any formula about points in $n$-dimensional hyperbolic geometry, written in terms of Tarski's betweenness and equidistance operators, can be converted into an equivalent formula about $n$-dimensional vectors of real numbers, where distances are represented in terms of that funky Klein-Beltrami metric but betweenness is the same as it always was. But the equivalent formula involving real numbers uses only field operations (addition, subtraction, multiplication, and division) so it's decidable if and only if your theory of the real numbers is decidable.
Tarski proved that the first-order theory of the real numbers (the theory of "real closed fields") is complete and decidable in 1933. I'm pretty sure the full second-order theory of the real numbers is not complete because set theories generally aren't complete. Schwabhäuser noted this distinction in section 2.5 and I glossed over it; basically he said that if you replace the second-order continuity axiom A11 with an axiom scheme consisting of all of the first-order axioms (that is, the only sets you're allowed to use in axiom A11 are those that are defined in terms of relationships between points---no funny business with sets defined in terms with other set quantifiers) then the resulting geometry is equivalent to the Klein-Beltrami model over a real-closed field (that is, the real numbers with a first-order completeness axiom instead of the full second-order least upper bound axiom), which is what Tarski proved is decidable.
So to sum things up: take Beeson's axioms, replace A10 with AP, optionally replace A8 and A9 with corresponding axioms for a higher-dimensional space, and restrict A11 to a first-order axiom schema, and you have a complete Tarski-style axiomatization of $n$-dimensional hyperbolic geometry.
