Skip to Main content Skip to Navigation
Conference papers

From Hilbert to Tarski

Abstract : In this paper, we describe the formal proof using the Coq proof assistant that Tarski's axioms for plane neutral geometry (excluding continuity axioms) can be derived from the corresponding Hilbert's axioms. Previously, we mechanized the proof that Tarski's version of the parallel postulate is equivalent to the Playfair's postulate used by Hilbert [9] and that Hilbert's axioms for plane neutral geometry (excluding continuity) can be derived from the corresponding Tarski's axioms [12]. Hence, this work allows us to complete the formal proof of the equivalence between the two axiom systems for neutral and plane Euclidean geometry. Formalizing Hilbert's axioms is not completely straightforward, in this paper we describe the corrections we had to make to our previous formalization. We mechanized the proof of Hilbert's theorems that are required in our proof of Tarski's axioms. But this connection from Hilbert's axioms, allows to recover the many results we obtained previously in the context of Tarski's geometry: this includes the theorems of Pappus[13], Desargues, Pythagoras and the arithmetiza-tion of geometry [8].
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/hal-01332044
Contributor : Julien Narboux <>
Submitted on : Wednesday, June 15, 2016 - 10:42:47 AM
Last modification on : Saturday, October 27, 2018 - 1:23:48 AM
Long-term archiving on: : Friday, September 16, 2016 - 10:12:08 AM

File

hilbert_to_tarski.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01332044, version 1

Citation

Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19. ⟨hal-01332044⟩

Share

Metrics

Record views

400

Files downloads

1299