定理7.6.1
  (Godel 不完全性定理) 若Z1是协调的,则存在Z1的一个语句A,在Z1AA都不可能形式证明。

  引理7.6.1
  对任一递归函数r , 关系Rr在Z1中是可定义的。

  引理7.6.2
  对任一递归函数r,关系Rr是一个递归关系。
  证明是容易的。

  引理7.6.3
  令A(x)是Z1的一个公式,[A(X)] = m 是它的 Godel 数,n 是一个整数,代表某一个项t,则 Sub( m , n ) = Sub( [A(x)], [t]) = [A(t)]

  引理7.6.4
  (对角线定理) 令(x)是Z1的语言L的任一个公式,它的唯一的自由变元是x,则存在语句y,使得
   Z1│-ψ([ψ])

  定理7.6.2
  (Godel的第二不完全性定理) 令CON(Z1) 表示Z1是协调的。通过编码,CON(Z1) 可以表达为Z1的一个形式公式,某一Z1的语句y在Z1中不可证明。(如果Z1不协调,任何公式都在Z1中可证。)
  实际上,y与CON(Z1)是等价的。
  定理7.6.3
  
(广义Godel 不完全性定理)
  令T是任何一个理论,它的公理是归纳地给出的,同时原始递归函数在T中可以定义,那么,若T协调,则
  (1)存在语句A ,AAT中都不可证。
  (2)CON(T)在T中是不可证的。