On Herbrand's Theorem
On Herbrand's Theorem
复制标题
DOI：
10.1007/3-540-60178-3_85
复制
发表时间：
1994-10
期刊：
影响因子：
--
通讯作者：
S. Buss
中科院分区：
文献类型：
--
作者：
S. Buss
我们首先考察赫布兰德定理的几种形式。许多教科书中通常所说的“赫布兰德定理”实际上是赫布兰德定理的一种非常简单的形式，仅适用于ℬ∃-公式；但赫布兰德定理的原始陈述适用于任意一阶公式。我们基于割消法给出了本质上赫布兰德原始定理的直接证明。最近在有界算术和皮亚诺算术中使用的“无反例定理”是这种形式的赫布兰德定理的直接推论。其次，我们讨论赫布兰德1930年论文中证明的结果。
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.