`Outside' as a primitive notion in constructive projective geometry
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.
- The common point problem in constructive projective geometry
- Simplifying von Plato's axiomatization of constructive apartness geometry
- A constructive real projective plane
- Constructive geometry
- A common axiom set for classical and intuitionistic plane geometry
- Dualitätsprinzipe der Darstellenden Geometrie.
- A system of axioms for geometry.
- Die Einführimg der idealen Elemente in die ebene Geometrie mit Hilfe des Satzes vom vollständigen Vierseit.
- Intuitionistische axiomatiek der projektieve meetkunde.
- Real numbers and projective spaces: intuitionistic reasoning with undecidable basic relations
- A constructive theory of ordered affine geometry
- A common axiom set for classical and intuitionistic plane geometry
- Brouwer and Euclid
- Constructive harmonic conjugates
- Real numbers and projective spaces: intuitionistic reasoning with undecidable basic relations
- The common point problem in constructive projective geometry
- Formalizing constructive projective geometry in Agda
- Implementing Euclid's straightedge and compass constructions in type theory
- A constructive real projective plane
- Constructive geometry and the parallel postulate
- Constructive projective extension of an incidence plane
- Intuitionistic mereology. II: Overlap and disjointness
This page was built for publication: `Outside' as a primitive notion in constructive projective geometry
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1909592)
