Tarski Geometry Axioms – Part II

In our earlier article, the first part of axioms of geometry proposed by Alfred Tarskiwas formally introduced by means of Mizar proof assistant. We defined a structurewith the following predicates:which satisfy the following properties:Also a simple model, which satisfies these axioms, was previously constructed, and described in. In this paper, we deal with four remaining axioms, namely:They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of trianglesis introduced via congruence of sides (SSS). [12] [14] [9] [6] TarskiPlane cong

of betweenness(a ternary relation), between

of congruence of segments(quarternary relation), equiv

congruence symmetry (A1),

congruence equivalence relation (A2),

congruence identity (A3),

segment construction (A4),

SAS (A5),

betweenness identity (A6),

Pasch (A7).

the lower dimension axiom (A8),

the upper dimension axiom (A9),

the Euclid axiom (A10),

the continuity axiom (A11).

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 naturalextension of ordinary metric structuresatisfies all these attributes. [5] Euclid 2

Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq, first approaches to this topic were done in Mizar in 1990(even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time). 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 Isabelleclarified things a bit. Our development allows for the future faithful mechanization ofand opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory. [11] [16] [8] [10] [13] [7]