Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards an Independent Version of Tarski's System of Geometry

Pierre Boutry, Stéphane Kastenbaum, Clément Saintier

TL;DR

The paper investigates independence phenomena in a variant of Gupta's adaptation of Tarski's system of planar geometry, splitting Pasch's axiom into a non-degenerate part and betweenness symmetry while adjusting the parallel postulate. It employs Coq to mechanize and verify counter-models, demonstrating equivalence to Tarski's original system and producing a concrete model on Cartesian planes over a real field, aided by a real-closed-field axiom. A Klein model is used to exhibit the independence of Euclid's parallel postulate within this framework, with ten of eleven counter-models formalized and four key axioms analyzed in detail. The results illustrate that small changes in axiom statements can alter model satisfaction and pave the way for higher-dimensional extensions and constructive treatments, underscoring the value of proof assistants in geometry independence results.

Abstract

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.

Towards an Independent Version of Tarski's System of Geometry

TL;DR

The paper investigates independence phenomena in a variant of Gupta's adaptation of Tarski's system of planar geometry, splitting Pasch's axiom into a non-degenerate part and betweenness symmetry while adjusting the parallel postulate. It employs Coq to mechanize and verify counter-models, demonstrating equivalence to Tarski's original system and producing a concrete model on Cartesian planes over a real field, aided by a real-closed-field axiom. A Klein model is used to exhibit the independence of Euclid's parallel postulate within this framework, with ten of eleven counter-models formalized and four key axioms analyzed in detail. The results illustrate that small changes in axiom statements can alter model satisfaction and pave the way for higher-dimensional extensions and constructive treatments, underscoring the value of proof assistants in geometry independence results.

Abstract

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.
Paper Structure (13 sections, 1 theorem, 6 equations, 3 tables)

This paper contains 13 sections, 1 theorem, 6 equations, 3 tables.

Table of Contents

  1. Introduction
  2. A Variant of Tarski's System of Geometry
  3. Tarski's System of Geometry
  4. Gupta's Contribution
  5. An Independent System for Planar Geometry
  6. A model of Tarski's system of geometry
  7. The Real Field Structure
  8. The Model
  9. Proof that the Axioms hold in the Model
  10. An Example of Independence Proof
  11. Klein's Model
  12. Independence of Euclid’s Parallel Postulate via Klein's Model
  13. Conclusion

Key Result

Theorem 1

Axiom A10' does not hold in Klein's model.

Theorems & Definitions (2)

  • Theorem 1
  • proof