1、贝里悖论

“不可描述的感觉”，这个词本身描述了一种感觉，但它又说这种感觉是不可描述的，这里存在矛盾。

贝里悖论是由英国的图书管理员贝里发现的，它和上面的例子类似。“不能用少于20个字确定的最小自然数”，这句话确定了一个自然数，但它本身又少于20个字，说明这个自然数能被少于20个字确定。

2、哥德尔定理

数学命题不是真的就是假的，或者说不是正确的就是错误的。以往认为，对于真的命题我们总能证明它，即使我们暂时还证明不了，但理论上这样的证明总是存在的。哥德尔定理表明，存在着真的但又无法证明的命题。

哥德尔在1931年实际上证明了，存在正确的算术命题，而这命题无法在算术中得到证明。麻省理工学院的逻辑学教授George Boolos于1989年给出哥德尔定理的一种新证明，这种新的证明参考了贝里悖论。

3、新证明的思路

“不能用少于20个字确定的最小自然数”，这句话不是数学命题。但Boolos将这句话翻译成算术命题，并且得到，这个命题是真的但无法在算术上证明它。和贝里悖论不同，这命题在数学上并不会导致矛盾。证明的思路如下。

Boolos首先给出“确定”这个概念的数学定义：

公式G(x)确定自然数m，当且仅当，∀x(G(x)↔x=m)是定理，即它可以在算术系统中证明。

按照这个定义，2x=4确定2，因为能够证明∀x(2x=4↔x=2)。

Boolos然后构造出公式F(x)：

∃y(y=10k∧A(x,y))

它的意思是：x是不能用长度小于10k的公式确定的最小自然数（这个公式的细节在后面解释）。而公式F(x)本身的长度又小于10k。所以F(x)本质上和贝里的那个句子相同。

令n是长度小于10k的公式无法确定的最小自然数，则∀x(F(x)↔x=n)是真的。

由于F(x)的长度小于10k，所以n无法由F(x)确定。按照确定的定义， ∀x(F(x)↔x=n)不是定理。

所以，∀x(F(x)↔x=n)是正确的算术命题，但无法在算术系统中证明。

4、证明的细节

(1)公式及其长度

公式由联结词、量词、运算符、谓词、个体常元、个体变元和括号按合适的方式组合而成。公式的长度就是公式包含的符号数。

联结词：﹁，→,  ∧，∨，↔

量词：∀，∃

运算符：+，x

谓词：=

个体常元：0，S0，S00，……

个体变元：x，x’，x’’，……

括号：(，)

一共有16个符号。

说明，上面的0就是通常的0，而通常的1用S0表示，2用S00表示……。为了方便，后面仍用通常的表示方法，但要清楚它实际上是上面的符号。同样，为了方便我们用y和z表示变量x’和x’’。

举个例子，∀x(x+1=y)是公式。这个公式的长度不是9，而是11。因为1是S0，y是x’。

由于只有16个符号，对任一个自然数i，只有有限个长度为i的公式，也只有有限个长度小于i的公式。

(2)“确定”的性质

如前面所述，“确定”的定义是这样的：

公式G(x)确定自然数m，当且仅当，∀x(F(x)↔x=m)是定理，即它可以在算术系统中证明。

容易证明，一个公式最多确定一个自然数。又由于只有有限个长度小于i的公式，所以存在不能被长度小于i的公式确定的自然数，而这些自然数中又有一个是最小的。即不能被长度小于i的公式确定的最小自然数是存在的。

(3)F(x)的展开

为什么∃y(y=10k∧A(x,y))表示 “x是不能用长度小于10k的公式确定的最小自然数”呢？

这里需要把A(x,y)展开。

先引入C(x,z)，C(x,z)表示“x可被某个长度为z的公式确定”。

令B(x,y)为∃z(z<y∧C(x,z))，它表示“x可被某个长度小于y的公式确定”。

令A(x,y) 为﹁B(x,y) ∧∀a(a<x→B(a,y))，它表示“x是不能被长度小于y的公式确定的最小自然数”。

F(x)是∃y(y=10k∧A(x,y))，即“x是不能被长度小于10k的公式确定的最小自然数”，其中k是A(x,y)的长度。

F(x)的长度是多少呢？10的长度是11，k的长度是k+1，A(x,y)的长度为k，其他为9，所以F(x)的长度是2k+21。因为k大于3，所以2k+21<10k。所以F(x)的长度小于10k。

 证明还没有完成，C(x,z)还需要进一步展开，或者需要证明C(x,z)能用算术公式表达。Boolos认为，利用哥德尔编码技术，C(x,z)能够用算术公式表达。不过他省略了具体的证明，这里的证明应该是和哥德尔的原始证明类似的。