1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
\begin{definition}\label{collinear}
$a$ is collinear with $b$ and $c$ iff $\Betw{a}{b}{c}$ or $\Betw{b}{c}{a}$ or $\Betw{c}{a}{b}$.
\end{definition}
\begin{axiom}[Reflexivity of congruence]\label{cong_refl_swap} % SST A1
Let $a, b$ be points.
Then $\Cong{a}{b}{b}{a}$.
\end{axiom}
\begin{axiom}[Pseudotransitivity of congruence]\label{cong_pseudotransitive} % SST A2
Let $a, b, c, d$ be points.
If $\Cong{c}{d}{a}{b}$ and $\Cong{c}{d}{e}{f}$ then $\Cong{a}{b}{e}{f}$.
\end{axiom}
\begin{axiom}[Identity of congruence]\label{cong_id} % SST A3
Let $a, b, c$ be points.
If $\Cong{a}{b}{c}{c}$ then $a = b$.
\end{axiom}
\begin{axiom}[Segment construction]\label{segment_construction} % SST A4
There exists a point $c$ such that $\Betw{a}{b}{c}$ and $\Cong{b}{c}{d}{e}$.
\end{axiom}
\begin{definition}\label{ofs}
Let $x,y,z,r,u,v,w,p$ be points.
$\OFS{x}{y}{z}{r}{u}{v}{w}{p}$ if and only if
$\Betw{x}{y}{z}
\land \Betw{u}{v}{w}$
and
$\Cong{x}{y}{u}{v}
\land \Cong{y}{z}{v}{w}
\land \Cong{x}{r}{u}{p}
\land \Cong{y}{r}{v}{p}$.
\end{definition}
\begin{axiom}[Five segment axiom]\label{five_segment} % SST A5
Let $a,b,c,d,a',b',c',d'$ be points.
If $\OFS{a}{b}{c}{d}{a'}{b'}{c'}{d'}$ and
$a \neq b$ then $\Cong{c}{d}{c'}{d'}$.
\end{axiom}
\begin{axiom}[Identity of betweenness]\label{betw_id}
Let $a,b$ be points.
If $\Betw{a}{b}{a}$ then $a = b$.
\end{axiom}
\begin{axiom}[Inner Pasch]\label{innerpasch} % SST A7
Let $x,y,z,u,v,w$ be points.
If $\Betw{x}{u}{z}$ and $\Betw{y}{v}{z}$ then there exists a point $w$
such that $\Betw{u}{w}{y}$ and $\Betw{v}{w}{x}$.
\end{axiom}
% \begin{axiom}[Lower dimension] % SST A8
% %There exist points $a, b, c$ such that
% There exists $a, b, c$ such that $a,b,c$ are points and
% $a$ is not collinear with $b$ and $c$.
% \end{axiom}
\begin{axiom}[Upper dimension]\label{upperdim} % SST A9
Let $x,y,z,u,v$ be points.
If $\Cong{x}{u}{x}{v}$ and $\Cong{y}{u}{y}{v}$
and $\Cong{z}{u}{z}{v}$ and $u \neq v$
then $x$ is collinear with $y$ and $z$.
\end{axiom}
% \begin{axiom}[Euclid]
% Assume $x \neq r$.
% If $\Betw{x}{r}{v}$ and $\Betw{y}{r}{z}$
% then there exist points $s,t$ such that
% $\Betw{x}{y}{s}$ and $\Betw{x}{z}{t}$ and $\Betw{s}{v}{t}$.
% \end{axiom}
\begin{lemma}[Reflexivity of congruence]\label{cong_refl} % Satz 2.1
Let $a, b$ be points.
Then $\Cong{a}{b}{a}{b}$.
\end{lemma}
\begin{lemma}[Symmetry of congruence]\label{cong_sym} % Satz 2.2
Let $a, b, c, d$ be points.
Suppose $\Cong{a}{b}{c}{d}$.
Then $\Cong{c}{d}{a}{b}$.
\end{lemma}
\begin{lemma}[Transitivity of congruence]\label{cong_transitive} % Satz 2.3
Let $a, b, c, d, e, f$ be points.
If $\Cong{a}{b}{c}{d}$ and $\Cong{c}{d}{e}{f}$
then $\Cong{a}{b}{e}{f}$.
\end{lemma}
\begin{lemma}\label{cong_shuffle_left} % Satz 2.4
Let $a, b, c, d$ be points.
If $\Cong{a}{b}{c}{d}$
then $\Cong{b}{a}{c}{d}$.
\end{lemma}
\begin{lemma}\label{cong_shuffle_right} % Satz 2.5
Let $a, b, c, d$ be points.
If $\Cong{a}{b}{c}{d}$
then $\Cong{b}{a}{d}{c}$.
\end{lemma}
\begin{lemma}[Zero segments are congruent]\label{cong_zero} % Satz 2.8
Let $a,b$ be points.
Then $\Cong{a}{a}{b}{b}$.
\end{lemma}
% Somewhat slow for now.
%\begin{lemma}[Concatenation of segments]\label{segment_concat} % Satz 2.11
% Assume $\Betw{x}{y}{z}$ and $\Betw{r}{v}{w}$.
% Assume $\Cong{x}{y}{r}{v}$ and $\Cong{y}{z}{v}{w}$.
% Then $\Cong{x}{z}{r}{w}$.
%\end{lemma}
%\begin{proof}
% % We have
% $\OFS{x}{y}{z}{x}{r}{v}{w}{r}$. % By previous results and assumption.
% If $x = y$ then $r = v$. % Axiom A3 gives this implication.
% If $x \neq y$ then $\Cong{x}{z}{r}{w}$. % Axiom A5 completes the proof.
%\end{proof}
|
