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).

  • $\begingroup$ Yes; see Tarski's axioms: at least plane geometry. $\endgroup$ Commented Nov 12, 2021 at 13:37
  • $\begingroup$ See A. Tarski & S. Givant, Tarski's system of geometry, BSL (1999) $\endgroup$ Commented Nov 12, 2021 at 13:44
  • 2
    $\begingroup$ Since the theory is complete, this is mostly a question of which statements in Euclidean geometry can be translated into Tarski's language. $\endgroup$
    – nombre
    Commented Nov 12, 2021 at 14:58
  • 1
    $\begingroup$ Thanks for the comments and the reference. @nombre: yes, this is more or less what I was hoping to hear - in general terms. $\endgroup$
    – knovice
    Commented Nov 12, 2021 at 15:20
  • $\begingroup$ 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. $\endgroup$ Commented Mar 19, 2022 at 0:33

1 Answer 1


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.

Then the question remains: which statements of geometry can be so expressed? In Tarski's system you can talk about parallelism and intersections of lines and congruence of angles, and if you specify a unit line segment, you can measure lengths of line segments and add/multiply/divide them (and in fact the points on a line can be turned into a real-closed field). So for instance, the theorem of Pythagoras, Pappus and Desargues can be expressed in Tarski's language. You can also talk about the areas of polygons. All theorems of Book 1 in Euclid's elements can be formulated and therefore proved in Tarski's system.

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.



You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .