Points in the plane (unfinished)

Points in the plane

This note is not expected to contain any new mathematical results; it has been written for archival purposes. For a variety of reasons I started earlier this semester with the study of Hilbert's "Foundations of Geometry". One reason was my growing dissatisfaction with the incomplete Euclidean axiomatization I grew up with: I wanted to know how that could be mended. A more important reason was my expectation of conceptual and notational challenges of a possibly different kind than I had met in the last year. Finally I hoped that these exercises would provide me with the opportunity of exploring new styles of proof presentation; for instance, while I was certain that variables of type "point" would be used all over the place, I did not know whether expressions of that type would enter the picture (in traditional texts on geometry they certainly don't).

I was surprised to see that Hilbert's text was so pictorial, and of course I did not like that because the picture does not show the extent to which it is overspecific. It is also very verbal (which made it annoying to have to make do with an English translation):

for instance, it had not even a formal expression - say "p on m" - to state that point p lies on line m . After a few weeks with Hilbert I turned to Coxeter's equally pictorial "In- troduction to Geometry". Here "(abc)" was used to express that the three points a,b,c were distinct an collinear, with b between a and c . The other difference was that, while Hilbert immediately starts with points, lines, and planes, Coxeter showed an axiomatiza- tion that for a long time mentioned points only. (He seemed to follow Veblen and Peano; all that work is now a century old, and it is a sobering thought that in my student days not even their names had penetrated into the curricular.) It was this latter text that inspired me to restrict myself to begin with to variables of type "point".

We obviously have to express the funda- mental notion of collinearity of points, and we shall introduce the boolean function "col" for that purpose, but the first question that presents itself is what type of argument to choose:

• a set of points. With $# .S$ denoting the cardinality of the set $S$ ,we would have

relations like

(0) $# .S \leq 2 \Rightarrow \operatorname{col}.S$ (1) col. $S \land \operatorname{col}T \land # .\left( {{S}{n}T}\right) \geq 2 \Rightarrow \operatorname{col}.\left( {{S}{n}U}\right)$ (2) $S \subseteq T \Rightarrow (\operatorname{col.} S \Leftarrow \operatorname{col.} T)$ .

• unordered triples of points. With $\left( {x,y,z}\right)$ denoting the unordered triple, the essence of (0) would be captured by

(3) col. $\overline{\left( {x,y}\right) }$ collinearity would no longer be defined on the empty set. The analog of (1) would be (4) $\operatorname{col}.\left( {p,q,x}\right) \land \operatorname{col}.\left( {p,q,y}\right) \land p \neq q \Rightarrow \operatorname{col}.\left( {p,x,y}\right)$

It is precisely this "transitivity" that makes it possible to focus on triples for the funda- mental concept. A major drawback is the absence of a canonical representation for the unordered triple.

• ordered triples of points. The fact that, as far as collinearity is concerned, the order is irrelevant has now to be ex-pressed as property of col . With $(x,y,z)$ denoting the ordered triple , we have now (5) $\operatorname{col.}\left( {x,y,z}\right) \equiv \operatorname{col.}\left( {y,x,z}\right) ;\operatorname{col.}\left( {x,y,z}\right) \equiv \operatorname{col.}\left( {x,z,y}\right)$
• the carried version of the previous; instead of col. $(x, y, z)$ , one now writes, with the infix

dot denoting left-associative function applica-tion : col.x.y.z

The last version has the advantage that it does not introduce a new argument type: col's type is $P \rightarrow P \rightarrow P \rightarrow B$ . (NB: These type- formation arrows are right-associative.)

For in retrospect probably not very convincing reasons I did not even try the first possibility. I feared the burden of having to distinguish between a point and the singleton set containing that point as its only element. The second possibility I rejected because of my unfortunate experience with unordered pairs- too often I found myself faced with the need of introducing arbitrary names for "the one" and "the other". With the ordered triples I did many experiments, but the parentheses did not really contribute. Nelly van Gasteren told me of her preference for the carried version, and I think I agree because it does not require a new type.

Our first axiom states that the order of the arguments of col does not matter:

(6) $\left\langle {\forall x,y,z : \operatorname{col.}x.y.z \equiv \operatorname{col.}y.x.z}\right.$

$$ \land \operatorname {c o l}. x. y. z \equiv \operatorname {c o l}. x. z. y $$

the two value-preserving permutations having been chosen in such a way that the remaining ones follow. So we "conclude

(7) col.x.y.z is invariant under any permutation of its arguments.