定理7.6.1 　　（Godel 不完全性定理） 若Z1是协调的，则存在Z1的一个语句A，在Z1中A及A都不可能形式证明。 　　引理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 ,A及A在T中都不可证。 　　(2)CON(T)在T中是不可证的。