`Outside' as a primitive notion in constructive projective geometry

DOI10.1007/BF00150870zbMath0846.51001OpenAlexW2009414585MaRDI QIDQ1909592

Dirk van Dalen

Publication date: 29 September 1996

Published in: Geometriae Dedicata (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00150870

zbMATH Keywords

projective planesconstructive projective geometryHeyting's systemJFM 53.0541.01

Mathematics Subject Classification ID

General theory of linear incidence geometry and projective geometries (51A05) Intuitionistic mathematics (03F55)

Related Items

A constructive real projective plane ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE ⋮ Brouwer and Euclid ⋮ Intuitionistic mereology. II: Overlap and disjointness ⋮ Constructive harmonic conjugates ⋮ 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 ⋮ Formalizing constructive projective geometry in Agda

This page was built for publication: `Outside' as a primitive notion in constructive projective geometry