<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

Published Online: Mar 28, 2018

Page range: 289 - 313

Received: Nov 29, 2017

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

Keywords
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

Published Online: Mar 28, 2018

Page range: 289 - 313

Received: Nov 29, 2017

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

KeywordsTarski’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.

Keywords
Tarski’s geometry axioms, foundations of geometry, Euclidean plane