Towards an Independent Version of Tarski's System of Geometry
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910304718290944 |
|---|---|
| author | Boutry, Pierre Kastenbaum, Stéphane Saintier, Clément |
| author_facet | Boutry, Pierre Kastenbaum, Stéphane Saintier, Clément |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_11904 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards an Independent Version of Tarski's System of Geometry Boutry, Pierre Kastenbaum, Stéphane Saintier, Clément Logic in Computer Science F4 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. |
| title | Towards an Independent Version of Tarski's System of Geometry |
| topic | Logic in Computer Science F4 |
| url | https://arxiv.org/abs/2401.11904 |