Towards an Independent Version of Tarski's System of Geometry - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2024

Towards an Independent Version of Tarski's System of Geometry

Stéphane Kastenbaum
  • Fonction : Auteur
  • PersonId : 1108704
Clément Saintier
  • Fonction : Auteur
  • PersonId : 1320155

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (321.36 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
licence : Domaine public

Dates et versions

hal-04324071 , version 1 (04-01-2024)

Identifiants

Citer

Pierre Boutry, Stéphane Kastenbaum, Clément Saintier. Towards an Independent Version of Tarski's System of Geometry. 14th International Conference on Automated Deduction in Geometry, Sep 2023, Belgrade, Serbia. pp.73-84, ⟨10.4204/EPTCS.398.11⟩. ⟨hal-04324071⟩
33 Consultations
7 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More