<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.</p><p>We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during <italic>Tarski Formalization Project</italic> by M. Beeson (the so-called Section 8A of SST).</p></abstract>

In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).

Tarski Geometry Axioms. Part IV – Right Angle

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

{"article-title":"Tarski Geometry Axioms. Part IV \u2013 Right Angle"}

In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for...

Tarski Geometry Axioms. Part IV – Right Angle

Data publikacji: 16 maj 2019

Zakres stron: 75 - 85

Przyjęty: 11 mar 2019

DOI: https://doi.org/10.2478/forma-2019-0008

Słowa kluczowe
Tarski geometry, foundations of geometry, right angle

© 2019 Roland Coghetto et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Tarski Geometry Axioms. Part IV – Right Angle

Data publikacji: 16 maj 2019

Zakres stron: 75 - 85

Przyjęty: 11 mar 2019

DOI: https://doi.org/10.2478/forma-2019-0008

Słowa kluczoweTarski geometry, foundations of geometry, right angle

© 2019 Roland Coghetto et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 Public License.

Słowa kluczowe
Tarski geometry, foundations of geometry, right angle