ヒルベルトの第2問題 1900年

数学が扱っている実数のような超限的な対象の存在はどのようにして保証すれば良いのだろうか。

ヒルベルトはまず超限的な対象に関わる性質を公理として形式的に表現し、つぎにこうして得られた形式体系の無矛盾性を証明 すればよいと考えた。

1931年ゲーデルは不完全性定理を証明し、ヒルベルトが当初考えていた「有限の立場」の範囲内で無矛盾性の証明を おこなうことはできないことを明らかにした。

ゲンツェンは1936年にヒルベルトの「有限の立場」を少し緩め、ある順序数までの 超限帰納法を認めることにより、自然数論の無矛盾性の証明に成功した。

竹内外史はより大きな順序数を記述する方法を開発し、 ゲンツェンの方法を拡張することによって実数論の部分体系の無矛盾性の証明をあたえた。