<abstract xmlns="http://www.w3.org/1999/xhtml">In our earlier article <xref ref-type="bibr" rid="j_forma-2016-0012_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa">[12]</xref>, the first part of axioms of geometry proposed by Alfred Tarski <xref ref-type="bibr" rid="j_forma-2016-0012_ref_014_w2aab2b8b1b1b7b1ab1ac14Aa">[14]</xref> was formally introduced by means of Mizar proof assistant <xref ref-type="bibr" rid="j_forma-2016-0012_ref_009_w2aab2b8b1b1b7b1ab1ab9Aa">[9]</xref>. We defined a structure <monospace>TarskiPlane</monospace> with the following predicates:
<list list-type="bullet"><list-item>of betweenness <monospace>between</monospace> (a ternary relation),</list-item><list-item>of congruence of segments <monospace>equiv</monospace> (quarternary relation),</list-item></list>
which satisfy the following properties:
<list list-type="bullet"><list-item>congruence symmetry (A1),</list-item><list-item>congruence equivalence relation (A2),</list-item><list-item>congruence identity (A3),</list-item><list-item>segment construction (A4),</list-item><list-item>SAS (A5),</list-item><list-item>betweenness identity (A6),</list-item><list-item>Pasch (A7).</list-item></list>
Also a simple model, which satisfies these axioms, was previously constructed, and described in <xref ref-type="bibr" rid="j_forma-2016-0012_ref_006_w2aab2b8b1b1b7b1ab1ab6Aa">[6]</xref>. In this paper, we deal with four remaining axioms, namely:
<list list-type="bullet"><list-item>the lower dimension axiom (A8),</list-item><list-item>the upper dimension axiom (A9),</list-item><list-item>the Euclid axiom (A10),</list-item><list-item>the continuity axiom (A11).</list-item></list>
They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles <monospace>cong</monospace> is introduced via congruence of sides (SSS).In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural <xref ref-type="bibr" rid="j_forma-2016-0012_ref_005_w2aab2b8b1b1b7b1ab1ab5Aa">[5]</xref> extension of ordinary metric structure <monospace>Euclid 2</monospace> satisfies all these attributes.Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq <xref ref-type="bibr" rid="j_forma-2016-0012_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa">[11]</xref>, first approaches to this topic were done in Mizar in 1990 <xref ref-type="bibr" rid="j_forma-2016-0012_ref_016_w2aab2b8b1b1b7b1ab1ac16Aa">[16]</xref> (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time <xref ref-type="bibr" rid="j_forma-2016-0012_ref_008_w2aab2b8b1b1b7b1ab1ab8Aa">[8]</xref>). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle <xref ref-type="bibr" rid="j_forma-2016-0012_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa">[10]</xref> clarified things a bit. Our development allows for the future faithful mechanization of <xref ref-type="bibr" rid="j_forma-2016-0012_ref_013_w2aab2b8b1b1b7b1ab1ac13Aa">[13]</xref> and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory <xref ref-type="bibr" rid="j_forma-2016-0012_ref_007_w2aab2b8b1b1b7b1ab1ab7Aa">[7]</xref>.</abstract>

In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates:
of betweenness between (a ternary relation),of congruence of segments equiv (quarternary relation),
which satisfy the following properties:
congruence symmetry (A1),congruence equivalence relation (A2),congruence identity (A3),segment construction (A4),SAS (A5),betweenness identity (A6),Pasch (A7).
Also a simple model, which satisfies these axioms, was previously constructed, and described in [6]. In this paper, we deal with four remaining axioms, namely:
the lower dimension axiom (A8),the upper dimension axiom (A9),the Euclid axiom (A10),the continuity axiom (A11).
They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles cong is introduced via congruence of sides (SSS).In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure Euclid 2 satisfies all these attributes.Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].

Tarski Geometry Axioms – Part II

Rue de la Brasserie 5, 7100 La Louvière,

Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok,

Formalized Mathematics

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

{"article-title":"Tarski Geometry Axioms \u2013 Part II"}

In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]....

Tarski Geometry Axioms – Part II

Pubblicato online: 08 dic 2016

Pagine: 157 - 166

Ricevuto: 30 giu 2016

DOI: https://doi.org/10.1515/forma-2016-0012

Parole chiave
Tarski’s geometry axioms, foundations of geometry, Euclidean plane

© 2016 Roland Coghetto et al., published by De Gruyter Open

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

Tarski Geometry Axioms – Part II

Pubblicato online: 08 dic 2016

Pagine: 157 - 166

Ricevuto: 30 giu 2016

DOI: https://doi.org/10.1515/forma-2016-0012

Parole chiaveTarski’s geometry axioms, foundations of geometry, Euclidean plane

© 2016 Roland Coghetto et al., published by De Gruyter Open

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

Parole chiave
Tarski’s geometry axioms, foundations of geometry, Euclidean plane