在对一阶形式理论及其模型的研究中， Godel 的不完全性定理，被认为是二十世纪最重要的数学定理。它深刻地揭示了语法及语义的关系，对数学以及哲学、认识论都有深刻的影响。重要结果之一，就是否定了 Hilbert 关于将一切数学领域形式化的所谓 " Hilbert 纲领 "。 Godel 定理断言： 对任一足够复杂的一阶理论，都存在一个形式语句A ,T推不出A , 也推不出A。 　　为了比较具体详细地介绍 Godel 不完全性定理，有必要介绍一个特殊的形式理论系统Z1。Z1 是一个比初等算术的形式理论"稍微大一点"的形式理论，我们将在Z1 上介绍和证明 Godel 不完全性定理。 　　Z1 可以理解成关于非负整数的一个形式理论，它的语言L中的谓词是R1(x,y,z) 及R2(x,y,z) ，分别表示 加法关系x+y= z 和乘法关系 x·y = z 。（注意到函词可以用谓词来定义）常项集合只含 0 和 1 。为简便计，约定!A(x) 是公式 xy( A(x) ∧(A(y)→x = y ) ) ，意思是存在一个唯一的元素 x ，使A(x) 成立。 　　Z1 的公理： 　　（1）x,y!z ( x +y = z ) 　　（2）x,y!z (x · y = z ) 　　（3）x ( x + 0 = x∧x · 1 = x ) 　　（4）x, y ( x+ ( y + 1) = (x+y) + 1 ) 　　（5）x, y ( x · (y+1) = x · y + x ) 　　（6）x, y ( x + 1 = y + 1→x = y ) 　　（7）x (( x + 1 = 0) ) 　　（8）令 A(x, t1 ,t2 ,..,tk ) 是 L 中的任一公式，含 x 作为自由变元，< t1 ,t2 ,..,tk > 可以是空集，则t1 ,t2 ,..,tk [(A(0, t1 ,t2 ,..,tk )∧y ( A(y, t1 ,t2 ,..,tk )→A(y+1, t1 ,t2 ,..,tk )))→x A(x, t1 ,t2 ,..,tk ) ] 　　第（8）款实际上包含无穷条公理，也称为公理模式。读者可以发现，它实际上是通常使用的归纳法的形式化。