Towards an Independent Version ofTarski's System of Geometry

In 1926-1927, Tarski designed a set of axioms for Euclidean geometry which reached its final formin a manuscript by Schwabh & auml;user, Szmielew and Tarski in 1983. The differences amount to simplifications obtained by Tarski and Gupta. Gupta presented an independent version of Tarski's system of geometry, thus establishing that his version could not be further simplified without modifying the axioms. To obtain the independence of one of his axioms, namely Pasch's axiom, he proved the independence of one of its consequences: the previously eliminated symmetry of betweenness. However, an independence model for the non-degenerate part of Pasch's axiom was provided by Szczerba for another version of Tarski's system of geometry in which the symmetry of betweenness holds. This independence proof cannot be directly used for Gupta's version as the statements of theparallel postulate differ. In this paper, we present our progress towards obtaining an independent version of a variant ofGupta's system. Compared to Gupta's version, we split Pasch's axiom into this previously eliminatedaxiom and its non-degenerate part and change the statement of the parallel postulate. We verified theindependence properties by mechanizing counter-models using the Coq proof-assistant