Tarski axioms of Euclidean geometry

Abstract

Tarského axiomatizace geometrie je prvořádovou teorií elementární eukleidovské geo- metrie. Věnujeme se axiomatické výstavbě geometrie uvnitř této teorie až k výstavbě alge- braického tělesa uvnitř geometrického prostoru, následujeme tak Schwabhäusera, Szmie- lew a Tarského, výstabu provádíme obdobně jako Hilbert. Teorie reálně uzavřených těles (RCF) je představena jako vhodná algebraická struktura pro zkoumání geometrie. V práci je ukázáno, že teorie RCF má eliminaci kvantifikátorů, z čehož vyvozujeme rozhod- nutelnost a úplnost této teorie. Užitím Tarského věty o reprezentaci můžeme výsledky o rozhodnutelnosti a úplnosti přenést i na Tarského axiomatizaci.

Tarski's axioms of geometry are a first-order axiomatization of elementary Euclidean geometry. Following Schwabhäuser, Szmielew and Tarski, and similarly to Hilbert, the axiomatic development of geometry inside the theory is explored, up to building an alge- braic field inside a geometric space. The theory of real-closed fields (RCF) is introduced as a suitable algebraic structure for studying geometry. We prove that RCF has elimina- tion of quantifiers, thus its decidability and completeness can be established. Using the Tarski's representation theorem, decidability and completeness then applies for Tarski's axiomatization as well.