Brouwer and Euclid

DOI10.1016/J.INDAG.2017.06.002zbMATH Open1437.03171arXiv1705.08984OpenAlexW2963020477MaRDI QIDQ1688971FDOQ1688971

Authors: Michael Beeson 

Publication date: 12 January 2018

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

Abstract: We explore the relationship between Brouwer's intuitionistic mathematics and Euclidean geometry. Brouwer wrote a paper in 1949 called "The contradictority of elementary geometry". In that paper, he showed that a certain classical consequence of the parallel postulate implies Markov's principle, which he found intuitionistically unacceptable. But Euclid's geometry, having served as a beacon of clear and correct reasoning for two millenia, is not so easily discarded. Brouwer started from a "theorem" that is not in Euclid, and requires Markov's principle for its proof. That means that Brouwer's paper did not address the question whether Euclid's "Elements" really requires Markov's principle. In this paper we show that there is a coherent theory of "non-Markovian Euclidean geometry." We show in some detail that our theory is an adequate formal rendering of (at least) Euclid's Book~I, and suffices to define geometric arithmetic, thus refining the author's previous investigations (which include Markov's principle as an axiom). Philosophically, Brouwer's proof that his version of the parallel postulate implies Markov's principle could be read just as well as geometric evidence for the truth of Markov's principle, if one thinks the geometrical "intersection theorem" with which Brouwer started is geometrically evident.

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

Recommendations

• scientific article; zbMATH DE number 3628886
• Euclid and his modern rivals
• scientific article
• scientific article; zbMATH DE number 51594
• scientific article; zbMATH DE number 3891296
• Euclid: Rhetoric in Mathematics

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• 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
• Constructive Coordinatization of Desarguesian Planes
• A constructive real projective plane
• Constructive geometry
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructive projective extension of an incidence plane
• Title not available (Why is that?)
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Title not available (Why is that?)
• Tarski's System of Geometry
• Title not available (Why is that?)
• Title not available (Why is that?)
• Finding proofs in Tarskian geometry
• A constructive version of Tarski's geometry
• Constructive geometry and the parallel postulate
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (5)

• A common axiom set for classical and intuitionistic plane geometry
• A direct proof of the Steiner-Lehmus theorem
• Lippmann's axiom and Lebesgue's axiom are equivalent to the Lotschnittaxiom
• Implementing Euclid's straightedge and compass constructions in type theory
• Why did Euclid not need the Pasch axiom?

This page was built for publication: Brouwer and Euclid

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688971)