Herbrand's Theorem and Non-Euclidean Geometry

BEESON, Michael, BOUTRY, Pierre et NARBOUX, Julien, 2015. Herbrand's Theorem and Non-Euclidean Geometry. The Bulletin of Symbolic Logic [en ligne]. juin 2015. Vol. 21, n° 2pp. 111-122. [Consultésans date]. DOI 10.1017/bsl.2015.6. Consulté de : https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/herbrands-theorem-and-noneuclidean-geometry/4AF5651CA1E13131D1F9B760D4ADC048We 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.1. .