Towards an Independent Version of Tarski's System of Geometry

Pierre Boutry
(Centre Inria d'Université Côte d'Azur, Sophia Antipolis, France)
Stéphane Kastenbaum
Clément Saintier

In 1926–1927, Tarski designed a set of axioms for Euclidean geometry which reached its final form in a manuscript by Schwabhä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 the parallel postulate differ.

In this paper, we present our progress towards obtaining an independent version of a variant of Gupta's system. Compared to Gupta's version, we split Pasch's axiom into this previously eliminated axiom and its non-degenerate part and change the statement of the parallel postulate. We verified the independence properties by mechanizing counter-models using the Coq proof-assistant.

In Pedro Quaresma and Zoltán Kovács: Proceedings 14th International Conference on Automated Deduction in Geometry (ADG 2023), Belgrade, Serbia, 20-22th September 2023, Electronic Proceedings in Theoretical Computer Science 398, pp. 73–84.
Published: 22nd January 2024.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: