ヒルベルトのテーゼについて【数学はFOLで形式化できるか】

ヒルベルトのテーゼとは

Hilbertのテーゼは、

数学における証明可能性は一階述語論理(First-Order Logic)における形式的な証明可能性によって捉えられる

という主張です。一階述語論理は以下FOLとしましょう。

「数学における証明可能性」というものは人間が経験を通してしか知ることのできないインフォーマルなものです。

数学と証明は切っても切り離せませんから、いくつも証明問題を解いて、いくつもの教科書の証明を追ってとしているうちに自然に証明とは何かを理解した気になれています。

しかし、証明するとはどういうことかをきちんと定義できていないと困る数理論理学においては「なんとなくわかっている」ではだめです。証明ができるとはこれこれこういうことだとはっきり書けないと困るわけです。

そこで、FOLにおいて証明可能とはこういうことだと定義することになります。HilbertやGentzenがそれぞれ異なった証明可能性の定義を与えています（それらは同値になることが知られているのですが）。

しかし、その定義が「数学における証明可能性」を厳密に捉えているかどうかは最終的には信頼するしかない。なぜなら、「数学における証明可能性」はインフォーマルなものなのですから正確に捉えようと努力する以上のことはできません。

そこで、「FOLにおける証明可能性の定義が数学における証明可能性の定義として妥当だと認めようじゃないか」という主張がヒルベルトのテーゼです。

Hilbertのテーゼというと「数学は集合論で形式化できる」という主張だと解されることがあります。

しかし、Berkは博士論文において「数学は集合論で形式化できる」という主張をHilbertのテーゼと呼んだり、Hilbertのテーゼに含まれていると考えることに批判的な態度を示しているそうです[1]。

あくまでHilbertのテーゼは「証明可能性」を捉えることによって数学を捉えようとするもので、集合論は別問題だということなのでしょう。

たしかに集合論は現代数学において極めて重要な位置を占めますが、「数学は集合論で形式化できる」という主張をHilbertに帰することはできないということです。

BarwiseはHilbertのテーゼが２階層からなると解説しているそうです[1]。

第１階層は先ほど述べた「FOLにおける証明可能性の定義が数学における証明可能性の定義として妥当だと認めようじゃないか」という主張です。これはどこまで行っても信頼するしかないものです。

第２階層は「数学的に真である命題は証明可能である」という数理論理学の主張です。これはGödelの完全性定理の片側で、もう少し正確に述べると、

論理式の集合を\(\Gamma\)とし, そのモデルを\(\mathcal{M}\)とする. \(\Gamma\)の任意のモデル\(\mathcal{M}\)で真となる論理式\(\varphi\)は\(\Gamma\)から形式的に証明できる.

という定理です。

後者は数学の定理なので、信頼するも何もありません。

個人的には「数学は集合論(ZFC)で形式化できる」という主張をどのように説明できるかに興味があります。

Hilbertのテーゼはむしろこのテーマについて調べている最中に出会ってまとめようと思ったという経緯があります。

単にGödelの完全性定理からの帰結だという考え方もあるようなので、次回あたりにこのことについて考えてみたいと思います。

[1] Reinhard Kahle, Is There a “Hilbert Thesis”?, Studia Logica(2019) 107: 145-165.

[2] 鹿島亮, 現代基礎数学15 数理論理学, 朝倉書店, 2009.