Sciweavers

LCC
1994

On Herbrand's Theorem

14 years 3 months ago
On Herbrand's Theorem
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 cutelimination, 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.
Samuel R. Buss
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1994
Where LCC
Authors Samuel R. Buss
Comments (0)