`Outside' as a primitive notion in constructive projective geometry (Q1909592)

An intuitionistic axiom system for projective planes with only one primitive is given. To the naive observer, the most striking feature of Intuitionism certainly is the renunciation of the ``tertium non datur'', the excluded middle. Therefore the (positive) apartness relation, \(\#\), implies \(\#\), but is not equivalent to \(\#\). Analogously, the relation ``outside'', defined as a positive counterpart of ``incident'', and the relation ``not incident'' in a projective space are not equivalent. The author has chosen to denote the relation ``outside'' also by \(\#\). He uses this as the only primitive, and gives an axiom system, which he proves is equivalent to Heyting's axioms for projective planes [\textit{A. Heyting}, Math. Ann. 98, 491-538 (1927; JFM 53.0541.01)]. To be precise: Heyting gives an axiom system for (3-dimensional) projective space, which has been adapted by the author. Note that the author refers to projective spaces, but his axioms clearly define projective planes only. The author seems to use the phrases Constructivism and Intuitionism synonymously.