We discuss the formal approach to Tarski geometry axioms modelled with the help of the Mizar computerized proof assistant system. We try however to go much further from the use of simple predicates in the direction of the use of structures with their inheritance, attributes as a tool of more human-friendly namespaces for axioms, and registrations of clusters to obtain more automation (with the possible use of external equational theorem provers like Otter/Prover9). The formal proof that Euclidean plane satis es all eleven axioms proposed by Tarski is an essential development, allowing to show the independence of the parallel postulate, one of the items from \Top 100 mathematical theorems".
ne Geometry In Tarski's system of axioms [TG99] the only primitive geometrical notions are points, the ternary relation B of \soft betweenness" and quaternary relation of \equidistance" or \congruence of segments". The axioms are re exivity, transitivity, and identity axioms for equidistance; the axiom of segment construction; re exivity, symmetry, inner and outer transitivity axioms for betweenness; the axiom of continuity, and some others. The original set consisted of 20 axioms for two-dimensional Euclidean geometry and was constructed in 1926{27, submitted for publication in 1940, and nally appeared in 1967 in a limited number of copies. There are many modi cations of this system, and Gupta's work in this area [Gup65] o ers an important simpli cation.
Another notable axiomatization, proposed by Hilbert [Hil80] in 1899, has three sorts: planes, points, and lines, and three relations: betweenness, containment, and congruence. In this sense it is a little bit more complex than Tarski's (but not necessarily in terms of numbers of axioms as it has also 20 of these). The two approaches establish a geometrical framework, in which theorems can be proven logically (remember Euclid's Elements proofs are mainly pictures or graphical constructions and rely heavily on intuition). This allows to use computerized theorem prover in order to nd the proof or proof checker to check the theory for its correctness. We deal with the proof checker Mizar based on classical rst order logic and Tarski-Grothendieck set theory (a variant of Zermelo-Fraenkel) and describe, how Tarski's theory was built formally.
Geometry in the Mizar Mathematical Library is based on eight various structures, so it raises communication issues between various approaches. The last article was PROJPL_1 dated back to 1994, and the series was not very actively developed (with the exception of the paper of the combinatorial Grassmanians COMBGRAS). But in 1990 Mizar articles on geometry were about 30% of the whole Mizar repository (out of 140 les). Of course, after that time revisions of this speci c area were quite active: one of the main streams (done also by the current author) was to get separate axioms of selected properties instead of a large block for the mode (i.e. the constructor of the type in Mizar). A ne approach to geometry was less important as there was another big challenge which for fteen years stimulated geometry (in analytical setting, however): the proof of the Jordan Curve Theorem.
As notable a ne geometrical facts already formalized in Mizar we can enumerate:
Hessenberg's theorem { HESSENBE; Desargues theorem (present in \Top 100 mathematical theorems") { ANPROJ_2; Pasch con guration axioms { PASCH; Fano projective spaces { PROJRED1; Desarguesian projective planes { PROJRED2; Pappus, Minor, Major and Trapezium Desargues axioms { AFF_2;
Minkowskian geometry { ANALORT.
In our opinion, the uni ying approach in Tarski's spirit could be quite useful to bind all of these geometrical results together. Among another signi cant facts in geometry we can point out Morley trisector theorem, Ceva, and Menelaus theorem. These facts however deal with Euclidean plane, so the proofs are in the area of analytic geometry; they were developed more than ten years later than the foundations of geometry in Mizar, when Euclidean spaces were more thoroughly explored in MML.
The distinction between classical and abstract mathematics (i.e. the one based on ordinary axioms of set theory, and all those using the notion of a structure, respectively) is important from the viewpoint of the organization of the Mizar repository. We had to choose between two paths: it is possible to formulate Tarski's axioms without the use of a structure, and also set theory could be meaningless for that framework, only the classical logic with Mizar predicates is enough; the use of Mizar structures forces us paradoxically to use fundamentals of set theory { de ning a signature of Tarski's plane needed to give a type of congruence of segments and betweenness relation, which was set-theoretic (Mizar language is typed, and it the earlier case one should also give a type at least to points, but it can be de ned as Mizar object).
The latter was also chosen by us as the whole geometry in MML is written in abstract style (as the majority of MML) as structures in Mizar are present for a long time. Even if in ordinary mathematical tradition they are considered as ordered tuples, in the implementation in Mizar they are treated rather as partial functions, with selectors as arguments, and ordinary inheritance mechanism (with polymorphic enabled, which will be extensively used in our formalizations). definition struct (1-sorted) TarskiPlane (# carrier -> set, Betweenness -> Relation of [:the carrier, the carrier:], the carrier,
Equidistance -> Relation of [:the carrier, the carrier:], [:the carrier, the carrier:] #);
The betweenness relation can be treated as a ternary relation, but the choice of this concrete model was quite arbitrary as the di erence between dealing with ternary relations and relations between ordered pairs and elements will not cause any major problems later (we use mainly predicates). Then we can use a type POINT of S just for elements of structures S, and predicates between a,b,c and a,b equiv c,d as [[a,b],c] in the Betweenness of S and [[a,b],[c,d]] in the Equidistance of S, respectively. 3
Original version of Mizar formalization of Tarski's axioms done by William Richter with the help of miz3 did not contained any existence proofs. This essentially caused the lack of the appropriate Mizar type. By using attributes instead of predicates we can have modular building of a complex structure, all other can be reused; hence in our Mizar article we focus on pure betweenness-equidistance part, not really mentioning the question of dimensions. We proved 44 theorems (properties of the predicates), with the Gupta's proof of Hilbert's I1 axiom (that two distinct points determine a line).
Our Mizar versions of Tarski's axioms have descriptive names, and follow the ones from SST (using for congruence of segments and B for betweenness relation): 8a;b ab CongruenceSymmetry (A1):
ba,
8a;b;p;q;r;s ab pq ^ ab rs ) pq rs,
8a;b;c ab cc ) a = b, 8a;q;b;c9x B(q; a; x) ^ ax SegmentConstruction (A4): bc,
8a;b B(a; b; a) ) a = b, and Pasch (A7): 8a;b;p;q;z B(a; p; z) ^ B(p; q; z) ) 9x B(p; x; b) ^ B(q; x; a).
One attribute has the form which substantially di ers from SST version: in order to shorten the notation, we introduced technical predicate definition let S be TarskiPlane; let a, b, c, x, y, z be POINT of S; pred a,b,c cong x,y,z means :: GTARSKI1:def 3
a,b equiv x,y & a,c equiv x,z & b,c equiv y,z; end; definition let S be TarskiPlane; attr S is satisfying_SAS means :: GTARSKI1:def 9 for a, b, c, x, a1, b1, c1, x1 being POINT of S holds a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 implies c,x equiv c1,x1; end; that is, denoting essentially SSS predicate for triangles. Using this notion, SST axiom (A5) could be encoded as follows: 8a;b;c;x;a0;b0;c0;x0 (a 6= b ^ ab a0b0 ^ bc b0c0 ^ ac
a0c0 ^ ^ B(a; b; x) ^ B(a0; b0; x0) ^ bx b0x0) ) cx c0x0:
Having separate attributes for distinct axioms could had already shown its usefulness in various geemetrical settings. It could also allow later for de ning equivalent axiom systems for Tarski geometry (and due to mechanism of clusters this equivalence will be obvious for the checker, once proven). But also additional attribute, satisfying_Tarski-model, was de ned as a shorthand for the above seven axioms.
It is well known fact that every metric space can be equipped with the natural topology. This informally obvious mathematical property brings some unexpected di culties when dealing with structures if automated proofassistants play a role. Namely then, if one considers topological spaces in a quite natural way, that is hU; i; and metric space as hU; di; respectively, one can rather naturally merge both structures into common hU; ; di:
During the formalization of the Jordan Curve Theorem in Mizar, however, another approach was chosen (and pushed consequently until the successful nale): Euclid 2 denoted metric space concerned with the Euclidean plane, and then special functor converting any metric space into the topoogical space was applied to obtain TOP-REAL 2 (of course the conversion can be made for arbitrary natural number n, not necessarily 2, but Jordan curves deal with two-dimensional case). The basic signature for metric spaces are MetrStruct, where distance is a function de ned on the Cartesian square of the carrier with the real values. Then, metrics (or pseudo-, quasi-, semimetrics, etc.) can be de ned in terms of attributes [KLS90], that is properties of the distance function. definition struct (MetrStruct,TarskiPlane) MetrTarskiStr (# carrier -> set, distance -> Function of [:the carrier, the carrier:], REAL, Betweenness -> Relation of [:the carrier, the carrier:], the carrier,
Equidistance -> Relation of [:the carrier, the carrier:], [:the carrier, the carrier:] #);
Then we have two worlds merged: a ne, where we have two Tarski's relations, and Euclidean, where in terms of distance function, we can have betweenness relation and the the measure for segments. We argue that, regardless of all the complications caused by merging structures (which increases the number of selectors, hence the chain of notions gets more complicated), such approach { not converting between two contexts, but rather to make reasoning in the world which is successor of both { allows for more exible reuse of knowledge from two original areas. definition let M be MetrTarskiStr; attr M is naturally_generated means :: GTARSKI1:def 15 (for a, b, c being POINT of M holds between a,b,c iff b is_Between a,c) & (for a, b, c, d being POINT of M holds a,b equiv c,d iff dist (a,b) = dist (c,d));
In merged structure, we want to have two segments congruent, if they are equal in terms of distance, and betweenness relation uses the predicate is_Between, also given in terms of the sum of distances.
Recalling the previous discussion on the structure merging, the construction of such a space from scratch (essentially more or less modi ed copy-and-paste work on the proof from [Try90]) can be avoided with the help of some useful tricks, investigating knowledge already present in MML with its possible reuse. For example, based on the geometry on the real line, appropriate geometrical structure from metric structure can be just an extension with properly de ned distance. definition func TarskiSpace -> MetrTarskiStr equals :: GTARSKI1:def 22
the naturally_generated TarskiExtension of RealSpace; coherence; end;
Then, we can show that in such extension the metric is well de ned, i.e. this space is re exive, symmetric, and discerning. Furthermore, if we take into account \geometrical part", all newly introduced Tarski's axioms are true. 5
At the beginning, we had to construct an example of the structure which satis es all these axioms. definition let n be Nat; func TarskiEuclidSpace n -> MetrTarskiStr equals
the naturally_generated TarskiExtension of Euclid n; :: GTARSKI2:def 1 and TarskiEuclid2Space is just the shorthand for the above functor with n = 2.
First part of the work, which was rather easy, was to show that such Euclidean plane satis es seven axioms from [RGA14]. It was expressed in terms of cluster registration: registration cluster TarskiEuclid2Space -> satisfying_Tarski-model; coherence; end;
Then, we de ned the remaining four axioms, with both descriptive names and those corresponding to SST namespace, as follows: notation let S be TarskiPlane; synonym S is satisfying_Lower_Dimension_Axiom for S is satisfying_A8; synonym S is satisfying_Upper_Dimension_Axiom for S is satisfying_A9; synonym S is satisfying_Euclid_Axiom for S is satisfying_A10; synonym S is satisfying_Continuity_Axiom for S is satisfying_A11; end;
Of course, their meaning is just as in SST. Then, nally we can deal with the remaining axioms: registration cluster TarskiEuclid2Space -> satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom satisfying_Euclid_Axiom satisfying_Continuity_Axiom; end;
Some of the proofs were proven based on the space with the dimension 2 (mainly those done by the second author), in few places we used Isabelle development and gave our Mizar proofs accordingly. The summary of formalizations in two Mizar les can be found in Table 2. 6
Although the history of the development of the axiom system for geometry by Tarski is not very clear from the beginnings (as the early works by Tarski seem to be postponed by the World War II), and even if the ultimate source of information is
The book by Schwabhauser, Szmielew and Tarski, reissued with the foreword of Michael Beeson, attracted recently a lot of focus from automated deduction systems. The remarkable item here is of course Narboux's formal development of Tarski's system with the use of Coq [Nar07]. We are planning to include some interesting results from GeoCoq in the Mizar system; Nakasho's et al. MML symbol reference system1 o ers quite userfriendly interface for browsing appropriate content. Of course, GeoCoq provides ready-to-use list of notions, which are connected only with the Tarski's system { that makes the browsing more convenient. Of course, after rescaling all de nitions and theorems can be browsed within MML providing a look in the style of GeoCoq project.
We have created in [RGA14] (and GTARSKI2 [CG16]) complete formal axiomatization of Tarski's geometry which, at least in our opinion, has the advantage of higher readability for ordinary mathematicians than e.g. Coq or Prover9 proof objects. In the same it is tightly connected with another axiomatization of Euclidean plane, due to Hilbert, already available in MML. Important part of our development was the proof that the real Euclidean plane satis es all Tarski's axioms.
1The system can be browsed at http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/ with the o cial version of the Mizar system. [Gra14] Grabowski A.: E cient rough set theory merging, Fundamenta Informaticae, 135(4), pp. 371{385 (2014) [Wie12] Wiedijk F.: A synthesis of the procedural and declarative styles of interactive theorem proving, Logical Methods in Computer Science, 8(1):30 (2012)