コンテンツにスキップ

ロッサーのからくり

出典: フリー百科事典『ウィキペディア(Wikipedia)』

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

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

背景

[編集]

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

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

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

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

ロッサー文

[編集]

ある固定された算術の理論に対し、をそれぞれ関連付けられた証明述語と論理否定関数であるとする。

変更された証明述語は以下のように定義される:

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

この変更された証明述語は変更された可証性述語の定義に使う:

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

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

対角化補題を使って、 ↔を証明可能であるような論理式であるとする。論理式は理論.ロッサー文である。

ロッサーの定理

[編集]

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

  1. を証明しない
  2. を証明しない

これを証明するために、まずある論理式およびある数について、が成り立つならば、を証明することを示す。これはゲーデルが第一不完全性定理の証明で行ったことと似たやり方で示される: は2つの具体的な自然数の関係であるを証明する。それからより小さなすべての自然数1つ1つにわたり、それぞれのについて、はやはり具体的な2つの自然数の関係であるを証明する。

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

加えて、が無矛盾でを証明するならば、におけるその証明のコードである数が存在し、におけるの否定の証明のコードである数は存在しない。したがってが成り立ち、よってを証明する。

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

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

出典

[編集]
  • Mendelson (1977), Introduction to Mathematical Logic(英語)
  • Smorynski (1977), "The incompleteness theorems", in Handbook of Mathematical Logic, Jon Barwise, Ed., North Holland, 1982, ISBN 0-444-86388-5(英語)
  • Barkley Rosser (September 1936). “Extensions of some theorems of Gödel and Church”. Journal of Symbolic Logic 1 (3): 87–91. doi:10.2307/2269028. JSTOR 2269028. https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/extensions-of-some-theorems-of-godel-and-church/0461E34DC1F219C459EE84CC2FA89068. (英語)

外部リンク

[編集]