On Herbrand's theorem
SR Buss - International Workshop on Logic and Computational …, 1994 - Springer
International Workshop on Logic and Computational Complexity, 1994•Springer
We firstly survey several forms of Herbrand's theorem. What is commonly called “Herbrand's
theorem” in many textbooks is actually a very simple form of Herbrand's theorem which
applies only to ℬ∃-formulas; but the original statement of Herbrand's theorem applied to
arbitrary first-order formulas. We give a direct proof, based on cut-elimination, of what is
essentially Herbrand's original theorem. The “nocounterexample theorems” recently used in
bounded and Peano arithmetic are immediate corollaries of this form of Herbrand's theorem …
theorem” in many textbooks is actually a very simple form of Herbrand's theorem which
applies only to ℬ∃-formulas; but the original statement of Herbrand's theorem applied to
arbitrary first-order formulas. We give a direct proof, based on cut-elimination, of what is
essentially Herbrand's original theorem. The “nocounterexample theorems” recently used in
bounded and Peano arithmetic are immediate corollaries of this form of Herbrand's theorem …
Abstract
We firstly survey several forms of Herbrand's theorem. What is commonly called “Herbrand's theorem” in many textbooks is actually a very simple form of Herbrand's theorem which applies only to ℬ∃-formulas; but the original statement of Herbrand's theorem applied to arbitrary first-order formulas. We give a direct proof, based on cut-elimination, of what is essentially Herbrand's original theorem. The “nocounterexample theorems” recently used in bounded and Peano arithmetic are immediate corollaries of this form of Herbrand's theorem. Secondly, we discuss the results proved in Herbrand's 1930 dissertation.
Springer