希尔伯特纲领 (5-2)

有穷主义有意义的断言不含无界量词断言，而是如 5＋7＝12 这样的关于具体自然数的命题和含有自由变元的无量词命题，如x＋1＝1＋x，这里x＋1＝1＋x 不再是关于自然数的全称性断言，而是关于自然数的一般性模式（Schematic generality)。一个有穷主义一般性模式不应该理解为一个无穷合取，而是看作一个假设判断：对任意给定的自然数n，有n＋1＝1＋n成立。用现代逻辑的术语来说，有穷主义有意义的断言对应于所有Π⁰₁命题。数论中一些命题，如哥德巴赫猜想就是一个Π⁰₁命题。

根据Tait 对有穷主义的分析（Tait 1981），有穷主义数学可由一个一阶算术理论——原始递归算术刻画 PRA 。原始递归算术（Primitive RecursiveArithmetic) PRA 是一个一阶理论。它的非逻辑符号包括一个常元 0 和与每个原始递归函数对应的函数符号。PRA 的公理包括：

1）关于后继函数的公理

S(x) ≠ 0

S(x)＝S(y) → x＝y

2）所有原始递归函数的定义方程

3）Σ⁰₀公式的归纳法

PRA可以表述为一个无量词的理论，称为无量词原始递归算术。我们将 PRA 的无量词版本记为 PRAq⁻ᶠ，它在 PRA 语言中去掉了量词，它的公理由命题逻辑的重言式、等词公理、关于后继函数的公理（同上）和所有原始递归函数的定义方程组成。它的推演规则包括分离规则 MP 和一个归纳规则：从φ(0) 和 φ(x) → φ(S(x))可以得到 φ(x)。

由下面的定理可知，如果我们只考虑Π⁰₂命题，PRA 和它的无量词版本没有本质区别。

定理 1.1. 如果 PRA ⊢ ∀x∃yφ(x，y)，其中 φ 是无量词公式，则可以构造一个项 t(x)，使得PRAq⁻ᶠ ⊢ φ(x，t(x))。

证明，首先证明 PRA 有一个全称公式构成的公理集。将归纳法替换为∀y(φ(0)∧∀x＜y(φ(x) → φ(S(x))) → φ(y))。然后应用 Herbrand 定理。 □

一阶逻辑中的语法概念，包括项、公式、证明等等，都可以被编码为原始递归关系。特别地，我们有一个原始递归函数n ↦♯Sⁿ(0)，称为数码函数。一个原始递归的三元函数Sub(x，y，z)，称为替换函数，它满足：

Sub(♯t，♯υ，♯t')＝♯t(t'/υ)

Sub(♯ф ，♯υ，♯t)＝♯ф(t/υ)

Sub(x，y，z)的直观意思是“将变元 y 在 x 中替换为 z”。我们定义一个特殊的替换函数 su(x，y，z)＝Sub(x，y，num(z))。它是原始递归的。我们也引入相应的函数符号 su 表示它。

对任意一个递归公理化的理论T，“公式序列 Γ 是公式 φ，在 T 中的证明”可以被编码为一个原始递归的关系 Prοοfᴛ(x，y)。

对每个原始递归函数，在PRA中都有一个对应的函数符号表示它，并且所有的原始递归函数在 PRA 中都是可证递归的。因此我们可以在 PRA 中形式化所有语法概念。我们有一个 PRA语言中的公式prfᴛ(x，y)在 PRA 中表示谓词 Prοοfᴛ(x，y)。我们也有一个公式prου(x)：＝∃yPrfᴛ(y，x)表示可证性谓词，我们将它记为□ᴛ(x)。对语言中的语法对象（变元、项、公式等等）σ，我们将S♯σ 0记作 ⌜σ⌝。对公式一个 φ，我们将 □ᴛ(⌜φ⌝) 记作□ᴛφ 。

可以证明PRA满足如下两个可证性条件：

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。