<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (“Satz”) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).</p></abstract>

In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (“Satz”) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).

Tarski Geometry Axioms. Part III

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

{"article-title":"Tarski Geometry Axioms. Part III"}

In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W....

Tarski Geometry Axioms. Part III

Publié en ligne: 28 mars 2018

Pages: 289 - 313

Reçu: 29 nov. 2017

DOI: https://doi.org/10.1515/forma-2017-0028

Mots clés
Tarski’s geometry axioms, foundations of geometry, Euclidean plane

© by Roland Coghetto

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Tarski Geometry Axioms. Part III

Publié en ligne: 28 mars 2018

Pages: 289 - 313

Reçu: 29 nov. 2017

DOI: https://doi.org/10.1515/forma-2017-0028

Mots clésTarski’s geometry axioms, foundations of geometry, Euclidean plane

© by Roland Coghetto

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.

Mots clés
Tarski’s geometry axioms, foundations of geometry, Euclidean plane