勒布定理

假设算术公理系统 S ，称 P 是 S 的可证性谓词，当且仅当 P 满足以下三个条件：

1. 如果 S⊢ψ ，那么 S⊢P(⌈ψ⌉) ，其中 ⌈ψ⌉ 是 ψ 的哥德尔编码。下文中我们直接用 Pψ 表示 P(⌈ψ⌉) 。

2. S⊢P(ψ→φ)→(Pψ→Pϕ) 。

3. S⊢Pψ→PPψ

可以证明“存在 x 编码了公式 ϕ 的证明”是算术系统 PA 的一个可证性谓词。下文中我们直接令 PA=S ，令 P(x) 为“存在 x 编码了公式 ϕ 的证明”。

在哥德尔第一不完全性定理中，罗瑟(Rosser)定义了一个语句 G ，使得 PA⊬G 且 PA⊬¬G ，进而证明了 PA 不是完全的。这个语句 G 可以简单理解为“ G 不可证”，类似于说谎者悖论。那么如果一个语句陈述自己可以被证呢？即语句 ϕ 满足 ϕ↔Pϕ 。如果这样的语句存在，那么它会有什么样的性质呢？

勒布定理：如果 Pψ→ψ 是 PA 的定理，那么 ψ 是 PA 的定理。

证明： P(x)→ψ 是含有一个自由变元的公式，根据不动点引理，存在公式 φ 满足 φ↔(Pφ→ψ) 。根据条件 3 可得 Pφ→(PPφ→Pψ) ，根据条件 2 可得 Pφ→Pψ ；由于 Pψ→ψ 是 PA 的定理，因此 Pφ→ψ 是 PA 定理，进一步得 φ 是 PA 定理，根据条件 1 可得 Pφ 是 PA 定理，则 ψ 是 PA 定理。因此勒布定理成立。 ⊣

由勒布定理可以轻松推出第二不完全性定理(Kreisel)：如果 PA 一致，令 ⊥ 为矛盾式 0=1 ，那么 ⊢P⊥→⊥ 蕴含 ⊢⊥ ，即 ⊢¬P⊥ 蕴含 ⊢⊥ ，由于假设 PA 一致，因此 ⊬⊥ ，则有 ⊬¬P⊥ ，而 ¬P⊥ 就是“ PA 是一致的”，第二不完全性定理成立。 ⊣