Gödel 不完备定理

哥德尔不完备定理
术语名称	哥德尔不完备定理
英语名称	Gödel's incompleteness theorem
别名	哥德尔不完全定理, 哥德尔不完备性定理, 哥德尔不完全性定理

Gödel 不完备定理(Gödel's incompleteness theorem)是一个著名定理：向一阶逻辑演算中加入一阶算术系统公理后，得到的理论是不完备的。

定理

Gödel 第一不完备定理

包含了一阶算术系统（如 Peano 公理）的一阶逻辑理论，如果是一致的，则不是完备的。即一阶逻辑演算包含一阶算术系统后，如果不允许任意一对矛盾同时可证明，则存在一对矛盾同时不可证明（即同时 [math]\displaystyle{ T\nvDash s }[/math] 且 [math]\displaystyle{ T\nvDash \lnot s }[/math]）。

Gödel 第二不完备定理

包含了一阶算术系统的一阶逻辑理论，且这一理论是一致的，则无法以算术系统本身为工具判定系统的一致性。

具体来说：

• 形式系统 [math]\displaystyle{ T }[/math] 。
• 通过某种任意的方式将公式的演算编码为系统内的算术，称为公式的哥德尔数(Gödel number)，记作 [math]\displaystyle{ \ulcorner \phi \urcorner }[/math] ，是一个从公式到哥德尔数的映射。
• 判定其是否可证明的一元谓词 [math]\displaystyle{ \operatorname{Prov}_T() }[/math] ，与一个哥德尔数一同构成新的公式，可以看成一个从哥德尔数到公式的映射。

则作为判定规则，应满足 Hilbert–Bernays 条件(Hilbert–Bernays conditions)：

• 若 [math]\displaystyle{ T\vdash\phi }[/math] 则 [math]\displaystyle{ T\vdash\operatorname{Prov}_T(\ulcorner\phi\urcorner) }[/math] 。
• [math]\displaystyle{ T\vdash\operatorname{Prov}_T(\ulcorner\phi\rightarrow\psi\urcorner)\rightarrow(\operatorname{Prov}_T(\ulcorner\phi\urcorner)\rightarrow \operatorname{Prov}_T(\ulcorner\psi\urcorner)) }[/math] 。
• [math]\displaystyle{ T\vdash\operatorname{Prov}_T(\ulcorner\phi\urcorner)\rightarrow \operatorname{Prov}_T(\ulcorner\operatorname{Prov}_T(\ulcorner\phi\urcorner)\urcorner) }[/math] 。

则命题 “[math]\displaystyle{ T }[/math] 是一致的”记作 [math]\displaystyle{ \mathrm{Con}_T }[/math] 必然有 [math]\displaystyle{ T\nvdash\mathrm{Con}_T }[/math] 。

与完备性定理的关系

• Gödel 完备性定理说明了逻辑公理和规则本身是一致且完备的。而第一不完备定理描述向其中增加新的非逻辑符号和公理后，得到的理论是不完备的，新增非逻辑符号后能表达的新公式中出现了无法通过新旧公理及推理规则推出的。
• 比 Gödel 完备性定理更强的模型存在定理说明了一致的理论必然存在模型；而对于一阶算术系统引入的非逻辑符号，新公式可能独立于这些公理所产生的理论，其不同的真值实际对应着不同的两类模型，而这些模型是一阶逻辑的表达能力无法区分的。根据语言本身的可靠性，只有有效的才是能推理出的，这些公式在不同模型中有不同表现，不可能通过语言本身的形式推理出。
  • 完备性定理中的前提 [math]\displaystyle{ T \vDash s }[/math] ，定义为任意模型/赋值中 [math]\displaystyle{ \sigma\vDash T }[/math] 则 [math]\displaystyle{ \sigma\vDash s }[/math] 。而这里不同模型中满足情况不同，既不总是有 [math]\displaystyle{ \sigma\vDash s }[/math] 也不总是有 [math]\displaystyle{ \sigma\vDash \lnot s }[/math] 。所以前提在这种情况下的真值是假。

与 Hilbert 纲领的关系

第二不完备定理说明了包含算术系统的理论不可能通过算术系统本身证明本身的一致性，必须借助比该系统本身更强有力的元理论。

证明论
研究动机与结果	Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理
结构化证明	推理系统 形式化公理系统 （形式化、公理化）	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
		Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
		Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
	证明、演绎	演绎、可演绎、证明、可证明
	命题、定理	命题、元命题、公理/公理模式、定理、元定理
	推理规则性质描述	保存真实性、保存重言性
	推理系统性质描述	可靠性、完备性/完全性、一致性、独立性
	重要元定理	演绎定理、切消定理（切割消除定理）
		（某种推理系统的）可靠性定理、完备性定理
序数分析	证明论序数
构造性证明 程序化证明	Curry–Howard 对应
	证明复杂度理论	证明复杂度