# Research Proposal: Foundations of Hyperbolic Geometry
## History and background
David Hilbert, in his 1903 work introducing the "calculus of ends", gave the first axiomatisation of plane hyperbolic geometry, wherein a hyperbolic parallel postulate is added to the postulates of absolute geometry. In 1938, Karl Menger [2] showed that the concepts of betweenness and equidistance for the hyperbolic plane are definable in terms of point-line incidence alone. Menger and his students believed this would eventually lead to a 'system of fairly simple assumptions in terms of the projective operations' [3]. Helen Skala [4] (1992) gave the first elegant first-order axiom system for plane hyperbolic geometry by introducing hyperbolic forms of the theorems of Pappus and Desargues to replace Menger’s axiom involving projectivities. As a consequence, Skala showed that hyperbolic geometry is an incidence geometry.
Recently, in the work of Bamberg and Penttila (2023) [1], Skala’s system has been further simplifed by replacing Pappus' and Desargues' theorems with two simpler axioms, also in terms of point-line incidence. While the first "midpoint axiom" is completely natural, the second "_perpendicularity axiom_" is more elaborate and its independence from the other seven axioms remains in question.
## Research question
* Investigate whether the perpendicularity axiom is necessary for a complete and independent set of axioms for plane hyperbolic geometry by using an algebraic form of the axiom system codified in an interactive proof solver.
## Methodology and Timeline
**Weeks 1-2**: Understand the scope of the problem, including the algebraic form of the geometric axioms. Perform investigations in GeoGebra and include visual illustrations in report. Become accustomed with an interactive proof solver.
**Weeks 3-4**: Utilising an interactive proof solver, codify the problem and search for a proof of the perpendicularity axiom.
**Weeks 5-6**: If a proof is found, translate it into standard mathematical language and seek to visualise the logic of the proof, elucidating the dependence of the perpendicularity axiom. If no proof is found, attempt to find a counterexample or to show that no proof exists, therefore showing the independence of the axiom. Detail all findings in report.
---
## References
[1]: J. Bamberg and T. Penttila, Simpler foundations for the hyperbolic plane,
Forum Mathematicum, 35 (2023), no. 5, 1301-1325.
[2]: K. Menger, Non-Euclidean geometry of joining and intersecting, Bull. Amer. Math. Soc. 44 (1938), no. 12, 821–824.
[3]: K. Menger. On algebra of geometry and recent progress in non-Euclidean geometry. Rice Inst. Pamphlet, no. 27, 41–79, 1940.
[4]: H. L. Skala, Projective-type axioms for the hyperbolic plane, Geom. Dedicata 44 (1992), no. 3, 255–272.
---
## Coming up with identities
Taking Jolyon's A13, we get this:
:::info
Suppose $X$ is a rimpoint, and we have half-turns $P,Q,R,S,O,O'$. Assume
- $(PQR)^2=1$
- $(PQS)^2=1$
- $X^{PQO*OPQ}=X$ where * could be one of $P$, $Q$, $R$, or $S$.
- $X^{RSO'*O'RS}=X$ where * could be one of $P$, $Q$, $R$, or $S$.
- $X^{OR}=X$.
We are required to prove that $X^{O'R}=X$.
:::
Simplification:
- We can rewrite $PQ=RT$ where $T=RPQ$. This eliminates one variable:
:::info
Suppose $X$ is a rimpoint, and we have half-turns $R,S,T,O,O'$. Assume
- $(RST)^2=1$
- $X^{RTO*ORT}=X$ where * could be one of $R$, $S$, $T$.
- $X^{RSO'*O'RS}=X$ where * could be one of $R$, $S$, $T$.
- $X^{OR}=X$.
We are required to prove that $X^{O'R}=X$.
:::
Some other things can be done, like noticing that $X^R=X^O$. We could also write $X$ in terms of a rimpoint $L$ on $RS$. For instance, we could have $L^O=X^{PQ}=X^{RT}$, and $L^{O'}=X^{RS}$. Then we have:
:::info
Suppose $L$ is a rimpoint, and we have half-turns $R,S,T,O,O'$. Assume
- $L^R=L^S=L^T$
- $L^{*ORT}=L^{OTR}$ where * could be one of $R$, $S$, $T$.
- $L^{*O'RS}=L^{O'SR}$ where * could be one of $R$, $S$, $T$.
- $L^{OTROR}=L^{OTR}$.
We are required to prove that $L^{O'SROR}=L^{O'SR}$.
:::
Simplifying ...
:::info
Suppose $L$ is a rimpoint, and we have half-turns $R,S,T,O,O'$. Assume
- $L^R=L^S=L^T$
- $L^{RORTRTO}=L$
- $L^{RO'RSRSO'}=L$
- $L^{OTROTO}=L$.
We are required to prove that $L^{O'SRO'SO'}=L$.
:::
# Why PGL?
The basic idea, is that a geometry with a lot of symmetry can be recovered from the symmetry. This is essentially Felix Klein's _Erlangen Programm_. The group of a Cayley-Klein hyperbolic plane is $PGL(2,F)$ for some ordered field $F$. But how do we characterise $PGL(2,F)$? First, let's think of its elements as fractional linear transformations of the form $$z\mapsto \frac{az+b}{cz+d}$$ where $ad-bc\ne 0$. The action on the conic is equivalent to the action on the projective line $PG(1,F)$, and is transitive on points of $PG(1,F)$. So any point stabiliser $PGL(2,F)_X$ is conjugate to the stabiliser of a particular element. The stabiliser of $\infty$ can be calculated easily:
$$\begin{align}
\infty=\frac{a\infty+b}{c\infty+d}&\iff \infty=\frac{a+b/\infty}{c+d/\infty}\\
&\iff \infty=\frac{a+0}{c+0}\\
&\iff c=0.
\end{align}$$ So the stabiliser of $\infty$ is the subgroup of fractional linear transformations of the form $$z\mapsto \frac{a}{d}z+\frac{b}{d}.$$ We can just rewrite the $a/d$ and $b/d$ terms and we see that we just get all affine transformations: $AGL(1,F)$. Now $AGL(1,F)$ is transitive on all the points of the projective line apart from $\infty$, and so we can consider fixing 0 in $AGL(1,F)$. Suppose $z\mapsto \alpha z+\beta$ fixes 0:
$$0=\alpha 0+\beta\iff \beta=0.$$
So we see that the stabiliser of $\infty$ and $0$ in $PGL(2,F)$ is just multiplication by nonzero elements of $F$, or more eloquently, the group $GL(1,F)$. We have used the fact that $PGL(2,F)$ is 2-transitive, but in fact, it is _sharply 3-transitive_. (This means that for every pair of triples of elements of the set, there is a unique group element mapping one to the other).
_Theorem (Jacques Tits, 1952):_ Suppose $H$ is sharply 3-transitive with an Abelian two-point stabiliser. Then $H$ is permutationally isomorphic to $PGL(2, F)$ acting on the projective line $PG(1,F)$, for some field $F$.
This is an amazing theorem, and even more remarkable that Tits was 22 years old when it was published!
So what about $PSL(2,F)$? The issue is that the properties we like about $PGL(2,F)$ no longer hold:
- $PSL(2,F)$ is the subgroup of fractional linear transformations $z\mapsto \frac{az+b}{cz+d}$ where $ad-bc=1$.
- $PSL(2,F)$ is 2-transitive, but not 3-transitive. It does, however, have just two orbits on distinct triples.
- The stabiliser of $\infty$ in $PSL(2,F)$ is $AGL^+(1,F)$: the fractional linear transformations $z\mapsto \alpha^2 z+\beta$ where $\alpha,\beta\in F$ and $\alpha\ne 0$. Notice that the scaling term is a square in $F$, which might not represent every element of $F$. (Only in characteristic 2, do we have every element is square).
- The stabiliser of $\infty$ and $0$ in $PSL(2,F)$ is $GL^+(1,F)$: the fractional linear transformations $z\mapsto \alpha^2 z$ where $\alpha\in F^*$.
So characterising $PSL$ would be tricky, but not unfathomnable. I just don't know of any nice characterisation.
Why does it matter? Well, we have a nice characterisation for $PGL(2,F)$, but we can only imagine doing that if we also include reflections. In the Cayley-Klein hyperbolic planes, the half-turns are orientation preserving, which means that you will only generate $PSL(2,F)$. This leaves the question wide open whether we could recover this group instead, via a characterisation of $PSL(2,F)$.
This following is the approach we took in a draft of the paper, which is another proof, but using Mäurer's Theorem:

### Some more thoughts
- Let $G$ be the group generated by the half-turns.
- We already know that $G$ is 2-transitive, and in fact, c-3-transitive.
- If we could show that the stabiliser of any three rimpoints in $G$ is trivial, then it will follow (from a nice little argument I have a draft of) that the two-point stabiliser is Abelian.
- Then by [Tararin's result](https://zbmath.org/1055.20001), we will get $PGL^+(2,F)$, and the rest will follow.
The issue is, I couldn't show that the stabiliser of three rimpoints is trivial! This is another situation where I get the Star of David.
If we could show that $G$ contains $PSL(2,F)$, then we would be done, and it would be amazing, because we definitely wouldn't need the axiom A11.
Things I know about fixing three rimpoints:
- If P, Q, R, S are finite points, then either PQRS = 1 or PQRS has at most two fixed rimpoints. They were not necessarily distinct finite points, so every nontrivial element of a 3-point stabiliser in $G$ is a product of at least 5 half-turns.
## Jolyon: argument towards showing three-point stabiliser is trivial
**Claim:**
The 2-pt stabiliser of X,Y is group generated by axial maps with axis XY.
*Proof:* not yet.
**Theorem: the three-point stabiliser is trivial.**
*Proof:*
Let g be in 3-point stabiliser of X,Y,Z. Then g is in two-point stabiliser of X,Y. Then by **Claim** above, g is the identity or g is an order-preserving axial map with axis XY. By thm, if g is order-preserving axial map with axis XY, then g has exactly two fixed points (X and Y), but by hypothesis, g is in the three-point stabiliser. Thus, g is not an order-preserving axial map. Thus, g is the identity, so the three-point stabiliser is trivial.
# Interpretation of A9 (bowtie-perpendicular)
## Jolyon: Proof of A9 in C-K hyperbolic plane
#### Statement of A9
Prelim:
* Introduction of axioms (A1) through (A7)
* Definition of join of two points, of point and end, and of two ends.
Let $\bar{X}$ be an end. For every point $P$ we define $\bar{X}^P$ as the end of the line $P\bar{X}$ that is different to $\bar{X}$. We adopt the notational convention $\bar{X}^{PQ} := (\bar{X}^P)^Q$ for all points $P,Q$.
Now we state (A9):
(A9) For every line $\ell$ and every end $\bar{X}$ not on $\ell$ there exists a line $m$ with end $\bar{X}$ such that for all distinct points $P,Q$ on $\ell$, if two distinct intersecting lines are each asymptotic to both $\ell$ and $\bar{X}^{PQ}\bar{X}^{QP}$, then their intersection point lies on $m$.
To simplify the statement of this axiom, following Bamberg and Penttila (p. 14), we introduce an operation $\bowtie$ (which may be read as 'bowtie' or 'cross') to give the intersection point of a pair of intersecting mutual asymptotes to two ultraparallel lines. Rigorously, let $\ell$ and $m$ be ultraparallel and let their ends be $L,L'$ and $M,M'$ respectively. Then (c.f. Bamberg and Penttila, Lemma 3.4, using (A1) to (A7) alone), one of the pairs $\{LM,L'M'\}$ or $\{LM',L'M\}$ of mutual asymptotes to $\ell$ and $m$ is an intersecting pair (while the other pair is not). We denote the intersection point of the intersecting pair of mutual asymptotes to $\ell$ and $m$ by $\ell\bowtie m$ (equally, $m\bowtie \ell$).
Thus, (A9) may be written more compactly as:
(A9) For every line $\ell$ and every end $\bar{X}$ not on $\ell$ there exists a line $m$ with end $\bar{X}$ such that for all distinct points $P,Q$ on $\ell$, the point $\ell\bowtie \bar{X}^{PQ}\bar{X}^{QP}$ lies on $m$.
This axiom specifies nothing more than that every point of the form $\ell\bowtie \bar{X}^{PQ}\bar{X}^{QP}$ for some $P,Q$ on $\ell$ and a fixed end $\bar{X}$ not on $\ell$ are collinear and that their line of alignment has end $\bar{X}$.
---
#### Interpretation of A9
To shed light on the meaning of (A9), we move to a concrete model of hyperbolic geometry -- the interior of a non-empty conic in a projective plane.
Let $\mathcal{P}$ be a projective plane and $\mathcal{O}$ be a non-empty conic ('oval') in $\mathcal{P}$. Denote the internal points of $\mathcal{O}$ by $\mathcal{I}$. Recall then that $\mathcal{I}$ serves as a (generalised, metric-free) Beltrami-Klein hyperbolic plane with set of ends $\mathcal{O}$.
We form the natural analogue in this setting for the notations defined above.
First, for all points $\bar{X}\in \mathcal{O}$ and $P\in \mathcal{I}$ we define $\bar{X}^P$ as the unique point on both $\mathcal{O}$ and $P\bar{X}$ (which is a secant to $\mathcal{O}$ by elementary results) that is different to $\bar{X}$. We adopt the notational convention $\bar{X}^{PQ} := (\bar{X}^{P})^Q$ for all $P,Q\in \mathcal{I}$.
Second, let $\ell,m$ be distinct secants of $\mathcal{O}$ and suppose their intersection point is external to $\mathcal{O}$. Take $\ell\cap\mathcal{O} = \{\bar{L},\bar{L}'\}$ and $m\cap\mathcal{O} = \{\bar{M},\bar{M}'\}$. It can be shown that exactly one of the two pairs of secants $\{\bar{L}\bar{M},\bar{L}'\bar{M'}\}$, $\{\bar{L}\bar{M}',\bar{L}'\bar{M}\}$ intersects in a point internal to $\mathcal{O}$ (i.e., in $\mathcal{I}$). We denote the intersection point of the internally intersecting pair by $\ell\bowtie m$ (equally, $m\bowtie \ell$).
Now, using elementary pole-polar theory and Rigby's (1969) theory of axial mappings, we prove that (A9) holds in the hyperbolic plane $\mathcal{I}$:
**Theorem (A9).** For every secant $\ell$ of $\mathcal{O}$ and every point $\bar{X}$ on $\mathcal{O}$ not lying on $\ell$, there exists a secant $m$ of $\mathcal{O}$ through $\bar{X}$ such that for all distinct points $P,Q\in \ell\cap \mathcal{I}$ it holds that $\ell\bowtie X^{PQ}X^{QP}\in m\cap\mathcal{I}$.
*Proof.*
N.B. We follow the convention that a singleton set is identified with its sole element.
Let $\ell$ be a secant of $\mathcal{O}$ and take a point $\bar{X}$ on $\mathcal{O}$ not lying on $\ell$. Let $L$ be the pole of $\ell$ with respect to $\mathcal{O}$ and define $m:= L\bar{X}$, which is a secant by elementary results. Note that $m\cap \mathcal{I}$ is the hyperbolic perpendicular to $\ell\cap \mathcal{I}$ with end $\bar{X}$.
Let $M$ be the pole of $m$. Then $M\in \ell$ (by elementary results).
Let $h_M$ denote the harmonic homology with centre $M$ and axis $m$. Since its centre $M$ is the pole with respect to $\mathcal{O}$ of its axis $m$, $h_M$ preserves the conic $\mathcal{O}$ (by elementary results). (Hence, if $\bar{O}$ is a point on $\mathcal{O}$ not lying on $m$ then its image under $h_M$ is the point $\bar{O}^R$ for any point $R$ on the secant $M\bar{O}$.) Thus, $h_M$ corresponds to the hyperbolic reflection of $\mathcal{I}$ and its ends $\mathcal{O}$ in the line $m\cap \mathcal{I}$.
Let $P,Q$ be any two distinct points on $\ell\cap \mathcal{I}$ and consider the action of $PQ$ on the points of $\mathcal{O}$ as defined above (i.e. $\bar{O}\mapsto \bar{O}^{PQ}$). Define $\bar{X}_1 := X^{PQ}$ and $\bar{X}_2 := X^{QP}$.
Take $R:= \ell\cap m$ and note that since $\ell$ and $m$ are secants, $R\in \mathcal{I}$.
Then, by Rigby 1969, 3.3, there exists a unique point $S\in\ell$ such that $\bar{O}^{RS} = \bar{O}^{PQ}$ for all $\bar{O}\in\mathcal{O}$ (since $PQ$ is an axial mapping by Rigby 1969, 3.2). Furthemore, it can be shown from Rigby's proof that $S\in\mathcal{I}$. (Alternatively, it can be shown more strenuously, that $\mathcal{I}$ satisfies the necessary axioms among A1 through A7 for Bamberg and Penttila's results to hold)
In particular, $R,S\in \ell\cap\mathcal{I}$ are such that $R\neq S$, $\bar{X}^{RS} = \bar{X}_1$ and $\bar{X}^{SR} = \bar{X}_2$.
Recalling the operation defined earlier, consider $\bar{X}^{RS}$. By the involutory nature of the operation, $\bar{X}_2 = \bar{X}^{SR} = \bar{X}^{RRSR} = \bar{X}^{RS'}$ where $S':= RSR$ (*noting that the action of half-turns can be naturally extended to the points in $\mathcal{I}$*), and $S'\in\ell\cap\mathcal{I}$ (by the proof of Rigby 1969, 4.1). By construction (*needs explanation*), $R$ is the hyperbolic midpoint of the segment $\overline{SS'}$.
Then (recalling that $h_M$ is the hyperbolic reflection in $m\cap\mathcal{I}$) $S' = h_M (S)$ (*needs further explanation*) .
Now we show that $h_M(\bar{X}_2) = \bar{X}_1$.
First, by definition $\bar{X}^R \in R\bar{X} = m$, so $h_M (\bar{X}^R)= \bar{X}^R$ since $m$ is the axis of $h_M$. Then, noting that $h_M$ fixes $\mathcal{O}$, we have that
$h_M (\bar{X}_2) = h_M ( (\bar{X}^R)^S) = h_M (S\bar{X}^R \cap \mathcal{O}^{\setminus} \{\bar{X}^R\}) = h_M (S\bar{X}^R) \cap h_M (\mathcal{O}^{\setminus} \{\bar{X}^R\})$
$= h_M(S).h_M (\bar{X}^R) \cap h_M (\mathcal{O}^{\setminus} \{\bar{X}^R\}) = S'\bar{X}^R \cap \mathcal{O}^{\setminus} \{\bar{X}^R\}$,
where $P.Q$ denotes the join of two points.
Thus, we finally consider $\ell\bowtie \bar{X}^{PQ}\bar{X}^{QP} = \ell \bowtie \bar{X}_1\bar{X}_2$.
Let $\ell\cap \mathcal{O} =\{\bar{L}_1,\bar{L}_2\}$ such that $\bar{L}_1\bar{X}_1 \cap \bar{L}_2\bar{X}_2$ is an internal point.
Then $h_M(\ell\bowtie\bar{X}^{PQ}\bar{X}^{QP}) = h_M(\bar{L}_1\bar{X}_1\cap\bar{L}_2\bar{X}_2) = h_M(\bar{L}_1\bar{X}_1)\cap h_M(\bar{L}_2\bar{X}_2) = h_M(\bar{L}_1). \bar{X}_2 \cap h_M(\bar{L}_2). \bar{X}_1$.
Now, since $R\in \ell = \bar{L}_1 M = \bar{L}_2M$, we deduce that $h_M(\bar{L}_1,\bar{L}_2) = (\bar{L}_1^R,\bar{L}_2^R) = (\bar{L}_2,\bar{L}_1)$.
Thus, $h_M(\ell\bowtie\bar{X}^{PQ}\bar{X}^{QP}) = h_M(\bar{L}_1\bar{X}_1\cap\bar{L}_2\bar{X}_2) = \bar{L}_2\bar{X}_2 \cap \bar{L}_1\bar{X}_1 = \ell\bowtie \bar{X}^{PQ}\bar{X}^{QP}$.
Since $\ell\bowtie \bar{X}^{PQ}\bar{X}^{QP}\in \mathcal{I}$ by definition (i.e. does not lie on $\mathcal{O}$ and is not $M$), and yet is fixed by $h_M$, it must lie on the axis $m$ of $h_M$.
Thus, for all $P,Q\in \ell\cap \mathcal{I}$, it holds that $\ell\bowtie \bar{X}^{PQ}\bar{X}^{QP} \in m\cap\mathcal{I}$ where $m$ is the line through $\bar{X}$ constructed at the beginning of the proof.
$\square$.
## 4-pt Pascal
### John: set-up and idea
We want to prove $A_{11}$:
> (A11) Let $X$ be a rimpoint not on a line $\ell$. Then there is a unique point $R$ on $\ell$ such that for every finite point $S$ on $\ell$, two common parallels to $\ell$ and $X^{SR}X^{RS}$ meet on $XR$.
We will use the Four-Point Pascal Theorem:
> Consider four points $A, C, D, F$ in an irreducible conic of $PG(2,F)$, and let $t_A$ and $t_D$ be the tangent lines at $A$ and $D$ (respectively) to the conic. Then the points $t_A\cap t_D$, $AC\cap DF$, $CD\cap FA$ are collinear.
> [name=jolyonjoyce, time=Fri, Jul 12, 2024 9:34 AM]. We can add that $t_C \cap t_F$ is collinear with these. This follows from another application of the theorem above.
Suppose we have a conic $\mathcal{C}$ in an ordered Pappian projective plane (over a Euclidean field). Let $X$ be a rimpoint (a point of $\mathcal{C}$) not on a secant line $\ell$. Let $L$ be the pole of $\ell$ and let $m:=XL$. Let $R:=\ell\cap m$ and let $S$ be a finite point on $\ell$. Let $Z:=\ell\bowtie X^{SR}X^{RS}$. Let $n$ be the perpendicular to $m$ passing through the point $Z$, and let $N$ be the pole of $n$. Let $L_1:=X^{SRZ}$ and $L_2:=X^{RSZ}$ be the rimpoints on $\ell$. Now we apply the Four-Point Pascal Theorem with $(A,C,D,F):=(L_1,X^{SR},L_2,X^{RS})$:
- Note that $t_A\cap t_D=L$,
- Note that $AC\cap DF=Z$.
Then $L$, $Z$, and $CD\cap FA$ are collinear.

:::success
__Claim:__ $N=CD\cap FA=X^{SR}L_2\cap X^{RS}L_1$.
:::
Now $L$ and $N$ lie on $m$ (because $n$ passes through the pole of $m$) and hence $Z$ lies on $m$, and the proof is complete.
### Jolyon: a completion
This uses 4-point Pascal three times and 6-pt Pascal once.
Take $\ell\cap\mathcal{C}=\{L_1,L_2\}$ and take $X_1$ and $X_2$ to be the points on $\mathcal{C}$ such that $Z=L_1X_2\cap L_2X_1$. Also, take $n\cap\mathcal{C}=\{N_1,N_2\}$ such that $L_1 N_1\cap L_2 N_2$ is an external point of $\mathcal{C}$.
Apply 4-pt Pascal to $L_1, L_2$ and their tangents and $X_1, X_2$ and their tangents.
Then $L, Z, L_1 X_1\cap L_2 X_2$ and the pole of $X_1 X_2$ are collinear.
Apply 4-pt Pascal to $L_1,L_2$ and their tangents and $N_1,N_2$ and their tangents.
Then $L, L_1 N_2\cap L_2 N_1, L_1 N_1\cap L_2 N_2$, and $N$ are collinear.
Similarly, the pole of $X_1 X_2$, $X_1 N_2\cap X_2 N_1, X_1 N_1\cap X_2 N_2$, and $N$ are collinear.
And we know from (6-pt) Pascal applied to $L_1,N_2,X_1,L_2,N_1,X_2$ that $L_1 N_2\cap L_2 N_1, Z$ and $N_1 X_2 \cap N_2 X_1$ are collinear.
Then $L,Z$ and $N$ are collinear, and since $\ell$ and $n$ are perpendicular to $m$, it holds that $L,N\in m$ and it follows that $Z$ lies on $m$. -- But, in fact I think this fails.
Until we show that X_1 X_2 is perp to $m$, which I did above using the special way X is mapped and a harmonic homology, we cannot c
### Jolyon: completion II (line reflection + 4-pt Pascal)
Let $M$ be the pole of $m$.
Define $X_1 := X^{RS}$. Then $X_1 \notin m$ since $S\notin m$ ($S\in \ell^{R}$ and $R= \ell\cap m$). Then $MX_1$ is a secant and the hyperbolic perpendicular to $m$ through $X_1$.
Define $X_2 := X_1^m$, i.e. $MX_1 = MX_2$.
Now we take the hyperbolic reflection of $S= X^R X_1 \cap \ell$ in $m$.
$S^m = (X^R X_1 \cap \ell)^m = (X^R X_1)^m \cap \ell^m = (X^R)^m (X_1)^m \cap \ell = X^R X_2 \cap \ell$, since $X^R \in m$, $M\in \ell$, and $X_1^m = X_2$. Then by construction, $X_2 = X^{RS^m}$
It remains to show that $X_2 = X^{SR}$. Since $X_2= X^{RS^m}$ and $X^{SR} = X^{RRSR} = X^{RS^R}$ (where the action of internal points is extended naturally from rimpoints to all internal points as well), we must show that $S^m = S^R$.
Well, $S\in \ell$ and $R= \ell\cap m$, so indeed
$S^m = S^R$. (*needs explanation*...).
\[Claim: $S^m = S^R$.]
Then $X_2 = X^{RS^R}$.
Now apply 4-pt Pascal to the rimpoints of $\ell$ and $X_1$ and $X_2$. Then $L$, $Z$ and the pole of $X_1 X_2$ are collinear. By definition, $X_2 = X_1^m$, so we know $M\in X_1 X_2$ and hence (by elementary results) the pole of $X_1 X_2$ lies on $m$. By construction, $M\in \ell$ so (by elementary results) $L\in m$. We conclude that $Z\in m$.
This proves A11.
Finally, by Rigby's theory of axial maps (see my original proof of A9 via line reflection), since $S\in \ell^\setminus\{R\}$ was chosen arbitrarily, we conclude that the result holds for every pair of distinct points $P,Q\in \ell$.
So $m$ is a line which proves 'A9':
> (A9) For every line $\ell$ and every end $X$ not on $\ell$ there exists a line $m$ with end $X$ such that for all distinct points $P,Q$ on $\ell, if two distinct intersecting lines are each asymptotic to both $\ell$ and $X^{PQ} X^{QP}$, then their intersection point lies on $m$.
$\square$.
---
## Szczerba's last napkin
### Preamble
### Proof idea
Let $\mathcal{O}$ be an ordered plane (or '*begrenzten Ebenenstuck*' in the sense of Sperner 1938). That is, a planar incidence geometry in which the set of all the points on each line is equipped with a total, dense and unending order. Equivalently, $\mathcal{O}$ need only satisfy the first two of Hilbert's axiom groups.
Informally, the axioms can be stated as follows (we choose to omit)
:::info
Incidence.
1 If two points are distinct then they belong to a unique common line.
2 Every line contains a point.
Order.
3 Strict: If a point is between two points then the three points and mutually distinct and all collinear.
4 Linear: If three collinear points are mutually distinct then exactly one is between the other two.
5 Transitive: If $A,B,C,D$ are points such that $A$ is between $B$ and $D$, and $B$ is between $C$ and $D$; then $B$ is between $A$ and $C$.
Extension.
6 Dense: If two points are distinct then there exists a point between them.
7 Unending: If two points are distinct then there exists a point collinear with and distinct from them that is not between them.
Planarity.
8 Non-degeneracy: There exist three non-collinear points.
9 Pasch's axiom: If a line intersects a side of a triangle internally and does not pass through the vertices of the triangle then it intersects another side internally.
:::
The meaning of the first two axioms is readily apparent. It follows from the first axiom that collinearity is transitive and from the first and second axioms that every two distinct lines meet in at most one point.
As for the order axioms 3, 4 and 5, they equip the points of each line with a linear order.
Next, the extension axioms 6 and 7 points of each line with a linear order that is dense and unending: on every line there exist infinitely many points between any two distinct points thereon, and infinitely many points on either side of any one of its points.
Even so, observe that two lines need not intersect. For a simple example, the real Euclidean plane is a totally ordered plane in which non-intersecting (i.e. parallel) lines exist. Thus, an ordered plane need not be a *projective plane*; that is, a planar incidence geometry in which every two distinct lines have a point of intersection. Such an ordered plane which is not a projective plane is what Sperner (1938[and 1962?]) had in mind when he used the term '*begrenzten Ebenenstück*' ('bounded plane-piece') for the models of Hilbert's incidence and order axioms. When we speak of an ordered plane, one may have in mind a bounded region of a two-dimensional plane, densely populated by points and not containing its boundary.
Similarly, a projective plane need not be an ordered plane. The theory of projective planes is well-developed and generally does not employ notions of geometric order, though geometric order may arise from the order on a coordinatising algebraic structure.
We seek to improve on Sperner's 1938 result that gives necessary and sufficient conditions for an ordered plane to be embeddedable in a Pappian projective plane -- namely, that Pappus' and Desargues' theorems are valid in the ordered plane.
When we speak of the validity of a configuration theorem in an ordered plane, we mean that the theorem holds for every *complete* configuration in the ordered plane -- a configuration being so called if and only if all its constituent points as well as the points of intersection with which the theorem is concerned actually exist (this not being necessary for ordered planes that are not projectively closed).
For brevity's sake, an ordered plane will be called *Pappian* if Pappus' theorem holds for all complete Pappus configurations in the ordered plane. Similarly, we speak of *Desarguesian* ordered planes.
In these terms, the result of [Sperner's 1938 paper] may be expressed as follows:
:::info
**Sperner's Theorem (1938).** Let $\mathcal{O}$ be a totally ordered plane. If $\mathcal{O}$ is Desarguesian then it may be extended to a Desarguesian projective plane. If $\mathcal{O}$ is Desarguesian and Pappian then it may be extended to a Pappian projective plane.
:::
We seek to prove the following:
:::info
**Conjecture.** Let $\mathcal{O}$ be a totally ordered plane. If $\mathcal{O}$ is Pappian then it may be extended to a Pappian projective plane.
:::
If the conjecture is true, an analogue to Hessenberg's theorem for projective planes will immediately follow:
:::info
**Corollary (Hessenberg's theorem for totally ordered planes).** Every Pappian totally ordered plane is Desarguesian.
:::
*Proof.* Let $\mathcal{O}$ be a Pappian totally ordered plane. By the conjecture, there exists a Pappian projective extension $\mathcal{P}$ of $\mathcal{O}$. By Hessenberg's theorem, $\mathcal{P}$ is Desarguesian, so Desargues' theorem is valid for every Desargues configuration in $\mathcal{P}$. Then Desargues' theorem is valid for every complete Desargues configuration in $\mathcal{O}\subseteq\mathcal{P}$, so $\mathcal{O}$ is Desarguesian. $\blacksquare$
To simplify the communication of the proof of the conjecture, we introduce notational shorthands.
We agree to adopt the following notations:
:::info
**Notation.** Let $P,Q,R$ be arbitrary points and $\ell$ an arbitrary line of $\mathcal{O}$.
- We write $P\in \ell$ if and only if $P$ lies on (i.e. is contained by) $\ell$.
- If $P\neq Q$ then we write $PQ$ to denote the unique line joining $P$ and $Q$.
- If $P_1,\dots,P_k$ are $k\geq 3$ points then we write $(P_1\dots P_k)$ if and only if all points and collinear and at least two are distinct.
- We write $[PQR]$ if and only if $Q$ is between $P$ and $R$.
- If $P_1,\dots,P_k$ are $k\geq 3$ points then we write $[P_1\dots P_k]$ if and only if $[P_i P_{i+1} P_{i+2}]$ for all $1\leq i\leq k-2$.
:::
To clarify the notion of betweenness and its associated notation, let $P,Q,R$ be points in $\mathcal{O}$ and suppose that $[PQR]$. Then $Q$ is 'between' $P$ and $R$, so by axiom 3, $P,Q$ and $R$ are collinear and mutually distinct. Furthermore, in accord with intuition:
1. $P\neq R$ by axiom 4,
2. $[RQP]$ by the standard meaning of 'between',
3. $\lnot [PRQ]$ and $\lnot [QRP]$ by point 2 and axiom 4,
4. $\lnot [QPR]$ and $\lnot [RPQ]$ by point 2 and axiom 4.
Further suppose that there is a point $S$ such that $[QRS]$. Then we may write $[PQRS]$. Furthermore, one can conclude that $[PQS]$ and $[PRS]$, in accord with intuition.
*Proof.* $Q$ is between $P$ and $R$, and $R$ is between $Q$ and $R$, so by axiom 3, $P,Q,R$ are collinear and mutually distinct, and $Q,R,S$ are collinear and mutually distinct. Then there exist lines $\ell$ and $Then $Q,R\in PQ$ and $Q,R\in QS$. Since $R\neq Q$, by axiom 1 there exists a unique line containing and it follows that $P,Q,R$ and $S$ are all collinear and mutually distinct. Then by axiom 4 at
In the sequel we will not be so insistent on
---
Let $OXY$ be a non-degenerate triangle in $\mathcal{O}$, whose existence is assured by axiom 8. Take $I$ to be a point such that $[XIY]$, whose existence is assured by density.
Take all the inverse elements that exist in the ordered plane. By Pappus, $(S,+)$ is a **commutative** unital magma which may or may not have any inverses - if an element has an inverse then it is unique. Also, the operation of multiplication is unital and **commutative**, though $S$ need not be closed under $\cdot$ and negative elements need not have $\cdot$-inverses. The positive elements of $S$ form a commutative loop under multiplication.
Now extend $S$ by adjoining a two-sided $+$-inverse for every element- by elementary results these must be unique. Denote this set by $R$. Hence $(R,+)$ is now a commutative loop.
One must then show that $R^\times$ is now closed under multiplication and that every element has a $\cdot$-inverse so that $(R^{\times},\cdot)$ is a commutative loop.
Now one wishes to form a planar ternary ring $(R,T)$ from these two loops on $R$. I will look in the literature for such a result. It was shown that a planar ternary ring can be formed from two arbitrary *countably infinite* loops. We need a generalisation to arbitrary infinite cardinality (since first order logic cannot control the order of infinite models by Lowenheim-Skolem).
If one can do so, then one can analytically define a projective extension $\mathcal{P}$ of the ordered plane as the unique projective plane coordinatised by $(R,T)$. (Giving homogeneous coordinates to points and equations to lines in terms of $T$.) Every two distinct points are joined by a unique line, every two distinct lines intersect in a unique point. The points whose coordinates come only from $S$ are the points of the original ordered plane, so it is embedded in $\mathcal{P}$.
Since $(R^{\times},\cdot)$ is commutative, it follows that $\mathcal{P}$ is Pappian. Then by Hessenberg's theorem, $\mathcal{P}$ is also Desarguesian. Then Desargues' theorem holds for every Desargues configuration in $\mathcal{P}$, including the complete configurations in $\mathcal{O}$, so $\mathcal{O}$ is Desarguesian by definition. $\blacksquare$.
---
## Trivial 3-pt stabilisers
Proof idea: John
Let $\mathcal{I}$ be a model of A1 through A7 and let $\mathcal{O}$ be its associated set of rimpoints. Let $G$ be the group generated by half-turns.
**Lemma 1.** If $X_1 \dots X_6$ is a hexagon of rimpoints such that $\mathrm{C}(X_1 X_5 X_2 X_4 X_6 X_3)$, then its diagonal points exist (and hence are collinear by A7).
*Proof.* [Proof with order required here]
**Conjecture.** (Using additional axioms if necessary) For all/some $g\in G$ and all rimpoints $A,U,V$, if $g$ fixes $A$ and moves $U$ such that $\mathrm{C}(AUU^g)$, then $\mathrm{C}(AVV^g)$. I.e. there is no rimpoint $V$ for which $\mathrm{C}(AV^g V)$.
*Corollary.* If $\mathcal{I}$ satisfies A11 then the only element of $G$ fixing three distinct rimpoints is the identity.

*Proof.*
Towards a contradiction, suppose there exists $g\in G$, $g\neq 1$ that fixes three distinct rimpoints $A,B,C$. Since $g\neq 1$, there exists another rimpoint $X$ that is not fixed by $g$.
Relabelling $A,B,C$ as necessary, we assume that $\mathrm{C}(AXC)$.
Define $Y:= X^g$. Relabelling $X,Y$ if necessary (which we are free to do since $g$ is an involution) we assume that $\mathrm{C}(AXY)$.
Now we construct a Pascal configuration that is fixed by $g$ by making use of A11 and Lemma 1.
With $\sigma_\ell$ as defined in $\S 4$ of Bamberg and Penttila (p. 14), noting that $\sigma_\ell$ is well-defined if and only if A11 holds on $\ell$, we construct the following points:
$D := C^{\sigma_{AB}}$, $E:= A^{\sigma_{BC}}$, $F:= B^{\sigma_{AC}}$.
Then, by the definition of $\sigma_\ell$, $D,E,F$ are fixed by $g$.
Furthermore [Proof with order required here], $\mathrm{C}(FEABCD)$.
Then by Lemma 1, the finite points $F_1:= FE\cap BC$, $F_2:= EA\cap CD$, $F_3:= AB\cap DF$ exist and are collinear, lying on the Pascal line $f$. Let $F'$ denote the one rimpoint of $f$ that is on the same side of $AB$ as $F$ (noting that $f$ passes through $F_3\in AB$).
Since $FEABCD$ is fixed by $g$, also $F'$ is fixed by $g$.
Similarly, consider the hexagon $XEABCD$ and $YEABCD$. As before, $\mathrm{C}(XEABCD)$ and $\mathrm{C}(YEABCD)$, so by Lemma 1, the hexagons' diagonal points exist and lie on Pascal lines $x$ and $y$ respectively. by Lemma 1. Let $x$ and $y$ denote the hexagons' respective Pascal lines and take $X'$ and $Y'$ to be the one rimpoint of each line that lies on the same side of $AB$ as $X$ (or equally $Y$). Since $Y = X^g$, by the symmetry of the constructions $Y' = X'^g$.
Now one shows (via order proof) that $\mathrm{C}(AY'X')$.
This stands in contradiction to Conjecture 1 since $\mathrm{C}(AXY)$.
---
# Some ideas on reducing products of 5 to 3
I'm assuming all the theory of perpendicularity holds and that I have reflections at my disposal.
:::success
**Observation:** Let $ABCD$ be four finite points, no 3 collinear. Let $Y$ and $Z$ be the points on $\langle A,B\rangle$ and $\langle C,D\rangle$ (respectively) such that $\langle Y,Z\rangle$ is the common perpendicular to $\langle A,B\rangle$ and $\langle C,D\rangle$. Then $ABCD=(ABY)YZ(ZCD)$. That is, if we only care about the transformation $ABCD$, then we can replace the quadrangle with a quadrangle $A'B'C'D'$ having right-angles at $B'$ and $C'$.
:::
So now we define a _special quadrangle_.
:::info
**Special quadrangle:** A quadrangle $ABCD$ is _special_ if
1. $\langle B, C\rangle$ is perpendicular to $\langle A,B\rangle$ and $\langle C,D\rangle$;
2. The perpendicular $q$ at $A$ to $\langle A,B\rangle$ does not intersect the perpendicular $r$ at $D$ to $\langle C,D\rangle$.
:::
Notice that if we have a special quadrangle $ABCD$, as above, then $q$ and $r$ have a common perpendicular $p$. Let $M:=q\cap p$ and let $N:=r\cap p$. Then we have a right-hexagon (i.e., every internal angle is a right-angle) $ABCNM$. So a special quadrangle is just four consecutive points of a right-hexagon.
_Theorem:_ Suppose $ABCD$ is a special quadrangle. Then $ABCD$ is a product of 2 half-turns.
> _Proof:_ Let $\ell:=\langle A,B\rangle$, $m:=\langle C,D\rangle$, and let $q$, $r$ be the perpendiculars to $\ell$ and $m$ (respectively) through $A$ and $D$ respectively. Since $q$ and $r$ do not intersect, they have a common perpendicular $p$. Let $x:=\langle B,C\rangle$. Then
$$ABCD=ABCD=(q\ell)(\ell x)(x m)(mr)=qr=(qp)(pr)$$ which is a product of half-turns because $q$ and $p$ are perpendicular, and $p$ and $r$ are perpendicular.
_Theorem (to be proved):_ Let $ABCDE$ be a pentagon with right-angles at $B$ and $C$. Then we can find $D'$, $E'$ on $DE$ such that $DE=D'E'$ and $ABCD'$ is a special quadrangle.
$ABCD$ not special:

$ABCD'$ special:

As a consequence, if we have such a pentagon, then $ABCD'=MN$ for two finite points $M$ and $N$, and hence
$$ABCDE=(ABCD')E'=MNE'.$$ Since we can assume without loss of generality that there are right-angles at $B$ and $C$ (see the observation above), this argument shows that every product of five half-turns is a product of three half-turns.
Therefore, we have:
_Theorem:_ Let $G$ be the group generated by half-turns. Then every element of $G$ is a product of at most 4 half-turns.
_Corollary:_ The three-point stabiliser in $G$ is trivial.
(Recall that $ABCD$ is either trivial or fixes at most two rimpoints.)
From here, we can use Tararin's result to reprove the characterisation of hyperbolic planes over Euclidean fields.
:::danger
**Question:** Can we do any of this without the theory of perpendicularity?
:::
----
## On completeness and decidability
On 'complete' vs 'decidable', here's one way to look at it. I've thrown in consistent for good measure. The math logic course I did in Manchester got as far as Lowenheim-Skolem but unfortunately didn't touch on decidability, probably because it would have introduced needless confusion for a first course on the subject.
### Context:
We consider classical (excluded middle) first-order logic only.
Let $L$ be a language and $\Sigma$ an $L$-theory - i.e. a set of $L$-sentences. We can think of $\Sigma$ as an axiom system for some structures we are interested in.
[ This means I'll have to cover the following in my thesis: classical predicate logic (its axioms), first-order language, formal deduction (i.e. formal proof), L-structure, Tarski's definition of truth and models of a theory, Soundness and Completeness theorems ]
### Definitions:
$\Sigma$ is "sound" =
for every $L$-sentence $\phi$:
if $\phi$ is a theorem of $\Sigma$ then $\phi$ is a true statement in every model of $\Sigma$.
$\Sigma$ is "consistent" =
for every $L$-sentence $\phi$:
if $\phi$ is a theorem of $\Sigma$ then $\lnot\phi$ is not a theorem of $\Sigma$.
i.e. $\Sigma$ does not entail a contradiction
N.B. By the soundness theorem, every theory $\Sigma$ is sound, and any theory $\Sigma$ is consistent if and only if $\Sigma$ is satisfiable (has a model) by the axiom of excluded middle / proof by contradiction, so these two properties are trivial in classical first-order logic. That being said, whether a given, sufficiently complex structure (e.g. arithmetic) is free of contradictions is something we have to assume -- maybe we will come across a contradiction some day, maybe mathematics is inconsistent...
$\Sigma$ is "complete" =
for every $L$-sentence $\phi$:
$\phi$ is a theorem of $\Sigma$ OR its negation $\lnot\phi$ is a theorem of $\Sigma$.
i.e. $\Sigma$ is "maximally strong".
N.B. OR is not XOR, so every inconsistent theory is trivially complete, since every sentence is a theorem of any contradiction. Both $\phi$ and $\lnot\phi$ hold for all $\phi$.
$\Sigma$ is "decidable" =
there exists a finitely defined and always terminating algorithm that will correctly assign to any $L$-sentence exactly one of the values "theorem of $\Sigma$" or "not theorem of $\Sigma$".
i.e. $\Sigma$ admits a "universal, theorem-checking algorithm"
Important examples:
1. every inconsistent theory $\Sigma$ is trivially decidable since every sentence is a theorem of any contradiction. The universal theorem-checker is just defined as the constant function "theorem of $\Sigma$".
2. every complete and recursively enumerable (i.e. recursively presented, a la 'finitely presented group') theory $\Sigma$ is decidable.
Why? If $\Sigma$ is inconsistent, then $\Sigma$ is decidable, as shown above. Now suppose $\Sigma$ is consistent.
Because $\Sigma$ is recursively enumerable, one can recursively enumerate (i.e. list) all the formal proofs, and these can be checked one-by-one. Because $\Sigma$ is complete, there exists a proof of $\phi$ or of $\lnot\phi$ in this list. Because $\Sigma$ is consistent, if $\lnot\phi$ is a theorem then $\phi$ is not. This constitutes the algorithm. QED.
The issue is that it may not be possible to (even recursively) list axioms for an infinite theory. For instance:
3. "True arithmetic" (i.e. the set of all first-order statements true of the natural numbers in the language of ordered fields) is trivially complete but not decidable.
Real-world examples:
- theory of ordered real-closed fields is consistent, complete and decidable
- theory of algebraically closed fields of fixed characteristic is consistent and decidable, but not complete
- theory of Euclidean fields is not decidable
- first-order theories of finite groups, groups, rings and fields are not decidable