On the Euclidean geometry of the double-edged ruler

Abstract

The aim of this note is to show that plane Euclidean geometry can be axiomatised by quantifier-free axioms in languages containing operations that correspond to the geometric constructions that can be performed by a double-edged ruler. The double-edged ruler is an instrument which can be used in the following ways: (i) as a ruler (to draw the line joining two points, as well as to construct the point of intersection of two intersecting lines); (ii) to draw the two parallels to a given line that lie at unit distance from that line; (iii) to draw two parallel lines at unit distance apart, one of which passes through A, the other of which passes through B, whenever the distance between the points A and B, $d(A,B)$, is $≥ 1$ (there are two such pairs of parallels whenever $d(A, B) > 1$). The subject of quantifier-free (universal) axiomatisations of elementary geometry goes back to [4], where plane Euclidean geometry of ruler and segment-transporter constructions was axiomatised by universal axioms in a language containing two quaternary operation symbols and three individual constants, with `points' as individual variables. It was further expanded in [2], [11], and [6]-[10]. The possibility of such axiomatisations is suggested by the well known fact (going back to Puller [11], see also [3]) that the set of points that can be constructed in the standard Euclidean plane by using a double-edged ruler in all three possible ways coincides with the set of points that can be constructed with safer and compass. However, this result does not indicate if and how a quantifier-free axiom system may be set up, for results on the constructibility of points always assume the underlying geometry as `given', whereas in a quantifier-free axiomatisation the geometry itself needs to be determined by axioms that refer to geometric constructions.