Tarski-like axiomatization of spherical or elliptic geometry

Question

Preamble

Tarski's axioms formalize Euclidean geometry in a first-order theory where the variables range over the points of the space and the primitive notions are betweenness $Bxyz$ (meaning $y$ is on the line segment between $x$ and $z$, inclusive) and congruence $xy\equiv zw$ (meaning the line segment between $x$ and $y$ is the same length as the line segment between $z$ and $w$). One of the features of this system that I like is that it is somewhat modular; the axioms of upper and lower dimension can be chosen independently of the other axioms to fix the dimension of the space, and, notably, the axiom of Euclid can be simply replaced by it's negation to change it into an axiomatization of hyperbolic geometry.

The question

It is very easy to adapt Tarski's axioms of Euclidean geometry to axioms of hyperbolic geometry. I am wondering if something similar can be done for spherical and elliptic geometry. From what I can tell, the answer is yes, but the betweenness and congruence relations have to be changed because of the different topology of spherical and elliptic geometry, compared to Euclidean and hyperbolic geometry.

Some more details

Specifically, the relations in Tarski's axioms indirectly rely on the fact that two points uniquely define a line segment in Euclidean and hyperbolic geometry, but this is not the case in spherical and elliptic geometries. Generally, two points will define two line segments, one going around the sphere the short way, and the other the long way. (In elliptic geometry, the line which is made up of these two line segments is still unique even when the points are maximally distant. In spherical geometry the problem is worse as the line is not uniquely defined when the points are antipodal.)

So I think that the betweenness relation would have to be modified to a relation meaning something like "$x$ is on the line segment that goes from $y$ to $z$ through $w$", and the congruence relation would have to be modified to something meaning "the line segment from $x$ to $y$ through $z$ has the same length as the line segment from $u$ to $v$ through $w$" - every line segment specification requires an additional point of information. But I am having difficulty figuring out how the behaviour of these new relations would be axiomatized. (And they very well might be different between spherical and elliptic.) Does anyone have any ideas?

Once the basic properties of these relations were axiomatized, I do not think it would be too difficult to translate the various geometrical axioms of Tarski's system (segment construction, Pasch's axiom, five-segment axiom, dimension axioms, and an axiom making the space curved). But the trick is getting the primitive relations to work correctly.

Thanks!

Answer 1

What you are working on is a problem that I would like to solve some day. I don't think I can help you much at this point but here's what I can say:

-Spherical and elliptical geometries can't be axiomatized the same because there being more than $2$ lines joining more than one set of $2$ distinct points has to be first order expressible if one wants to be able to say anything regarding lines and points.

-One main distinction between Euclidean planes and $2$-spheres is that spheres are bounded. This is first order expressible too if you have congruence and betweeness.

-Though I understand the benefit of a modular approach to axiomatizing geometries, I am not sure this kind of approach is always possible.

-Maybe allowing every point to be between two antipodal points (thus not taking a forth point into account) isn't a problem. I'm just saying that; I get that you'd prefer two points to always determine a line segment.

Do you have a reference for your claim that hyperbolic geometry arises from negating the axiom of Euclid?

Do you have a method for proving that your new system of axioms (once you have figured it) is an axiomatization of spherical geometry? Both the formulation and the proof would be difficult I believe. Tarski proved that models of his system are cartesian planes parametrized by real closed fields, and he did so by defining arithmetic operations on points of one line. His axiomatization is interesting because of this and what this implies (model completeness and completeness). If one seeks a more visual are powerful axiomatization, I think Hilbert is better since lines are elementary and only real planes satisfy the axioms. There are versions of hyperbolic, spherical and elliptical geometry a la Hilbert.

Anyway, if you are interested in Tarski's point of view, arguably, what you would have to prove is that any model of your system is isomorphic to $\{(x,y,z) \in F^3 \ | \ x^2 + y^2 + z^2 = 1\}$ where $F$ is real closed, with betweenness and congruence defined using the "scalar product" $(x,y,z), (a,b,c) \mapsto xa + yb + zc$.

Assuming the definitions of arithmetic operations can be adapted to the points of a great circle, since a circle can't be a field, you would then have to understand how the field structure emerges from the poor arithmetic structure on the circle and this might be a difficult problem.

I am not saying this to discourage you, I think this is a beautiful task!

Answer 2

One way you can do that is use the Tarski's axioms for 3D space, and then do geometry on a sphere. Given a center $O$ and a point $a$ on the sphere, we say that $x$ is on the sphere if $$Ox \equiv Oa$$. We then just work with these points.