Metamath Proof Explorer


Table of Contents - 16. 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 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.

  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. slotsinbpsd
    16. slotslnbpsd
    17. lngndxnitvndx
    18. trkgstr
    19. trkgbas
    20. trkgdist
    21. trkgitv
    22. df-trkgc
    23. df-trkgb
    24. df-trkgcb
    25. df-trkge
    26. df-trkgld
    27. df-trkg
    28. istrkgc
    29. istrkgb
    30. istrkgcb
    31. istrkge
    32. istrkgl
    33. istrkgld
    34. istrkg2ld
    35. istrkg3ld
    36. axtgcgrrflx
    37. axtgcgrid
    38. axtgsegcon
    39. axtg5seg
    40. axtgbtwnid
    41. axtgpasch
    42. axtgcont1
    43. axtgcont
    44. axtglowdim2
    45. axtgupdim2
    46. axtgeucl
    47. 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. ttgvalOLD
    5. ttglem
    6. ttglemOLD
    7. ttgbas
    8. ttgbasOLD
    9. ttgplusg
    10. ttgplusgOLD
    11. ttgsub
    12. ttgvsca
    13. ttgvscaOLD
    14. ttgds
    15. ttgdsOLD
    16. ttgitvval
    17. ttgelitv
    18. ttgbtwnid
    19. ttgcontlem1
    20. xmstrkgc
    21. Geometry in the complex plane
    22. Geometry in Euclidean spaces