Definition df-trkg 28775

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 2800.

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

• A1 A kind of reflexivity for the congruence relation (TarskiG_C)
• A2 Transitivity for the congruence relation (TarskiG_C)
• A3 Identity for the congruence relation (TarskiG_C)
• A4 Axiom of segment construction (TarskiG_CB)
• A5 5-segment axiom (TarskiG_CB)
• A6 Identity for the betweenness relation (TarskiG_B)
• A7 Axiom of Pasch (TarskiG_B)
• A8 Lower dimension axiom (^◡Dim_TarskiG≥ “ {2})
• A9 Upper dimension axiom (V ∖ (^◡Dim_TarskiG≥ “ {3}))
• A10 Euclid's axiom (TarskiG_E)
• A11 Axiom of continuity (TarskiG_B)

Our definition is split into 5 parts:

• congruence axioms TarskiG_C (which metric spaces fulfill)
• betweenness axioms TarskiG_B
• congruence and betweenness axioms TarskiG_CB
• upper and lower dimension axioms Dim_TarskiG≥
• axiom of Euclid / parallel postulate TarskiG_E

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

Step	Hyp	Ref	Expression
1		cstrkg 28749	. 2 class TarskiG
2		cstrkgc 28750	. . . 4 class TarskiGC
3		cstrkgb 28751	. . . 4 class TarskiGB
4	2, 3	cin 3905	. . 3 class (TarskiGC ∩ TarskiGB)
5		cstrkgcb 28752	. . . 4 class TarskiGCB
6		vf	. . . . . . . . . 10 setvar 𝑓
7	6	cv 1569	. . . . . . . . 9 class 𝑓
8		clng 28756	. . . . . . . . 9 class LineG
9	7, 8	cfv 6540	. . . . . . . 8 class (LineG‘𝑓)
10		vx	. . . . . . . . 9 setvar 𝑥
11		vy	. . . . . . . . 9 setvar 𝑦
12		vp	. . . . . . . . . 10 setvar 𝑝
13	12	cv 1569	. . . . . . . . 9 class 𝑝
14	10	cv 1569	. . . . . . . . . . 11 class 𝑥
15	14	csn 4591	. . . . . . . . . 10 class {𝑥}
16	13, 15	cdif 3903	. . . . . . . . 9 class (𝑝 ∖ {𝑥})
17		vz	. . . . . . . . . . . . 13 setvar 𝑧
18	17	cv 1569	. . . . . . . . . . . 12 class 𝑧
19	11	cv 1569	. . . . . . . . . . . . 13 class 𝑦
20		vi	. . . . . . . . . . . . . 14 setvar 𝑖
21	20	cv 1569	. . . . . . . . . . . . 13 class 𝑖
22	14, 19, 21	co 7419	. . . . . . . . . . . 12 class (𝑥𝑖𝑦)
23	18, 22	wcel 2146	. . . . . . . . . . 11 wff 𝑧 ∈ (𝑥𝑖𝑦)
24	18, 19, 21	co 7419	. . . . . . . . . . . 12 class (𝑧𝑖𝑦)
25	14, 24	wcel 2146	. . . . . . . . . . 11 wff 𝑥 ∈ (𝑧𝑖𝑦)
26	14, 18, 21	co 7419	. . . . . . . . . . . 12 class (𝑥𝑖𝑧)
27	19, 26	wcel 2146	. . . . . . . . . . 11 wff 𝑦 ∈ (𝑥𝑖𝑧)
28	23, 25, 27	w3o 1102	. . . . . . . . . 10 wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))
29	28, 17, 13	crab 3418	. . . . . . . . 9 class {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}
30	10, 11, 13, 16, 29	cmpo 7421	. . . . . . . 8 class (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
31	9, 30	wceq 1570	. . . . . . 7 wff (LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
32		citv 28755	. . . . . . . 8 class Itv
33	7, 32	cfv 6540	. . . . . . 7 class (Itv‘𝑓)
34	31, 20, 33	wsbc 3746	. . . . . 6 wff [(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
35		cbs 17293	. . . . . . 7 class Base
36	7, 35	cfv 6540	. . . . . 6 class (Base‘𝑓)
37	34, 12, 36	wsbc 3746	. . . . 5 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
38	37, 6	cab 2743	. . . 4 class {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}
39	5, 38	cin 3905	. . 3 class (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
40	4, 39	cin 3905	. 2 class ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
41	1, 40	wceq 1570	1 wff TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))

This definition is used by:  axtgcgrrflx  28784  axtgcgrid  28785  axtgsegcon  28786  axtg5seg  28787  axtgbtwnid  28788  axtgpasch  28789  axtgcont1  28790  tglng  28868  f1otrg  29277  eengtrkg  29393