Segment Construction

Given any two line segments, the second can be "extended" by a line segment congruent to the first.

Such economy of primitive and defined notions means that Tarski's system is not very convenient for doing Euclidian geometry.

Rather, Tarski designed his system to facilitate its analysis via the tools of mathematical logic, i.e., to facilitate deriving its metamathematical properties.

Tarski's system has the unusual property that all sentences can be written in universal-existential form, a special case of the prenex normal form. This form has all universal quantifiers preceding any existential quantifiers, so that all sentences can be recast in the form

This fact allowed Tarski to prove that Euclidean geometry is decidable: there exists an algorithm which can determine the truth or falsity of any sentence.

Tarski's axiomatization is also complete. This does not contradict Gödel's first incompleteness theorem, because Tarski's theory lacks the expressive power needed to interpret Robinson arithmetic (Franzén 2005, pp. 25–26).