Logic – Axioms for Synthetic Euclidean and Hyperbolic Geometry

hyperbolic-geometrylo.logicmg.metric-geometry

There are familiar analytic equiconsistency proofs for Euclidean and hyperbolic geometry.  Those proofs are so robustly geometric that it seems like they must have synthetic analogues.

Looking into the literature, though, I wonder if I am too optimistic about this.  The most common rigorous axiomatizations for synthetic Euclidean and hyperbolic geometry, so far as I can tell, are Hilbert's from his Foundations of Geometry, with two changes.  They omit the non-elementary axiom of continuity, and they add something to assure that circles will actually have points of intersections with lines and other circles that they cross.  The only difference, in these axiomatizations, between Euclidean and hyperbolic geometry is in the axiom of parallels. But this synthetic hyperbolic geometry is incapable of some constructions that we take pretty much for granted both in Euclidean geometry and also (more to my point) in analytic hyperbolic geometry.   Notably $n$-section of lines, see trisection-of-a-hyperbolic-line-segment.  Maybe the analytic equiconsistency proofs really do not transfer well to synthetic geometry.

I know Greenberg's discussion of axiomatic issues in Greenberg. But I do not have all his references at hand.  Judging from the ones I do have (including Hartshorne) it seems likely that  his discussion of equiconsistency for the two geometries (pp.213-214) refers to analytic presentations of geometry.

Can I find mutually interpretable axioms for synthetic Euclidean and hyperbolic geometry?

Edit: Erik Walsberg's comment about Tarski's axioms answers my title question, even though not in the way I had in mind when I wrote the text.  My text was ambiguous about "synthetic" methods, in just the way that Tarski What is elementary geometry? means when he says   "In colloquial language the term elementary geometry is used loosely […with] no well determined meaning."   

Hilbert, Tarski, and Greenberg all show that the important logical distinction characterizing elementary methods is not between using or not using coordinates in some field.  It is between using or not using higher order notions like point-set continuity and limits.  First order algebraic considerations on fields (notably pythagorean fields) are already implicit in Euclid and  central to successful first-order elementary geometry.  

The work that led me to this question is about interpretation in first order logic, and not about compass (or horocompass) and straightedge or other such construction methods, and really not about avoiding coordinates.  So my title was true to my actual concern.  Some of my text concerning synthetic methods was less relevant (though those questions too intrigue me).  Walsberg's comment is really an answer both to the question as titled and to my actual concern, though he correctly saw I had another issue about methods also in mind. 

Best Answer

Here is an expanded version of my previous comments. There are a lot of things to check here and I haven't.

In my opinion the right axioms for Euclidean/Hyperbolic geometry are the Tarski axioms. Tarski works in a system where the domain is $\mathbb{R}^2$ and you have two relations, a ternary betweenness relation and an equidistance relation $E(x,y;x',y')$ which says that the line segments $\overline{xy}$ and $\overline{x',y'}$ are congruent. In this system all the axioms are phrased in terms of points, not in terms of both points and lines like in Euclid. Lines emerge as definable sets.

The Tarski axioms for Euclidean geometry are on Wikipedia, and you just change the parallel postulate to get axioms for Hyperbolic geometry. The usual proof of bi-interpretability goes by showing that both theories are bi-interpretable with the theory of $(\mathbb{R},+,×,<)$, i.e. the theory of real closed fields. I'm not sure where the hyperbolic case was written down, maybe by Szmielew. I don't know of a synthetic version of the proof.

But it should be possible to get a synthetic proof. There are well-known Euclidean models of the hyperbolic plane, like the Klein model, so it should be enough to make a Hyperbolic model of the Euclidean plane.

Edit: I think that my initial attempt at the Hyperbolic model of the Euclidean plane fails, because equidistance isn't definable. Following a suggestion of @ColinMcLarty, I will describe a different model that I think works. This model is from Greenberg's book "Euclidean and Non-euclidean geometries".

Let $\mathbb{H}$ be the Hyperbolic plane. In this model the points are just the points in $\mathbb{H}$ and the lines all all lines in $\mathbb{H}$ through the origin together with the curves in $\mathbb{H}$ that are equidistant from a line through the origin.

To get a model of Euclidean geometry we need a betweenness and equidistance relationship, and these relationships need to be definable in $\mathbb{H}$. The betweenness relationship is easy, you just need to observe that the lines form a uniformly definable family of sets. Equidistance is more complicated.

Greenberg describes a map $\rho : \mathbb{H} \to \mathbb{R}^2$ and says that the equidistance relation on $\mathbb{H}$ is the pull-back of the equidistance relation on $\mathbb{R}^2$ by $\rho$. We can put polar coordinates on $\mathbb{H}$ in the same way as on the Euclidean plane. We fix a ray $\ell$ through the origin and let the polar coordinates of $p \in \mathbb{H}$ be $(r,\theta)$ where $r$ is the Hyperbolic distance from the origin to $p$ and $\theta$ is the angle that $p$ makes with $\ell$. If $p \in \mathbb{H}$ is the point with polar coordinates $(r,\theta)$ then $\rho(p)$ is the point $$ \rho(p) = (\sinh r \sin \theta, \sinh r \cos \theta) = \sinh r (\cos \theta, \sin \theta). $$ So $\rho(p)$ is the point in $\mathbb{R}^2$ whose (euclidean) polar coordinates are $(\sinh r, \theta)$.

Now let's suppose that $\mathbb{H}$ is the Poincare disc model. I think it is enough to show that $\rho$ is semialgebraic, i.e. definable in $(\mathbb{R},+,\times,<)$. The Hyperbolic distance $r$ of $p$ from the origin is not a semialgebraic function of $p$, but it is the arcsinh of a semialgebraic functions, see Wikipedia. (On Wikipedia there is a factor of $2$ in from the arcsinh, but that is just a scaling factor, so we can drop it). I think it should be pretty clear that $\rho$ is semialgebraic.

Once we know that $\rho$ is semialgebraic we know that the equidistance relation on our Hyperbolic model of Euclidean geometry is semialgebraic. This should imply that it is definable in Hyperbolic geometry, but one would need extra arguments to see it directly.