This part develops elementary geometry based on Tarski's axioms, following [Schwabhauser]. Tarski's geometry is a first-order theory with one sort, the "points". It has two primitive notions, the ternary predicate of "betweenness" and the quaternary predicate of "congruence". To adapt this theory to the framework of set.mm, and to be able to talk of *a* Tarski structure as a space satisfying the given axioms, we use the following definition, stated informally:
A Tarski structure is a set (of points) together with functions and on satisfying certain axioms (given in Definitions df-trkg et sequentes). This allows to treat a Tarski structure as a special kind of extensible structure (see df-struct).
The translation to and from Tarski's treatment is as follows (given, again, informally).
Suppose that one is given an extensible structure . One defines a betweenness ternary predicate Btw by positing that, for any , one has "Btw " if and only if , and a congruence quaternary predicate Congr by positing that, for any , one has "Congr " if and only if . It is easy to check that if satisfies our Tarski axioms, then Btw and Congr satisfy Tarski's Tarski axioms when is interpreted as the universe of discourse.
Conversely, suppose that one is given a set , a ternary predicate Btw, and a quaternary predicate Congr. One defines the extensible structure such that is , and is the function which associates with each the set of points such that "Btw ", and is the function which associates with each the set of ordered pairs such that "Congr ". It is easy to check that if Btw and Congr satisfy Tarski's Tarski axioms when is interpreted as the universe of discourse, then satisfies our Tarski axioms.
We intentionally choose to represent congruence (without loss of generality) as instead of "Congr ", as it is more convenient. It is always possible to define for any particular geometry to produce equal results when conguence is desired, and in many cases there is an obvious interpretation of "distance" between two points that can be useful in other situations. Encoding congruence as an equality of distances makes it easier to use these theorems in cases where there is a preferred distance function. We prove that representing a congruence relationship using a distance in the form causes no loss of generality in tgjustc1 and tgjustc2, which in turn are supported by tgjustf and tgjustr.
A similar representation of congruence (using a "distance" function) is used in Axiom A1 of [Beeson2016] p. 5, which discusses how a large number of formalized proofs were found in Tarskian Geometry using OTTER. Their detailed proofs in Tarski Geometry, along with other information, are available at https://www.michaelbeeson.com/research/FormalTarski/.
Most theorems are in deduction form, as this is a very general, simple, and convenient format to use in Metamath. An assertion in deduction form can be easily converted into an assertion in inference form (removing the antecedents ) by insert a in each hypothesis, using a1i, then using mptru to remove the final prefix. In some cases we represent, without loss of generality, an implication antecedent in [Schwabhauser] as a hypothesis. The implication can be retrieved from the by using simpr, the theorem as stated, and ex.
For descriptions of individual axioms, we refer to the specific definitions below. A particular feature of Tarski's axioms is modularity, so by using various subsets of the set of axioms, we can define the classes of "absolute dimensionless Tarski structures" (df-trkg), of "Euclidean dimensionless Tarski structures" (df-trkge) and of "Tarski structures of dimension no less than N" (df-trkgld).
In this system, angles are not a primitive notion, but instead a derived notion (see df-cgra and iscgra). To maintain its simplicity, in this system congruence between shapes (a finite sequence of points) is the case where corresponding segments between all corresponding points are congruent. This includes triangles (a shape of 3 distinct points). Note that this definition has no direct regard for angles. For more details and rationale, see df-cgrg.
The first section is devoted to the definitions of these various structures. The second section ("Tarskian geometry") develops the synthetic treatment of geometry. The remaining sections prove that real Euclidean spaces and complex Hilbert spaces, with intended interpretations, are Euclidean Tarski structures.
Most of the work in this part is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. See also the credits in the comment of each statement.