ロッサーのからくり

数理論理学において、**ロッサーのからくり** () とは考慮中の理論のω無矛盾性を仮定することなしにゲーデルの不完全性定理を証明する手法である (Smorynski 1977, p.&nbsp;840; Mendelson 1977, p.&nbsp;160)。この手法はゲーデルが1931年に出版した元の不完全性定理の証明を改善するものとして、1936年にジョン・バークリー・ロッサーによって導入された。

ゲーデルによる元の証明は (非形式的に言えば)「この文は証明できない」と主張する文を使うが、ロッサーのからくりは「この文が証明可能ならば、この文の否定のより短い証明が存在する」と主張する論理式を使う。

## 背景
ロッサーのからくりはゲーデルの不完全性定理と同様の仮定から始まる。実効的、無矛盾、かつ初頭算術の十分な断片を含む理論Tを選ぶ。

ゲーデルの証明は、任意のそのような理論に対してある論理式\operatorname{Proof}_T(x,y)が存在し、その意図された意味はyはある論理式の自然数のコード (ゲーデル数) であり、xはTの公理からyによってコード化された論理式の証明へのゲーデル数であることを示す (以降本記事では、数yとyによってコード化された論理式を区別せず、論理式\phiのコードである数を\#\phiで表す)。加えて、論理式\operatorname{Pvbl}_T(y)を \exists x\operatorname{Proof}_T(x,y)と定義する。これはTから証明可能な論理式の集合を定義することを意図している。

Tに課した仮定から、yが論理式\phiのコードならば、\text{neg}(y)は論理式\neg \phiのコードであるという性質を持つ論理否定関数\text{neg}(y)を定義できることも示せる。論理否定関数はどんな値であっても入力に取ることができる。入力が論理式のコードであるとは限らない。

理論Tのゲーデル文\phi (G_Tと表すこともある)は、Tが\phi&nbsp;↔\neg \operatorname{Pvbl}_T(\#\phi)を証明できるような論理式である。ゲーデルの証明が示したことは以下の通りである。Tが無矛盾ならば、Tは自分自身のゲーデル文を証明できない。しかしゲーデル文の否定も証明できないことを示すためには、理論が単なる無矛盾ではなくω無矛盾であるという、より強い仮定を追加する必要がある。たとえば、理論T=\text{PA}+\neg \text{G}_{PA} (ここでPAはペアノ算術) は\neg G_Tを証明する。ロッサー (1936) はゲーデルの証明に使われたゲーデル文を置き換えることができる異なる自己言及文を構築し、ω無矛盾性の仮定を取り除いた。

## ロッサー文
ある固定された算術の理論Tに対し、\operatorname{Proof}_T(x,y)と\text{neg}(x)をそれぞれ関連付けられた証明述語と論理否定関数であるとする。

変更された証明述語\operatorname{Proof}^R_T(x,y)は以下のように定義される:

\operatorname{Proof}^R_T(x,y) \equiv \operatorname{Proof}_T(x,y) \land \lnot \exists z \leq x [ \operatorname{Proof}_T(z,\operatorname{neg}(y))],

その意味は以下の通りである。

\lnot \operatorname{Proof}^R_T(x,y) \equiv \operatorname{Proof}_T(x,y) \to \exists z \leq x [ \operatorname{Proof}_T(z,\operatorname{neg}(y))].

この変更された証明述語は変更された可証性述語\operatorname{Pvbl}^R_T(y)の定義に使う:

\operatorname{Pvbl}^R_T(y) \equiv \exists x \operatorname{Proof}^R_T(x,y).

非形式的にいうと、\operatorname{Pvbl}^R_T(y)は以下のような主張である。yはあるコード化された証明xによって証明可能であり、yの否定のより小さなコード化された証明は存在しない。Tが無矛盾であるという仮定のもとでは、各論理式\phiごとに、論理式\operatorname{Pvbl}^R_T(\#\phi)が成り立つことと\operatorname{Pvbl}_T(\#\phi)が成り立つことは同値である。なぜならば、もし\phiの証明のコードが存在するならば、(Tの無矛盾性の仮定に従い) \neg \phiの証明のコードは存在しないからである。しかしながら、\operatorname{Pvbl}_T(\#\phi)と\operatorname{Pvbl}^R_T(\#\phi)はTにおける証明可能性の観点からは異なる性質を持つ。

Tが十分な算術を含むなら、すべての論理式\phiに対し、\operatorname{Pvbl}^R_T(\phi)は\neg \operatorname{Pvbl}^R_T(\text{neg}(\phi))を含意することを証明可能であることが、定義から直ちに従う。なぜならば、もしそうでなければ、2つの数n,mが存在し、それぞれ\phiと\neg \phiの証明のコードであり、nとmの両方を満たすからである (実はTに必要なのはそのような状況がいかなる2数に対しても起き得ないことの証明と、いくばくかの一階述語論理のみである)。

を使って、\rhoをTが\rho&nbsp;↔\neg \operatorname{Pvbl}_T^R(\#\rho)を証明可能であるような論理式であるとする。論理式\rhoは理論の**ロッサー文**である。

## ロッサーの定理
Tを実効的で十分な算術を含む無矛盾な理論、そのロッサー文を\rhoとする。すると以下が成り立つ (Mendelson 1977, p.&nbsp;160):
# Tは\rhoを証明しない
# Tは\neg \rhoを証明しない

これを証明するために、まずある論理式yおよびある数eについて、\operatorname{Proof}^R_T(e,y)が成り立つならば、Tは\operatorname{Proof}^R_T(e,y)を証明することを示す。これはゲーデルが第一不完全性定理の証明で行ったことと似たやり方で示される: Tは2つの具体的な自然数の関係である\operatorname{Proof}_T(e,y)を証明する。それからeより小さなすべての自然数z1つ1つにわたり、それぞれのzについて、Tはやはり具体的な2つの自然数の関係である\neg \operatorname{Proof}_T(z, \text{(neg}(y)))を証明する。

Tがその場合に\operatorname{Pvbl}^R_T(y)を証明できることは、Tが十分な算術 (実際には、必要なのは基本的な一階述語論理である) を含むという仮定が保証する。

加えて、Tが無矛盾で\phiを証明するならば、Tにおけるその証明のコードである数eが存在し、Tにおける\phiの否定の証明のコードである数は存在しない。したがって\operatorname{Proof}^R_T(e,y)が成り立ち、よってTは\operatorname{Pvbl}^R_T(\#\phi)を証明する。

(1)の証明はゲーデルによる第一不完全性定理の証明と似ている: Tが\rhoを証明すると仮定する; すると上記により、Tが\operatorname{Pvbl}^R_T(\#\rho)を証明することが従う。よってTは\neg \rhoも証明する。しかしTは\rhoを証明すると仮定したから、これはTが無矛盾ならばありえない。Tは\rhoを証明しないと結論せざるをえない。

(2)の証明も特定の形の\operatorname{Proof}^R_Tを使う。Tが\neg \rhoを証明すると仮定する; すると上記により、Tが\operatorname{Pvbl}^R_T(\text{neg}\#(\rho))を証明することが従う。しかし前節で説明されたロッサーの可証性述語の定義から直ちにわかるように、Tは\neg \operatorname{Pvbl}^R_T(\#\rho)を証明することが従う。よってTは\rhoも証明する。しかしTは\neg \rhoを証明すると仮定したから、これはTが無矛盾ならばありえない。Tは\neg \rhoを証明しないと結論せざるをえない。

## 出典
* Mendelson (1977), *Introduction to Mathematical Logic*
* Smorynski (1977), "The incompleteness theorems", in *Handbook of Mathematical Logic*, Jon Barwise, Ed., North Holland, 1982, 
* 

## 外部リンク
* Avigad (2007), "Computability and Incompleteness", lecture notes.