:设T是一个包含佩亚诺算术的理论，如果T是协调的，那幺T}f ConT，其中Con二是一个表示T是协调的语句.该定理表明，一个形式系统的协调性是不能在这个系统内部证明的.换句话说，要想证明它的协调性，必须找一个更强的形式系统.德国数学家希尔伯特(Hil6ert,D.)原打算用有穷方法证明古典数学的无矛盾性，但后来哥德尔得到了不完全性定理，它表明只用有穷方法不能得到无矛盾性的证明.这对希尔伯特的构想是一个很大的打击，后来只得放宽对证明的要求.