ゲーデルは不動点定理を用いて「この文は証明できない」という趣旨を表現する算術の文gを構成して、gが無矛盾な公理系では証明も反証もできないことを示して、算術の不完全性を示した。
それでは、「この文は証明できる」を表現する算術の文を構成したらどうだろう。これは証明できるのか、できないのか。こういう問題をレオン・ヘンキンは立てた(1950)。この文をヘンキン文hと呼ぼう。
マーティン・レープは以下の定理を証明することで、ヘンキンの問題を肯定的に解決した(1955)。
- Provable(φ)→φを証明できるなら、φを証明できる。
ヘンキン文hはProvable(x)の不動点として構成できる。不動点定理により
- h ←→ Provable(h)
これは証明可能である。この双条件文を片方の条件文に変えると
- Provable(h)→h
が得られる。よってレープの定理の前件が満たされたので、hは証明できることが示される。
レープの定理の証明には、次の一項述語を利用する*1。
- Provable(x) → φ
- l ←→ (Provable(l)→φ)
が証明可能。lは「この文が証明可能ならφ」と言っているように読める。この双条件文を片方の条件文にすると
- l → (Provable(l) →φ)
これは証明可能なので、
- Provable(l → (Provable(l) →φ))
も証明可能*2。分配して
- Provable(l) → Provable(Provable(l) →φ)
も証明可能。さらに分配して
- Provable(l) → Provable(Provable(l) ) → Provable(φ)
も証明可能。一般に
- Provable(x)→Provable(Provable(x) )
は証明可能なので、
- Provable(l) → Provable(φ)
が証明可能。仮定により
- Provable(φ) → φ
が証明可能なので、
- Provable(l)→φ
が証明可能となる。これが証明できれば、lも証明できることになり、lが証明できればProvable(l)も証明できて、modus ponensでφが証明できる。q.e.d.
レープの定理の対偶をとってφに矛盾記号を代入すると、第二不完全性定理になる。第二不完全性定理からもレープの定理が導出できるので、この二つはある意味同値。
関連記事
*1:cf.Löb's theorem - Wikipedia
*2:可導性条件derivability conditionsの一つを使っている。以下のステップも同様。