# Tarski's elementary Euclidean geometry

It is a well-known theorem of Tarski that (what is now called) Tarski's elementary Euclidean geometry is a decidable theory. This is a first-order theory, as opposed to Hilbert's second-order axiomatization of Euclidean geometry.

My (somewhat vague) question is whether Tarski's axiomatization encompasses (i.e., proves) "most" geometry statements of interest, at least, say, at the college level geometry courses, so that one could arguably state that "Tarski's result mechanizes questions in Euclidean geometry" in such a context. In other words, I would like to have a better idea of the scope of "elementary geometry" within general Euclidean geometry.

I would also be happy if you could give me examples (or categories) of geometric statements that lie outside of the scope of Tarski's axiomatization (i.e., they essentially need something like Hilbert's second-order system).

• Yes; see Tarski's axioms: at least plane geometry. Nov 12, 2021 at 13:37
• See A. Tarski & S. Givant, Tarski's system of geometry, BSL (1999) Nov 12, 2021 at 13:44
• Since the theory is complete, this is mostly a question of which statements in Euclidean geometry can be translated into Tarski's language. Nov 12, 2021 at 14:58
• Thanks for the comments and the reference. @nombre: yes, this is more or less what I was hoping to hear - in general terms. Nov 12, 2021 at 15:20
• My guess (and I certainly don't know for certain, much less have any proof) is that anything that needs something like Hilbert's second-order system would come down to anything essentially requiring a second-order version of the completeness axiom schema. At least in my opinion/perception, it seems like that is the only axiom (schema) for which the restriction to first-order logic potentially meaningfully limits the "expressiveness". But obviously this conjecture/hypothesis is a LONG way from anything remotely resembling a valid proof. Still, I would be VERY surprised if this weren't true. Mar 19, 2022 at 0:33

Tarski's first-order system is complete, which means that a sentence is provable if and only if it is true in a model of the axioms, which happens if and only if it is true in all models of the axioms. One such model is the ordinary Euclidean plane $$\Bbb{R}^2$$. This plane is also the only model (up to isomorphism) of Hilbert's second order geometry and of Tarski's second order geometry (which comes from Tarski's first-order system by replacing the axiom schema of continuity by a single axiom of continuity that quantifies over arbitrary sets of points).
So if you have a statement of geometry that can be expressed as a sentence in Tarski's first-order language, then this statement is true in ordinary second order Euclidean geometry $$\Bbb{R}^2$$ if and only if the sentence is provable from Tarski's axioms, which can be determined with Tarski's decision method.
As to statements that can't be so expressed: the Archimedes axiom is a theorem of second order Euclidean geometry that says "given two positive-length line segments $$S_1$$ and $$S_2$$, you can always find a natural number $$n\in\Bbb{N}$$ so that $$n S_1$$ is longer than $$S_2$$". This theorem cannot be proven in Tarski's system because there are real-closed fields that contain infinitesimals. Euclid (implicitly) uses the Achimedes axiom to develop his theory of proportions in Book 5, so those statements probably also cannot be proven in Tarski's system. In general, statements that refer to integers or to "all polygons" or to "... can be constructed with straightedge and compass" cannot be expressed in Tarski's first-order system. Lengths of curves and areas of curved regions also cannot be expressed in that system.