ロッサーのからくり

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

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

背景

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

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

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

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

ロッサー文

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

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

$${\mathrm{Proof}}_T^R(x,y)\equiv {\mathrm{Proof}}_T(x,y)\wedge \mathrm{\neg }\mathrm{\exists }z\le x[{\mathrm{Proof}}_T(z,\mathrm{neg}(y))],$$

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

$$\mathrm{\neg }{\mathrm{Proof}}_T^R(x,y)\equiv {\mathrm{Proof}}_T(x,y)\to \mathrm{\exists }z\le x[{\mathrm{Proof}}_T(z,\mathrm{neg}(y))].$$

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

$${\mathrm{Pvbl}}_T^R(y)\equiv \mathrm{\exists }x{\mathrm{Proof}}_T^R(x,y).$$

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

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

テンプレート:仮リンクを使って、$\rho$を$T$が$\rho$ ↔$\mathrm{\neg }{\mathrm{Pvbl}}_T^R(\mathrm{\#}\rho )$を証明可能であるような論理式であるとする。論理式$\rho$は理論テンプレート:Nowrapのロッサー文である。

ロッサーの定理

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

1. $T$は$\rho$を証明しない
2. $T$は$\mathrm{\neg }\rho$を証明しない

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

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

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

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

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

出典

• Mendelson (1977), Introduction to Mathematical Logicテンプレート:En icon
• Smorynski (1977), "The incompleteness theorems", in Handbook of Mathematical Logic, Jon Barwise, Ed., North Holland, 1982, テンプレート:ISBN2テンプレート:En icon
• テンプレート:Cite journalテンプレート:En icon

外部リンク

• Avigad (2007), "Computability and Incompleteness", lecture notes.テンプレート:En icon