Quantifier-free axioms for constructive affine plane geometry (Q1840989)

In the spirit of \textit{N. Moler} and \textit{P. Suppes} [Compositio Math. 20, 143-152 (1968; Zbl 0183.24902)], which started the programme of constructive axiomatizations of various geometries, the author provides quantifier-free (constructive) axiom systems for fragments of first-order affine geometry. The first of these is expressed in a language with a ternary collinearity predicate and two binary operations, the midpoint and the point-reflection operation. The midpoint operation, as well as some of the axioms have been first used in a non-constructive setting by \textit{W. Szmielew} [From affine to Euclidean geometry. D. Reidel Publishing Co., Dordrecht-Boston; PWN Warsaw (1983; Zbl 0516.51001)]. For the second axiom system the language is enlarged with the ternary betweenness relation, the quaternary affine congruence relation, and the quaternary trapezoid operation \(Z\) (if \(a,b,c\) form a triangle, and \(v\) is distinct from \(a, b, c\) and collinear with \(b\) and \(c\), then \(Z_v(abc)\) is the intersection point of the parallel from \(c\) to \(ba\) with \(va\), otherwise an arbitrary point). The task of providing representation theorems for these axiom systems, i.\ e.\ theorems that describe algebraically up to isomorphism the classes of models of the axiom systems, is left open. Theorem 13 is not meant to be read as a representation theorem.