希尔伯特纲领 (5-3)

D₁：如果T ⊢ φ那么PRAF ⊢ □ᴛφ：

D₂：PRA ⊢ □ᴛ(φ → ф) → (□ᴛφ →□ᴛф)。

我们也定义一个特殊的表达可证性的公式。令φ 为 PRA 的语言中的一个公式，且 φ 中的自由变元恰好是x₁，...，xₙ 。定义公式□ᴛ[φ]为：

□ᴛ[φ]：＝□ᴛ(su(...su(su(⌜φ⌝，⌜x₁⌝, x₁)，⌜x₂⌝，x₂)...，⌜xₙ⌝，xₙ))

□ᴛ[φ] 与 φ 有相同的变元 x₁，...，xₙ 。如果 φ 是一个闭公式，则 □ᴛ[φ]＝□ᴛφ 。

引入□ᴛ [φ] 的作用是证明“可证 Σ₁-完全性”：

引理 1.2.（可证 Σ₁ 完全性）对任意 Σ₁ 公式φ，PRA ⊢ φ → □ᴛ[φ] 。

由“可证Σ₁-完全性”可以得到第三可证性条件：

D₃：PRA ⊢ □ᴛφ → □ᴛ□ᴛφ 。

根据 Tait 的论证，原始递归算术是能够形式化所有形式系统的语法概念的最弱的理论，任何非平凡的数学推理都需要预设 PRA 中的概念。如果有一种数学哲学立场怀疑 PRA 中推理的可靠性，我们可以将这种立场所承认的数学推理形式化为一个公理系统 A，但是 A 中的语法推演已经预设了PRA 中的概念，如果有这种立场的人怀疑 PRA 中推理的正确性那么他就无法做出任何数学推理。因此，PRA 是在笛卡尔怀疑论的基础上的“绝对可靠的”的数学基础。即便我们不承认康德意义上的直观可以为有穷主义数学的可靠性提供保证，我们也没有更好的理由去怀疑 PRA 中推理的正确性。

通过对语法编码的更细致的分析，上述的语法概念都可以用初等递归函数¹来编码，我们可以在一个比原始递归算术更弱的系统──初等递归算术 ERA² 中建立起所有的语法概念。ERA 的可证递归函数恰好是初等递归函数。因此ERA 也被看作严格有穷主义的形式化。不过 Tait 论证对 ERA 仍然有效。

1.3 一致性证明

在形式主义的观点下，希尔伯特将无穷视为“理想元”，是用来帮助我们更高效的推演出关于具体有限对象的工具。如复数、几何中的无穷远点。引入这种“理想元”的唯一要求就是不会发生矛盾。希尔伯特将包含理想元的数学称为“理想数学”，为了替理想数学的合法性辩护，并且回应直觉主义者对古典数学的诘难，希尔伯特希望使用绝对可靠的有穷主义方法来证明无穷数学是无矛盾的。希尔伯特纲领的目标就是使用有穷主义方法证明理想数学的一致性。这样希尔伯特纲领可以分为两步来实施：

（1）将理想数学形式化为一个公理系统 T；

（2）使用有穷主义方法 F 来证明系统 T 的一致性。

一致性本身是一个Π⁰₁句子：Conᴛ ≡ ∀x ¬ Prοοfᴛ(x，⌜0＝1⌝)，其中0＝1代表矛盾式。因此 T 一致性是一个属于有穷数学的命题。（2）是在有穷数学内部对一个有穷数学中的命题的证明。

根据我们在上一节中对有穷主义数学的形式化，我们可以更深入探讨证明一致性的意义。事实上，一致性等价于Π⁰₁-反射原理。

─────

¹初等递归函数类是由常值零函数、后继函数、投影函数、加法函数、乘法函数、截断减法函数和指数函数 2ˣ通过复合、有界和、有界积生成的最小函数类

²ERA是语言L＝{0，S，＋，·，exp} 中的一阶理论，它的公理由鲁滨逊算术 Q、Δ₀-归纳公理模式和关于指数函数的递归定义公理构成。

设 S 是任意包含 PRA 的理论，我们将它看作是有穷主义数学的形式化。令T是一个包含S的递归可公理化的理论，我们将它看作是理想数学的形式化。

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