K.ゲーデル（オーストリア→アメリカ）は以下の不完全性定理を発表した。
「公理体系Pが無矛盾であれば、ある論理式Aで、AもAの否定も証明不能なものが存在する。すなわち、決定可能（decidable）でない」
これから、「Pが無矛盾であれば、Pの無矛盾性の証明の有限的な方法を与えることはできない」も示される。
この定理は、数学を有限の手続きで公理論的に展開しようとしていた形式主義に致命的な打撃を与えた。
しかし、数学にとっては致命的ではないことを注意しておきたい。基礎があるということと有用であるということは別のことなのである。