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

Definition df-trkg 28139
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, (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑀) where βˆ’ = (distβ€˜π‘Š)
  • for betweenness, 𝑦 ∈ (π‘₯𝐼𝑧), where 𝐼 = (Itvβ€˜π‘Š)
With this definition, the axiom A2 is actually equivalent to the transitivity of equality, eqtrd 2771.

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 (TarskiGCB)
  • A5 5-segment axiom (TarskiGCB)
  • A6 Identity for the betweenness relation (TarskiGB)
  • A7 Axiom of Pasch (TarskiGB)
  • A8 Lower dimension axiom (β—‘DimTarskiGβ‰₯ β€œ {2})
  • A9 Upper dimension axiom (V βˆ– (β—‘DimTarskiGβ‰₯ β€œ {3}))
  • 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 DimTarskiGβ‰₯
  • 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 ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
Distinct variable group:   𝑓,𝑝,𝑖,π‘₯,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkg
StepHypRef Expression
1 cstrkg 28113 . 2 class TarskiG
2 cstrkgc 28114 . . . 4 class TarskiGC
3 cstrkgb 28115 . . . 4 class TarskiGB
42, 3cin 3947 . . 3 class (TarskiGC ∩ TarskiGB)
5 cstrkgcb 28116 . . . 4 class TarskiGCB
6 vf . . . . . . . . . 10 setvar 𝑓
76cv 1539 . . . . . . . . 9 class 𝑓
8 clng 28120 . . . . . . . . 9 class LineG
97, 8cfv 6543 . . . . . . . 8 class (LineGβ€˜π‘“)
10 vx . . . . . . . . 9 setvar π‘₯
11 vy . . . . . . . . 9 setvar 𝑦
12 vp . . . . . . . . . 10 setvar 𝑝
1312cv 1539 . . . . . . . . 9 class 𝑝
1410cv 1539 . . . . . . . . . . 11 class π‘₯
1514csn 4628 . . . . . . . . . 10 class {π‘₯}
1613, 15cdif 3945 . . . . . . . . 9 class (𝑝 βˆ– {π‘₯})
17 vz . . . . . . . . . . . . 13 setvar 𝑧
1817cv 1539 . . . . . . . . . . . 12 class 𝑧
1911cv 1539 . . . . . . . . . . . . 13 class 𝑦
20 vi . . . . . . . . . . . . . 14 setvar 𝑖
2120cv 1539 . . . . . . . . . . . . 13 class 𝑖
2214, 19, 21co 7412 . . . . . . . . . . . 12 class (π‘₯𝑖𝑦)
2318, 22wcel 2105 . . . . . . . . . . 11 wff 𝑧 ∈ (π‘₯𝑖𝑦)
2418, 19, 21co 7412 . . . . . . . . . . . 12 class (𝑧𝑖𝑦)
2514, 24wcel 2105 . . . . . . . . . . 11 wff π‘₯ ∈ (𝑧𝑖𝑦)
2614, 18, 21co 7412 . . . . . . . . . . . 12 class (π‘₯𝑖𝑧)
2719, 26wcel 2105 . . . . . . . . . . 11 wff 𝑦 ∈ (π‘₯𝑖𝑧)
2823, 25, 27w3o 1085 . . . . . . . . . 10 wff (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
2928, 17, 13crab 3431 . . . . . . . . 9 class {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))}
3010, 11, 13, 16, 29cmpo 7414 . . . . . . . 8 class (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})
319, 30wceq 1540 . . . . . . 7 wff (LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})
32 citv 28119 . . . . . . . 8 class Itv
337, 32cfv 6543 . . . . . . 7 class (Itvβ€˜π‘“)
3431, 20, 33wsbc 3777 . . . . . 6 wff [(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})
35 cbs 17151 . . . . . . 7 class Base
367, 35cfv 6543 . . . . . 6 class (Baseβ€˜π‘“)
3734, 12, 36wsbc 3777 . . . . 5 wff [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})
3837, 6cab 2708 . . . 4 class {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}
395, 38cin 3947 . . 3 class (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
404, 39cin 3947 . 2 class ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
411, 40wceq 1540 1 wff TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
Colors of variables: wff setvar class
This definition is referenced by:  axtgcgrrflx  28148  axtgcgrid  28149  axtgsegcon  28150  axtg5seg  28151  axtgbtwnid  28152  axtgpasch  28153  axtgcont1  28154  tglng  28232  f1otrg  28557  eengtrkg  28679
  Copyright terms: Public domain W3C validator