Version: v1, Published online: 1998
Retrieved April 25, 2024, from https://www.rep.routledge.com/articles/thematic/herbrands-theorem/v-1
Article Summary
According to Herbrand’s theorem, each formula F of quantification theory can be associated with a sequence F1, F2, F3,… of quantifier-free formulas such that F is provable just in case Fn is truth-functionally valid for some n. This theorem was the centrepiece of Herbrand’s dissertation, written in 1929 as a contribution to Hilbert’s programme. It provides a finitistically meaningful interpretation of quantification over an infinite domain. Furthermore, it can be applied to yield various consistency and decidability results for formal systems. Herbrand was the first to exploit it in this way, and his work has influenced subsequent research in these areas. While Herbrand’s approach to proof theory has perhaps been overshadowed by the tradition which derives from Gentzen, recent work on automated reasoning continues to draw on his ideas.
Ungar, A.M.. Herbrand’s theorem, 1998, doi:10.4324/9780415249126-Y004-1. Routledge Encyclopedia of Philosophy, Taylor and Francis, https://www.rep.routledge.com/articles/thematic/herbrands-theorem/v-1.
Copyright © 1998-2024 Routledge.