A constructive real projective plane (Q265603)

This article features an axiomatic approach to planar projective geometry that follows the paradigms of informal intuitionistic logic, avoiding the law of excluded middle. This necessitates, for example, axioms like ``For any point \(P\) and any line \(l\), if \(\lnot (P \notin l)\) then \(P \in l\).'' or the assumption that no three tangents at distinct points of a (regular) conic are concurrent. Particular care is also required when defining harmonic conjugates or polar lines: Their constructions must avoid case distinctions as to whether base points coincide or points are on/off a given conic. The structure follows classical axiomatics of projective geometry and covers projectivities, harmonic quadruples, or conics in the sense of Steiner, including Pascal's theorem and polarities in conics. Consistency of axioms is proved by providing a constructive model (the real projective plane) but their independence remains open. The author briefly discusses differences of his model to constructive projective extensions of affine planes. Moreover, he provides sufficient information on constructive mathematics and motivates it, so that his ideas should be accessible to geometricians working in the spirit of classical logic. Large parts of the classical theory are recovered, but some interesting questions remain open: While there is a fundamental theorem for projectivities between lines, a constructive proof of a fundamental theorem for the whole plane is missing. A projectivity between two lines is the product of at most six perspectivities but the exact upper bound is not known (it is three in the classical theory). Finally, a general concept of polarity that is sufficiently general to define conics in the sense of von Staudt is not available. Thus, also the classical equivalence of both definitions still requires a constructive proof.