指1931年，美籍奥地利数学家哥德尔(Godel , K.)证明的下列定理:设T是一个包含佩亚诺算术的理论，那幺存在一个语句沪，使得

1.如果T是协调的，那幺T队件

2.如果T是。协调的，那幺T队件事实上如果T是PA(佩亚诺算术)，那幺存在一个语句沪，使得T队沪且T队}}p.PA的协调性是由根岑(Gentzen,G.)于1935年证明的.沪是系统PA的一个语句，但不可证，而且又是一个真的语句.这说明PA是不完全的.这个定理说明直观的算术理论不可能完全形式化，从而，表明形式系统有其固有的局限性.