在对一阶形式理论及其模型的研究中, Godel 的不完全性定理,被认为是二十世纪最重要的数学定理。它深刻地揭示了语法及语义的关系,对数学以及哲学、认识论都有深刻的影响。重要结果之一,就是否定了 Hilbert 关于将一切数学领域形式化的所谓 " Hilbert 纲领 "。 Godel 定理断言: 对任一足够复杂的一阶理论,都存在一个形式语句A ,T推不出A , 也推不出A
  为了比较具体详细地介绍 Godel 不完全性定理,有必要介绍一个特殊的形式理论系统Z1Z1 是一个比初等算术的形式理论"稍微大一点"的形式理论,我们将在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)款实际上包含无穷条公理,也称为公理模式。读者可以发现,它实际上是通常使用的归纳法的形式化。