- 無矛盾性の証明とは、数学的な体系が矛盾を含まないことを示す証明のことです。
- ゲーデルの不完全性定理によると、自然数論を含むω無矛盾な公理的理論は不完全であり、決定不能な命題が存在します。
- 有限の立場とは、形式主義における「記号の有限的な操作のみから構成される」立場を指します。
- ゲーデルは1931年に有限の立場では自然数論の無矛盾性の証明が成立しないことを示しました。
- ゲンツェンは1936年に有限の立場を少し拡張して超限帰納法を認めることで自然数論の無矛盾性の証明に成功しました。
したがって、無矛盾性の証明が成立するために有限の立場を拡張する必要がある範囲は、少なくとも超限帰納法までであると考えられます。ただし、この拡張も自然数論では許されない方法であり 、さらに高度な体系ではより大きな順序数まで記述する方法が必要になります。
