Mohr-Mascheroni as an axiomatizability statement (Q2770187)

The famous MOHR-MASCHERONI Theorem states that all points that can be constructed with ruler and compass in Cartesian planes over Archimedean ordered Euclidean fields can be constructed with the compass alone.NEWLINENEWLINENEWLINEIn the precisely written paper the author shows that plane Euclidean geometry over Archimedean ordered Euclidean fields can be axiomatized by quantifier-free axioms within algorithmic logic in a language with points as individual variables and a quaternary operation symbol \(\kappa\), with \(\kappa (a,b,c,d)\) and \(\kappa (c,d,a,b)\) denoting -- in arbitrary order -- the intersection points of the circles with centres \(a\) and \(c\) and radii \(ab\) and \(cd\), provided that they exist, and arbitrary points otherwise.