Metamath Proof Explorer

Table of Contents - 15. ELEMENTARY GEOMETRY

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, 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 the definitions df-trkg et sequentes). This allows us 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

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.

  1. Definition and Tarski's Axioms of Geometry
    1. cstrkg
    2. cstrkgc
    3. cstrkgb
    4. cstrkgcb
    5. cstrkgld
    6. cstrkge
    7. citv
    8. clng
    9. df-itv
    10. df-lng
    11. itvndx
    12. lngndx
    13. itvid
    14. lngid
    15. trkgstr
    16. trkgbas
    17. trkgdist
    18. trkgitv
    19. df-trkgc
    20. df-trkgb
    21. df-trkgcb
    22. df-trkge
    23. df-trkgld
    24. df-trkg
    25. istrkgc
    26. istrkgb
    27. istrkgcb
    28. istrkge
    29. istrkgl
    30. istrkgld
    31. istrkg2ld
    32. istrkg3ld
    33. axtgcgrrflx
    34. axtgcgrid
    35. axtgsegcon
    36. axtg5seg
    37. axtgbtwnid
    38. axtgpasch
    39. axtgcont1
    40. axtgcont
    41. axtglowdim2
    42. axtgupdim2
    43. axtgeucl
    44. Justification for the congruence notation
  2. Tarskian Geometry
    1. Congruence
    2. Dimension
    3. Betweenness and Congruence
    4. Congruence of a series of points
    5. Motions
    6. Colinearity
    7. Connectivity of betweenness
    8. Less-than relation in geometric congruences
    9. Rays
    10. Lines
    11. Point inversions
    12. Right angles
    13. Half-planes
    14. Midpoints and Line Mirroring
    15. Congruence of angles
    16. Angle Comparisons
    17. Congruence Theorems
    18. Equilateral triangles
  3. Properties of geometries
    1. Isomorphisms between geometries
  4. Geometry in Hilbert spaces
    1. cttg
    2. df-ttg
    3. ttgval
    4. ttglem
    5. ttgbas
    6. ttgplusg
    7. ttgsub
    8. ttgvsca
    9. ttgds
    10. ttgitvval
    11. ttgelitv
    12. ttgbtwnid
    13. ttgcontlem1
    14. xmstrkgc
    15. Geometry in the complex plane
    16. Geometry in Euclidean spaces