Brouwer and Euclid
From MaRDI portal
Publication:1688971
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3899653 (Why is no real title available?)
- scientific article; zbMATH DE number 3485716 (Why is no real title available?)
- scientific article; zbMATH DE number 218495 (Why is no real title available?)
- scientific article; zbMATH DE number 3215147 (Why is no real title available?)
- scientific article; zbMATH DE number 3216177 (Why is no real title available?)
- scientific article; zbMATH DE number 5203535 (Why is no real title available?)
- scientific article; zbMATH DE number 3056548 (Why is no real title available?)
- scientific article; zbMATH DE number 3062923 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- scientific article; zbMATH DE number 3074068 (Why is no real title available?)
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- A common axiom set for classical and intuitionistic plane geometry
- A constructive real projective plane
- A constructive version of Tarski's geometry
- Constructive Coordinatization of Desarguesian Planes
- Constructive geometry
- Constructive geometry and the parallel postulate
- Constructive projective extension of an incidence plane
- Finding proofs in Tarskian geometry
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Tarski's System of Geometry
- The axioms of constructive geometry
- The common point problem in constructive projective geometry
- `Outside' as a primitive notion in constructive projective geometry
Cited in
(5)- A direct proof of the Steiner-Lehmus theorem
- Implementing Euclid's straightedge and compass constructions in type theory
- Lippmann's axiom and Lebesgue's axiom are equivalent to the Lotschnittaxiom
- A common axiom set for classical and intuitionistic plane geometry
- 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)