Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-22T14:35:32.337Z Has data issue: false hasContentIssue false
  • English
  • Français

HERBRAND’S THEOREM AND NON-EUCLIDEAN GEOMETRY

Published online by Cambridge University Press:  04 June 2015

MICHAEL BEESON ,
PIERRE BOUTRY  and
JULIEN NARBOUX
MICHAEL BEESON
Affiliation:
SAN JOSÉ STATE UNIVERSITY SAN JOSE, CA USAE-mail: [email protected]
PIERRE BOUTRY
Affiliation:
ICUBE, UNIVERSITY OF STRASBOURG CNRS, STRASBOURG FRANCEE-mail: [email protected]
JULIEN NARBOUX
Affiliation:
ICUBE, UNIVERSITY OF STRASBOURG CNRS, STRASBOURG FRANCEE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.

Keywords

geometryTarskiEuclidHerbrand’s theoremparallel postulate
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 21 , Issue 2 , June 2015 , pp. 111 - 122
Copyright
Copyright © The Association for Symbolic Logic 2015 

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

Buss, Samuel R., Introduction to proof theory, Handbook of proof theory (Buss, Samuel R., editor), Studies in Logic and the Foundations of Mathematics, vol. 137, Elsevier, Amsterdam, 1998, pp. 1–78.CrossRefGoogle Scholar
Caviness, B. F. and Johnson, J. R. (editors), Quantifier elimination and cylindrical algebraic decomposition, Springer, Wien/New York, 1998.CrossRefGoogle Scholar
Greenberg, Marvin Jay, Euclidean and non-Euclidean geometries: Development and history, fourth ed., W. H. Freeman, New York, 2008.Google Scholar
Gupta, Haragauri Narayan, Contributions to the axiomatic foundations of geometry, Ph.D. thesis, University of California, Berkeley, 1965.Google Scholar
Hartshorne, Robin, Geometry: Euclid and beyond, Springer, Berlin, 2000.CrossRefGoogle Scholar
Kleene, Stephen C., Introduction to metamathematics, van Nostrand, Princeton, NJ, 1952.Google 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, Springer–Verlag, Berlin, 1983. Reprinted 2012 by Ishi Press, with a new foreword by Michael Beeson.Google Scholar
Skolem, T., Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit mathematischer Satzsysteme, nebst einem theoreme über dichte mengen, Selected papers (J. Fenstad, editor), Universiteitsforlaget, Oslo, 1970, pp. 103–136.Google Scholar
Tarski, Alfred, A Decision Method for Elementary Algebra and Geometry, Technical Report R-109, second revised edition, reprinted in [2], pp. 24–84, Rand Corporation, Santa Monica, CA, 1951.Google Scholar
Tarski, Alfred and Givant, Steven, Tarski’s system of geometry. The Bulletin of Symbolic Logic, vol. 5 (1999), no. 2, pp. 175–214.CrossRefGoogle Scholar
Veblen, O., A system of axioms for geometry. Transactions of the American Mathematical Society, vol. 5 (1904), pp. 343–384.CrossRefGoogle Scholar
Plato, Jan von, Terminating Proof Search in Elementary Geometry, Technical Report 43, Institut Mittag-Leffler, Djursholm, 2000/2001.Google Scholar