日々の流転

λ. ヘンキン文

先日、「H↔Provable([H]) な H の真偽」というクイズを書いた。 反応が全く無くて少し寂しかったのだけど、忘れないうちに簡単な解説を。

この論理式はヘンキン文(Henkin sentence)と呼ばれていて、その名の通り1950年頃にヘンキンによってその真偽が問題にされたそうだ。 そして、この論理式が真であることは Löb によって1955年に示されている。 以下に簡単に証明するが、なかなかトリッキーで面白い。

• Löb, M. H. 1955. Solution of a problem of Leon Henkin. Journal of Symbolic Logic, vol. 20, pp. 115-18.

前提

証明可能性は可導性条件(derivability conditions)と呼ばれる以下の条件を満たす。

D1

T ⊢ P ⇒ T ⊢ Provable([P])

D2

T ⊢ Provable([P→Q]) → Provable([P]) → Provable([Q])

D3

T ⊢ Provable([P]) → Provable([Provable([P])])

また、不動点定理が成り立つ。すなわち、任意の一変数論理式 P(x) に対して、ある論理式Qが存在して T ⊢ Q↔P([Q]) が成り立つ。

証明

H は T ⊢ H↔Provable([H]) を満たすとする。

まず、不動点定理によって、ある論理式Dが存在して T ⊢ D ↔ (Provable([D])→H) を満たす。

S := Provable([D])→H とすると T ⊢ D → S

D1を適用して T ⊢ Provable([D → S])

D2を適用して T ⊢ Provable([D]) → Provable([S])

Sを展開してもう一回D2を適用して T ⊢ Provable([D]) → Provable([Provable([D])]) → Provable([H])

D3より T ⊢ Provable([D])→Provable([Provable([D])]) なので、T ⊢ Provable([D]) → Provable([H])

Hの定義より T ⊢ H↔Provable([H]) なので、T ⊢ Provable([D]) → H

Dの定義より T ⊢ D ↔ (Provable([D])→H) なので T ⊢ D で、D1 より T ⊢ Provable([D])

T ⊢ Provable([D]) と T ⊢ Provable([D]) → H とにMPを適用して T ⊢ H

様相論理との関係

Provable([X]) を □X と書くことにすると、D1は必然化に、D2はKに、D3は4に対応する。 さらに不動点定理に対応するものを様相論理で公理化して……という話があるがそれはまたそのうち。

λ. かつ泉の宝山豚ロースかつ定食(中)

美味しかった。