Oberseminar "Mathematische Logik" - Luisa Després

Herbrand's theorem is a well-known logical theorem about the realizability of first-order formulae in a suitable universe. In the context of (Tarski's axiomatization of) Euclidean geometry, it has been used 'negatively' by Beeson, Boutry and Narboux to show the underivability of the parallel axiom from a first-order version of the other axioms. This talk discusses a 'positive' application of Herbrand's theorem: the extraction of computational content from proofs in geometry. As a case study, it presents the extraction of a Herbrand disjunction for the Outer Pasch theorem from its proof by Schwabhäuser, Szmielew and Tarski. It turns out that this extraction can be done in a modular way. The talk explores why this is likely to be possible for most proofs in geometry, in contrast to the generally bad behaviour of Herbrand's theorem in connection with the modus ponens rule. The talk is based on a bachelor thesis supervised by Prof. U. Kohlenbach and a submitted paper: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/Despres-Kohlenbach.pdf.