竹内氏の推測

数学において、竹内予想は、二階述語論理の連続形式化にはカット除去が存在するという竹内ガイシの予想である(Takeuti 1953)。この予想は肯定的に解決された。

• Taitによる、 Schütte (Tait 1966)の研究に基づいて、カット除去を証明する意味論的手法を使用する。
• Prawitz (Prawitz 1968) と Takahashi (Takahashi 1967)がそれぞれ独立に同様の手法で証明した (Takahashi 1967)。ただし、Prawitz と Takahashi の証明は 2 階論理に限定されず、高階論理一般に関するものである。
• これは、Jean-Yves GirardによるSystem Fの強正規化の構文的証明の帰結です。

竹内予想は、各ステートメントが原始再帰算術(PRA)の弱いシステムで互いに導出できるという意味で、2階算術の1一貫性と同等です。また、ジラール/レイノルドのシステムFの強い正規化と同等です。

• ヒルベルトの第二問題

• Dag Prawitz、1968年。「高階論理のための基本原則」Journal of Symbolic Logic、33:452–457、1968年。
• ウィリアム・W・テイト、1966年。「第二階述語論理に対するゲンツェンの主定理の非構成的証明」アメリカ数学会報、72:980-983。
• 竹内外司、1953年。一般化された論理計算について。日本数学会誌、23:39–96。この論文の訂正は、同誌24:149–156、1954年に掲載された。
• 高橋素夫, 1967. 単純型理論におけるカット消去の証明.日本数学会誌, 10:44–45.