Brouwer and Euclid

DOI10.1016/j.indag.2017.06.002zbMath1437.03171arXiv1705.08984OpenAlexW2963020477MaRDI QIDQ1688971

Michael J. Beeson

Publication date: 12 January 2018

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1705.08984

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Euclidean geometries (general) and generalizations (51M05) Intuitionistic mathematics (03F55)

Related Items

Implementing Euclid's straightedge and compass constructions in type theory ⋮ A direct proof of the Steiner-Lehmus theorem ⋮ Why did Euclid not need the Pasch axiom? ⋮ Lippmann's axiom and Lebesgue's axiom are equivalent to the Lotschnittaxiom

Cites Work

• A constructive real projective plane
• A constructive version of Tarski's geometry
• A common axiom set for classical and intuitionistic plane geometry
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• The common point problem in constructive projective geometry
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Finding proofs in Tarskian geometry
• Constructive Coordinatization of Desarguesian Planes
• Tarski's System of Geometry
• CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
• Constructive projective extension of an incidence plane
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item