The common point problem in constructive projective geometry (Q1928390)

In 1959 \textit{A. Heyting} [Studies Logic Found. Math., Axiomatic Method 160--173 (1959; Zbl 0092.25002)] introduced axioms for intuitionistic plane affine geometry, including three axioms the author needed to allow for the existence of the projective extension of any model of the axiom system. In \textit{D. van Dalen} [Nederl. Akad. Wet., Proc., Ser. A 66, 349--368 (1963); Indag. Math. 25, 349--368 (1963; Zbl 0127.11304)], two of Heyting's additional axioms, that were introduced to allow for the intuitionistic construction of the projective extension of an affine plane, were shown to be superfluous. Using results proved in his paper [Beitr. Algebra Geom. 48, No. 2, 547--589 (2007; Zbl 1169.51002)], the author shows that the real plane satisfies all of Heyting's axioms, yet its Heyting projective extension does not satisfy constructively the statement that any two lines have a point in common, as this statement implies that for any real number \(\alpha\) either \(\alpha\leq 0\) or \(\alpha\geq 0\), which is not intuitionistically valid.