Tarski Geometry Axioms

William Richter; Adam Grabowski; Jesse Alama

Formalized Mathematics (2014)

  • Volume: 22, Issue: 2, page 167-176
  • ISSN: 1426-2630

Abstract

top
This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.

How to cite

top

William Richter, Adam Grabowski, and Jesse Alama. "Tarski Geometry Axioms." Formalized Mathematics 22.2 (2014): 167-176. <http://eudml.org/doc/268727>.

@article{WilliamRichter2014,
abstract = {This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.},
author = {William Richter, Adam Grabowski, Jesse Alama},
journal = {Formalized Mathematics},
keywords = {Tarski’s geometry axioms; foundations of geometry; incidence geometry},
language = {eng},
number = {2},
pages = {167-176},
title = {Tarski Geometry Axioms},
url = {http://eudml.org/doc/268727},
volume = {22},
year = {2014},
}

TY - JOUR
AU - William Richter
AU - Adam Grabowski
AU - Jesse Alama
TI - Tarski Geometry Axioms
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 2
SP - 167
EP - 176
AB - This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.
LA - eng
KW - Tarski’s geometry axioms; foundations of geometry; incidence geometry
UR - http://eudml.org/doc/268727
ER -

References

top
  1. [1] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  2. [2] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  3. [3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  4. [4] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  5. [5] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990. 
  6. [6] Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In F. Botana and T. Recio, editors, Automated Deduction in Geometry, volume 4869, pages 139–156, 2007. Zbl1195.03019
  7. [7] Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983. Zbl1237.51003
  8. [8] Alfred Tarski and Steven Givant. Tarski’s system of geometry. Bulletin of Symbolic Logic, 5(2):175–214, 1999. 
  9. [9] Wojciech A. Trybulec. Axioms of incidence. Formalized Mathematics, 1(1):205–213, 1990. 
  10. [10] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  11. [11] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. Received June 16, 2014 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.