MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-trkg Structured version   Unicode version

Definition df-trkg 23571
Description: Define the class of Tarski geometries. A Tarski geometry is a set of points, equipped with a betweenness relation (denoting that a point lies on a line segment between two other points) and a congruence relation (denoting equality of line segment lengths). Here, we are using the following:
  • for congruence,  ( x  .-  y )  =  ( z  .-  w ) where  .-  =  ( dist `  W )
  • for betweenness,  y  e.  ( x I z ), where  I  =  (Itv `  W )
With this definition, the axiom A2 is actually equivalent to the transitivity of addition, eqtrd 2501.

Tarski originally had more axioms, but later reduced his list to 11:

  • A1 A kind of reflexivity for the congruence relation (TarskiGC)
  • A2 Transitivity for the congruence relation (TarskiGC)
  • A3 Identity for the congruence relation (TarskiGC)
  • A4 Axiom of segment construction (TarskiGBC)
  • A5 5-segment axiom (TarskiGBC)
  • A6 Identity for the betweenness relation (TarskiGB)
  • A7 Axiom of Pasch (TarskiGB)
  • A8 Lower dimension axiom (TarskiG2D)
  • A9 Upper dimension axiom (TarskiG2D)
  • A10 Euclid's axiom (TarskiGE)
  • A11 Axiom of continuity (TarskiGB)
Our definition is split into 5 parts:
  • congruence axioms TarskiGC (which metric spaces fulfill)
  • betweenness axioms TarskiGB
  • congruence and betweenness axioms TarskiGCB
  • upper and lower dimension axioms TarskiG2D
  • axiom of Euclid / parallel postulate TarskiGE

So our definition of a Tarskian Geometry includes the 3 axioms for the quaternary congruence relation (A1, A2, A3), the 3 axioms for the ternary betweenness relation (A6, A7, A11), and the 2 axioms of compatibility of the congruence and the betweenness relations (A4,A5).

It does not include Euclid's axiom A10, nor the 2-dimensional axioms A8 (Lower dimension axiom) and A9 (Upper dimension axiom) so the number of dimensions of the geometry it formalizes is not constrained.

Considering A2 as one of the 3 axioms for the quaternary congruence relation is somewhat conventional, because the transitivity of the congruence relation is automatically given by our choice to take the distance as this congruence relation in our definition of Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017.) (Revised by Thierry Arnoux, 27-Apr-2019.)

Assertion
Ref Expression
df-trkg  |- TarskiG  =  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
Distinct variable group:    f, p, i, x, y, z

Detailed syntax breakdown of Definition df-trkg
StepHypRef Expression
1 cstrkg 23546 . 2  class TarskiG
2 cstrkgc 23547 . . . 4  class TarskiGC
3 cstrkgb 23548 . . . 4  class TarskiGB
42, 3cin 3468 . . 3  class  (TarskiGC  i^i TarskiGB )
5 cstrkgcb 23549 . . . 4  class TarskiGCB
6 vf . . . . . . . . . 10  setvar  f
76cv 1373 . . . . . . . . 9  class  f
8 clng 23554 . . . . . . . . 9  class LineG
97, 8cfv 5579 . . . . . . . 8  class  (LineG `  f )
10 vx . . . . . . . . 9  setvar  x
11 vy . . . . . . . . 9  setvar  y
12 vp . . . . . . . . . 10  setvar  p
1312cv 1373 . . . . . . . . 9  class  p
1410cv 1373 . . . . . . . . . . 11  class  x
1514csn 4020 . . . . . . . . . 10  class  { x }
1613, 15cdif 3466 . . . . . . . . 9  class  ( p 
\  { x }
)
17 vz . . . . . . . . . . . . 13  setvar  z
1817cv 1373 . . . . . . . . . . . 12  class  z
1911cv 1373 . . . . . . . . . . . . 13  class  y
20 vi . . . . . . . . . . . . . 14  setvar  i
2120cv 1373 . . . . . . . . . . . . 13  class  i
2214, 19, 21co 6275 . . . . . . . . . . . 12  class  ( x i y )
2318, 22wcel 1762 . . . . . . . . . . 11  wff  z  e.  ( x i y )
2418, 19, 21co 6275 . . . . . . . . . . . 12  class  ( z i y )
2514, 24wcel 1762 . . . . . . . . . . 11  wff  x  e.  ( z i y )
2614, 18, 21co 6275 . . . . . . . . . . . 12  class  ( x i z )
2719, 26wcel 1762 . . . . . . . . . . 11  wff  y  e.  ( x i z )
2823, 25, 27w3o 967 . . . . . . . . . 10  wff  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) )
2928, 17, 13crab 2811 . . . . . . . . 9  class  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) }
3010, 11, 13, 16, 29cmpt2 6277 . . . . . . . 8  class  ( x  e.  p ,  y  e.  ( p  \  { x } ) 
|->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
319, 30wceq 1374 . . . . . . 7  wff  (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
32 citv 23553 . . . . . . . 8  class Itv
337, 32cfv 5579 . . . . . . 7  class  (Itv `  f )
3431, 20, 33wsbc 3324 . . . . . 6  wff  [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
35 cbs 14479 . . . . . . 7  class  Base
367, 35cfv 5579 . . . . . 6  class  ( Base `  f )
3734, 12, 36wsbc 3324 . . . . 5  wff  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } )
3837, 6cab 2445 . . . 4  class  { f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f
)  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  (
p  \  { x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) }
395, 38cin 3468 . . 3  class  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } )
404, 39cin 3468 . 2  class  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
411, 40wceq 1374 1  wff TarskiG  =  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  axtgcgrrflx  23580  axtgcgrid  23581  axtgsegcon  23582  axtg5seg  23583  axtgbtwnid  23584  axtgpasch  23585  axtgcont1  23586  tglng  23654  f1otrg  23843  eengtrkg  23957
  Copyright terms: Public domain W3C validator