<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

Publicado en línea: 28 mar 2018

Páginas: 289 - 313

Recibido: 29 nov 2017

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

Palabras clave
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

Publicado en línea: 28 mar 2018

Páginas: 289 - 313

Recibido: 29 nov 2017

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

Palabras claveTarski’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.

Palabras clave
Tarski’s geometry axioms, foundations of geometry, Euclidean plane