完备性、非完备性定理简介*

哥德尔完备性定理: 每一个为真的逻辑公式是可证明的。

其等价表述是: 每一个逻辑公式或者是可满足的(Satisfiable),或者是可证否的(Refutable). 如果一个逻辑公式为真,那么必存在一个形式化证明(Formal Proof).

完备性定理的重要意义在于建立了一阶逻辑的语义真值与语法可证明性之间的联系。同时,也建立了模型论与证明理论之间的联系。

哥德尔的证明(梗概):

哥德尔首先引入Hilbert和Ackermann 1928年论文中的结论: 任意一阶逻辑公式可以转化为前束范式πn(若干个块).

哥德尔又认为前束范式π2(度为1)的完备性等同于前束范式πn的完备性。

最后,哥德尔证明前束范式π2的完备性, 即:任何前束范式π2,要么是可满足的,要么是可证否的。

以稍简单的实例来证明:

φ=x0x1ψ(x0,x1).

定义:

φ0:ψ(x0,x1) φ1:ψ(x0,x1)ψ(x1,x2) φn:ψ(x0,x1)ψ(xn,xn+1).

对于任意的n, 可以分析x0xn+1φn的可满足性。

第一种情况:

如果对于某个n, φn不可满足。 根据命题逻辑的完备性, 可得¬φn是可证明的。 也就是说φ是可证否的。

第二种情况:

如果φn始终是可满足的, 那么在{x0,,xn+1}中可构造出可数个模型(Model)满足所有的φn, 于是φ是可满足的。

哥德尔的完备性证明本质上有个前提, 是紧致性(Compactness)定理。

关于哥德尔的完备性定理, 当前流行的证明方法是亨金(Henkin)的证明

此外, 哥德尔证明中的可满足情形下的模型是可数的, 所以,这个哥德尔的证明本质上也证明了勒文海姆–斯科伦(Löweheim-Skolem)定理。

勒文海姆–斯科伦定理是模型论最基本的定理之一:任何可数的理论如果有一个模型,那么这是一个可数的模型。

哥德尔第一非完备性定理:

任何一致的(Consistent)形式系统P,总是存在P语言中的若干语句不能在P中被证明或证否。

If P is ω-consistent, then there is a sentence which is neither provable nor refutable from P.

换个具体的说法是:

没有一致的公理系统可以证明算术中的所有真命题。

也就是说, 任意支持算术的理论中, 一致性和完备性不可能同时满足。

哥德尔的ω一致概念: P是ω一致的(ω-consistent),如果nP¬φ(n) 蕴含 Pxφ(x).

另一个重要的工具是哥德尔数(G?del Numbering),提供一种将公式转换成自然数的机制。

核心思想是: 公式一旦能转换成自然数,就可以作为参数传递给公式了。

具体地,为每个符号s赋一个固定值#(s).

#(0)=1,#(=)=5,#(¬)=9,

#(1)=2,#(()=6,#()=10,

#(+)=3,#())=7,#(vi)=11+i,

#(×)=4,#()=8,

符号串(或公式)w=w0,,wk对应于

[w]=2#(w0)3#(w1)pk#(wk)

其中pk是第k+1个素数.

哥德尔的不动点(Fixed-Point)定理

如果ϕ(v0)是一个公式,那么一定存在一个公式ψ使得Pψϕ(ψ), 此处 ψ是个对应于ψ自然数编码的公式。

证明(梗概): 令Prf(x,y)(哥德尔原文中用B(x,y))是一个P理论中的公式。

1.n是关于ϕPPrf(n,ϕ)的证明(编码)。

2.那么n一定不是ϕP¬Prf(n,ϕ)的证明(编码)。

现在令Prov(y)(哥德尔原文中用Bew(y))表示公式xPrf(x,y). 根据哥德尔的不动点定理,有这样一个语句ϕ满足:

3.P(ϕ¬(n,ϕ)). 这里ϕ可以理解成"我是不可证明的".

如果Pϕ, 那么根据第1式,存在 n使得PPrf(n,ϕ),于是PProv(ϕ), 再看第3式,就不一致了。

所以,

4.Pϕ.

或者说(结合第4式和第2式), P¬Prf(n,ϕ).

后来, 布鲁斯(George Boolos)简化了哥德尔第一非完备性定理的证明。

哥德尔第二非完备性定理是第一非完备性定理的扩展, 一个简单的表述是:

语言的一致性不能在该语言中被证明。

If P is consistent, then Con(P) is not provable from P.

严谨的哥德尔第二非完备性定理证明由希尔伯特和伯尼斯(Bernays)于1939年给出。

此外, 费弗曼(Feferman)于1960-1961年给出了更简洁的哥德尔第一、第二非完备性定理的严谨证明。