Tarski's axioms

Lore & Background

Tarski's system was the first system of Euclidean geometry simple enough for all axioms to be expressed in terms of primitive notions only, without defined notions. It also made a clear distinction between full geometry and its elementary (first-order) part. Unlike other modern axiomatizations such as Birkhoff's and Hilbert's, Tarski's has no primitive objects other than points, so variables or constants cannot refer to lines or angles. The only primitive relations are betweenness and congruence among points. Tarski designed his system to facilitate analysis via mathematical logic, and it has the unusual property that all sentences can be written in universal-existential form, allowing him to prove that Euclidean geometry is decidable.

Reader's Guide

Tarski's axioms are significant because they provided the first complete and decidable first-order axiomatization of Euclidean geometry. This achievement does not contradict Gödel's first incompleteness theorem, because Tarski's theory lacks the expressive power needed to interpret Robinson arithmetic. The system's economy of primitive notions—only points, betweenness, and congruence—makes it less convenient for doing geometry but ideal for metamathematical analysis. Tarski's work culminated in the monograph by Schwabhäuser, Szmielew, and Tarski (1983), which set out 10 axioms and one axiom schema, along with associated metamathematics. The system's completeness means every sentence in its language is either provable or disprovable from the axioms, and its decidability means an algorithm can determine truth or falsity of any sentence. This work built on earlier efforts by Pieri, Hilbert, and Birkhoff, but Tarski's approach was distinguished by its logical transparency and its focus on elementary (first-order) geometry.

Did You Know?

• Tarski's axioms use only points as primitive objects, with no variables for lines or angles.
• The system contains infinitely many axioms, though the final version has 10 axioms and one axiom schema.
• Tarski's system is complete and decidable, meaning an algorithm can determine the truth of any sentence.
• The length of all Tarski's axioms together is not much more than just one of Pieri's 24 axioms.