希尔伯特是19世纪和20世纪初最具影响力的数学家之一，在严格化的大纷争中，他带领的形式主义派系技压群雄，得到许多当时有名望的数学家的支持。希尔伯特打算通过形式化的手段，将证明抽象成一堆符号的转换。令人惊奇的是这似乎真的可行！为此，希尔伯特希望能够证明：
在任意一个无矛盾的形式系统中，对任意的陈述，都能判断出真伪。
然而，这一企图被哥德尔的博士论文《论数学原理及有关系统中不可判定命题》无情击碎，不完备性定理揭示：
在任意一个无矛盾的形式系统中，存在命题，无法证明其真伪。
这在当时的数学界掀起轩然大波，它不仅具有数学意义，还蕴含着深刻的哲学意义。
不能判断出真伪，自然就想到古老的悖论：这句话是假的（说它真也不行，说它假也不行！）。1905年法国数学家理查德在数学系统中构造出来这样的悖论：
理查兹性也是一个自然数的性质，对应的编号为N，那么N是理查德数吗？
理查德悖论是有瑕疵的：自然数的性质应该是“能被2整除”、“大于100”等，而理查兹性质则把性质和描述性质的语言纠缠在一起了！
罗素和一些人认为如果把对象语言和讨论对象语言的元语言区分开来就能避免这种问题。希尔伯特用精确的形式语言构建的形式公理系统，已经严格区分了数学和元数学，建立起隔离墙，堵住了这个漏洞。哥德尔要想把这个公式是不可证明的放在系统里，必须绕过这堵墙，用数学语言来描述即证明：
在任何相容的形式系统，只要蕴含皮亚诺算术公理，就可以在其中构造在体系中不能被证明的命题，因此通过推演不能得到所有的真命题（即体系是不完备的）。
所谓相容，就是不矛盾，所谓完备，就是所有的真理都能被形式证明，所谓皮亚诺算术公理是指意大利数学家皮亚诺提出的关于自然数的五条公理系统：
根据这五条公理系统可以建立起一阶算术系统。
我们来看哥德尔的证明，首先他将命题映射成自然数，现在搞计算机的一看可能觉得用Unicode不就完了？但是这个论文比计算机早了很多年，可以了解一下哥德尔编码。
G(F)：命题F(x)的哥德尔数。 P(x)：在系统中哥德尔数x对应的命题是可证明的。 SU(z)：对于F(x)有z=G(F)，设y是命题F(G(F))的哥德尔数，则有~P(y)成立。 p：SU(G(SU))。
当问到p是否为真的时候，我们其实就是在问不可证这个特性本身是不可证的吗？这样就造成了矛盾（这是Wikipedia上面给出的）。