Skinerrian's blog

論理学・哲学・科学史・社会学などに興味があるので、その方面のことを書きます。更新は不定期。

ヘンキンの問題

ゲーデル不動点定理を用いて「この文は証明できない」という趣旨を表現する算術の文gを構成して、gが無矛盾な公理系では証明も反証もできないことを示して、算術の不完全性を示した。

それでは、「この文は証明できる」を表現する算術の文を構成したらどうだろう。これは証明できるのか、できないのか。こういう問題をレオン・ヘンキンは立てた(1950)。この文をヘンキン文hと呼ぼう。

マーティン・レープは以下の定理を証明することで、ヘンキンの問題を肯定的に解決した(1955)。

  • Provable(φ)→φを証明できるなら、φを証明できる。

ヘンキン文hはProvable(x)の不動点として構成できる。不動点定理により

  • h ←→ Provable(h)

これは証明可能である。この双条件文を片方の条件文に変えると

  • Provable(h)→h

が得られる。よってレープの定理の前件が満たされたので、hは証明できることが示される。

レープの定理の証明には、次の一項述語を利用する*1

  • Provable(x) → φ

この述語の不動点をlとすると、不動点定理により

  • 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の一つを使っている。以下のステップも同様。