ロッサーのからくり

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

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

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

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

Summarize Timeline Top Qs Fact Check

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

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

$${\displaystyle \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))],}$$

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

$${\displaystyle \lnot \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\to \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))].}$$

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

$${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {Proof} _{T}^{R}(x,y).}$$

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

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

対角化補題を使って、${\displaystyle \rho }$を${\displaystyle T}$が${\displaystyle \rho }$ ↔${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}$を証明可能であるような論理式であるとする。論理式${\displaystyle \rho }$は理論${\displaystyle T}$.のロッサー文である。