Herbrand's theorem and non-Euclidean geometry

Michael Beeson, Pierre Boutry, Julien Narboux

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 constru…