Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-16T05:21:32.419Z Has data issue: false hasContentIssue false
  • English
  • Français

CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE

Published online by Cambridge University Press:  29 March 2016

MICHAEL BEESON
MICHAEL BEESON*
Affiliation:
DEPARTMENT OF MATHEMATICS SAN JOSÉ STATE UNIVERSITY 185 VIEW COURT, APTOS, CA 95003, USAE-mail: [email protected]: www.michaelbeeson.com
Get access Rights & Permissions [Opens in a new window]

Abstract

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean (straightedge-and-compass) geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.

We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom (dating from 1795), which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.

We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions.

Keywords

GeometryintuitionismEuclidconstructive mathematicsTarskiruler and compass
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 22 , Issue 1 , March 2016 , pp. 1 - 104
Copyright
Copyright © The Association for Symbolic Logic 2016 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Avigad, Jeremy, Dean, Edward, and Mumma, John, A formal system for Euclid’s Elements. Review of Symbolic Logic, vol. 2 (2009), pp. 700–768.Google Scholar
Beeson, Michael, Foundations of Constructive Mathematics, Springer-Verlag, Berlin, Heidelberg, New York, 1985.Google Scholar
Beeson, Michael, Constructive geometry, Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008 (Arai, Tosiyasu, editor), World Scientific, Singapore, 2009, pp. 19–84.Google Scholar
Beeson, Michael, Logic of ruler and compass constructions, Computability in Europe 2012 (Barry Cooper, S., Dawar, Anuj, and Loewe, Benedict, editor), Theoretical Computer Science and General Issues, vol. 7318, Springer-Verlag, Berlin, Heidelberg, 2012.Google Scholar
Beeson, Michael, Proof and computation in geometry, Automated Deduction in Geometry (ADG 2012) (Ida, Tetsuo and Fleuriot, Jacques, editors), Springer Lecture Notes in Artificial Intelligence, vol. 7993, Springer-Verlag, Berlin, Heidelberg, 2013, pp. 1–30.Google Scholar
Beeson, Michael, A constructive version of Tarski’s geometry. Annals of Pure and Applied Logic, vol. 166 (2015), pp. 1199–1273.Google Scholar
Bishop, Errett, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967.Google Scholar
Borsuk, Karol and Szmielew, Wanda, Foundations of Geometry: Euclidean and Bolyai-Lobachevskian Geometry, Projective Geometry, North-Holland, Amsterdam, 1960. Translated from Polish by Marquit, Erwin.Google Scholar
Brouwer, L. E. J., Consciousness, philosophy, and mathematics, L. E. J. Brouwer, Collected Works (Heyting, Arend, editor), vol. 1, North-Holland, Amsterdam, 1975, pp. 480–494.Google Scholar
Dehn, Max, Die Grundlegung der Geometrie in historischer Entwicklung, B. G. Teubner, Berlin, 1926. Appendix in [27].Google Scholar
Descartes, René, The Geometry of Rene Descartes, with a facsimile of the first edition, published in 1637 as an appendix to Discours de la Methode, Dover, New York, 1952. Original title, La Geometrie. Facsimile with English translation by Smith, David Eugene and Latham, Marcia L..Google Scholar
Euclid, The Thirteen Books of The Elements, Dover, New York, 1956. Three volumes. Includes commentary by the translator, Sir Heaath, Thomas L..Google Scholar
Euclid, The Bones: A Handy, Where-to-Find-It Pocket Reference Companion to Euclid’s Elements, Green Lion Press, Santa Fe, New Mexico, 2007. Statements and diagrams only, no proofs.Google Scholar
Euclid, The Elements, Green Lion Press, Santa Fe, New Mexico, 2007.Google Scholar
Greenberg, Marvin Jay, Euclidean and non-Euclidean Geometries: Development and History, W. H. Freeman, New York, fourth edition, 2008.Google Scholar
Hartshorne, Robin, Geometry: Euclid and Beyond, Springer, New York, 2000.Google Scholar
Heyting, Arend, Zur intuitionistischen Axiomatik der projectiven Geometrie. Mathematische Annalen, vol. 98 (1927), pp. 491–538.Google Scholar
Heyting, Arend, Axioms for Intuitionistic Plane Affine Geometry, Studies in Logic and the Foundations of Mathematics, vol. 27, 1959, pp. 160–173.Google Scholar
Heyting, Arend, Axioms for intuitionistic plane affine geometry, The Axiomatic Method with Special Reference to Geometry and Physics (Henkin, Leon, Suppes, Patrick, and Tarksi, Alfred, editors), Proceedings of an international symposium, University of California, Berkeley, December 26, 1957-January 4, 1958., North-Holland, 1959, pp. 160–173.Google Scholar
Hilbert, David, Foundations of Geometry (Grundlagen der Geometrie), Open Court, La Salle, Illinois, 1960. Second English edition, translated from the tenth German edition by Unger, Leo. Original publication date, 1899.Google Scholar
Kijne, D., Plane Construction Field Theory, PhD thesis, Rijksuniversiteit te Utrecht, 1956.Google Scholar
Kortenkamp, Ulrich, Foundations of Dynamic Geometry, PhD thesis, Swiss Federal Institute of Technology (ETH), 1999.Google Scholar
Lombard, Melinda and Vesley, Richard, A common axiom set for classical and intuitionistic plane geometry. Annals of Pure and Applied Logic, vol. 95 (1998), pp. 229–255.Google Scholar
Moler, N. and Suppes, Patrick, Quantifier-free axioms for constructive plane geometry. Compositio Mathematica, vol. 20 (1968), pp. 143–152.Google Scholar
Pambuccian, Victor, Axiomatizations of hyperbolic and absolute geometries, Non-Euclidean geometries, János Bolyai Memorial Volume(Prékopa, András and Molnár, Emil, editors). Papers from the International Conference on Hyperbolic Geometry held in Budapest, July 6–12, 2002, Mathematics and Its Applications, vol. 581, New York, 2006, pp. 119–153.CrossRefGoogle Scholar
Pasch, Moritz, Vorlesung über Neuere Geometrie, Teubner, Leipzig, 1882.Google Scholar
Pasch, Moritz and Dehn, Max, Vorlesung über Neuere Geometrie, B. G. Teubner, Leipzig, 1926. The first edition (1882), which is the one digitized by Google Scholar, does not contain the appendix by Dehn.Google Scholar
Schwabhäuser, W., Szmielew, Wanda, and Tarski, Alfred, Metamathematische Methoden in der Geometrie: Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Teil II: Metamathematische Betrachtungen, Hochschultext, Springer–Verlag, 1983. Reprinted 2012 by Ishi Press, with a new foreword by Beeson, Michael.Google Scholar
Tarski, Alfred and Givant, Steven, Tarski’s system of geometry, this Bulletin, vol. 5 (1999), pp. 175–214.Google Scholar
Troelstra, Anne, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, Heidelberg, New York, 1973.Google Scholar
van Dalen, Dirk, Intuitionistic Logic, The Handbook of Philosophical Logic, vol. 3, Dordrecht, Reidel, 1986, pp. 225–339.Google Scholar
van Dalen, Dirk, Heyting and intuitionistic geometry, Mathematical Logic (Petrov, P., editor), Plenum Press, New York, 1990, pp. 19–27.Google Scholar
van Dalen, Dirk, “Outside” as a primitive notion in constructive projective geometry. Geometriae Dedicata, vol. 60 (1996), pp. 107–111.Google Scholar
von Plato, Jan, The axioms of constructive geometry. Annals of Pure and Applied Logic, (1995), pp. 169–200.Google Scholar
von Plato, Jan, A constructive theory of ordered affine geometry. Indagationes Mathematicae, vol. 9 (1998), pp. 549–562.Google Scholar