Skip to main content
PRL Project

Constructive Euclidean Geometry


Project Description

We have been interested in developing a constructive version of Euclidean geometry for many years, and we have posted sample material on the PRL project page from time to time. Recently we have made a renewed effort to avoid any use of Markov's principle, with which we have experimented in the past. We have been informed over the years by the stimulating and comprehensive articles by Michael Beeson (see citations) and also by the Coq effort to formalize classical geometry from the very influential book of Tarski, Schwabhauser, and Szmielew [2].

We now believe that we have a sound and purely constructive basis for our formalization of Euclid. We plan to enrich Nuprl with Geogebra, an open source dynamic geometry software, in order to enable interactive construction in Geogebra while Nuprl users complete geometric proofs. We plan to extend this work to develop a pedagogical software that makes the Nuprl/Geogebra combination readily accessible to secondary school students for the purpose of teaching proof and geometric reasoning.

We also see this work as an effort to promote synthetic geometry, and we hope that in due course we will be able to relate Euclidean geometry to our extensive research on the foundations of homotopy type theory .

Project Background and History

The methods for geometric constructions set out in Euclid’s Elements remain a staple of mathematics education and practice despite centuries of advancement in the field of geometry, arguably because of their highly intuitive nature. The ruler and compass constructions in many propositions from the Elements provide an accessible introduction to geometry for novice mathematics students for whom algebraic methods may be too abstract. In fact, the heavy reliance on the analytic approach to geometry that developed after Descartes introduced it in the seventeenth century was a point of contention for some:

“...the synthetic geometers argued that the results gained by the application of algebraic methods could hardly be considered as truly geometrical, for it was evident that in the algebraic manipulation of the equations of geometrical figures it was not possible to follow each one of the geometrical steps corresponding to the algebraic operation. Then, the analytic method not only concealed the geometrical meaning of the results obtained, but also through this method we reached claims without knowing their place among the system of geometrical truths."[1]

A concern for the preservation of a synthetic system of geometry modeled after the Elements coincided with a wider consensus in the mathematical community that the logical gaps in the Elements, such as the assumption that certain geometric configurations are non-degenerate, needed to be addressed. The axiomatic accounts of Hilbert, Pasch, and Peano were given in the nineteenth century with the aim of addressing the logical gaps in the Elements. These accounts provided an informal basis for the formal accounts given later in the twentieth century by Tarksi [2,3] and von Plato [4]. We continue the movement toward formalization with consideration of Brouwer’s intuitionism [5] and the work of Michael Beeson [6], while preserving the synthetic methods from geometry’s inception.

Euclid's Propositions

For now, we share our developments in Nuprl.



We give a visual comparison of the theorem progressions and axioms sets for Tarski, Euclid, and our constructive account.

Education

The typical geometry student in secondary school is found in a unique situation: they are fairly new to the world of algebraic manipulation, they have not yet rigorously exercised their spatial reasoning, and also haven’t been formally introduced to logic or mathematical proof and argumentation. A “synthetics first” approach to geometry pedagogy can support student development of geometric intuition and mathematical argumentation while removing the potentially excessive burden of calculation and algebraic manipulation. Hilbert himself argued

“...geometry as such suffered in the end from the one–sided development of this [coordinate based] method. One calculated exclusively, without having any intuition of what was calculated. The sense for the geometrical figure and for the geometrical construction was lost.[1]

While modern geometry education is equipt with dynamic geometry software allowing students to efficiently explore conjectures, figures, and constructions, it lacks both a substantial consideration of problems that are proof related [7] and a fully synthetic approach. There is therefore a niche to be filled in geometry education: a fully synthetic theorem prover. With such a tool, students can be tasked with focusing on rigorous argumentation about figures only and can have their argumentation checked instantaneously.

References

1. Eduardo N. Giovannini. Bridging the Gap Between Analytic and Synthetic Geometry: Hilbert's Axiomatic Approach. Synthese, 193(1):31-70, 2016.

2. W. Schwabhauser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Teil II: Metamathematische Betrachtungen (Hochschultext), Springer-Verlag, 1983. Reprinted 2012 bt Ishi Press, wish a new foreward by Micahel Beeson.

3. A. Tarski and S.Givant, Tarsk'is System of Geometry, The Bulletin of Sybolic Logic, 5 (1999), pp. 175-214.

4. von Plato, Jan (1995). The axioms of constructive geometry. Annals of Pure and Applied Logic 76 (2):169-200.

5. L.E.J. Brouwer, Contradictority of Elementary Geometry, KNAW Proc., 52 (1949), pp. 315-316.

6. Michael Beeson. Brouwer and euclid. Indagationes Mathematicae , to appear in a special issue devoted to Brouwer, 2017.

7. Ke Wang and Zhendong Su. Automated Geometry Theorem Proving for Human-Readable Proofs. In Proceedings of the 24th International Conference of Artificial Intelligence, IKCAI'15, pages 1193-1199. AAAI Press, 2015.