素数のまばらさに関する定理については「ロッサーの定理 」をご覧ください。
数理論理学 において、ロッサーのからくり (英 : Rosser's trick ) とは考慮中の理論のω無矛盾 性を仮定することなしにゲーデルの不完全性定理 を証明する手法である (Smorynski 1977, p. 840; Mendelson 1977, p. 160)。この手法はゲーデルが1931年に出版した元の不完全性定理の証明を改善するものとして、1936年にジョン・バークリー・ロッサー によって導入された。
ゲーデルによる元の証明は (非形式的に言えば)「この文は証明できない」と主張する文を使うが、ロッサーのからくりは「この文が証明可能ならば、この文の否定のより短い証明が存在する」と主張する論理式を使う。
背景 ロッサーのからくりはゲーデルの不完全性定理と同様の仮定から始まる。実効的、無矛盾、かつ初頭算術の十分な断片を含む理論
T
{\displaystyle T}
ゲーデルの証明は、任意のそのような理論に対してある論理式
Proof
T
(
x
,
y
)
{\displaystyle \operatorname {Proof} _{T}(x,y)}
y
{\displaystyle y}
x
{\displaystyle x}
T
{\displaystyle T}
y
{\displaystyle y}
y
{\displaystyle y}
y
{\displaystyle y}
ϕ
{\displaystyle \phi }
#
ϕ
{\displaystyle \#\phi }
Pvbl
T
(
y
)
{\displaystyle \operatorname {Pvbl} _{T}(y)}
∃
x
Proof
T
(
x
,
y
)
{\displaystyle \exists x\operatorname {Proof} _{T}(x,y)}
T
{\displaystyle T}
T
{\displaystyle T}
y
{\displaystyle y}
ϕ
{\displaystyle \phi }
neg
(
y
)
{\displaystyle {\text{neg}}(y)}
¬
ϕ
{\displaystyle \neg \phi }
neg
(
y
)
{\displaystyle {\text{neg}}(y)}
理論
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
G
T
{\displaystyle G_{T}}
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
¬
Pvbl
T
(
#
ϕ
)
{\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}
T
{\displaystyle T}
T
{\displaystyle T}
ω無矛盾 であるという、より強い仮定を追加する必要がある。たとえば、理論
T
=
PA
+
¬
G
P
A
{\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}
ペアノ算術 ) は
¬
G
T
{\displaystyle \neg G_{T}}
ロッサー文 ある固定された算術の理論
T
{\displaystyle T}
Proof
T
(
x
,
y
)
{\displaystyle \operatorname {Proof} _{T}(x,y)}
neg
(
x
)
{\displaystyle {\text{neg}}(x)}
変更された証明述語
Proof
T
R
(
x
,
y
)
{\displaystyle \operatorname {Proof} _{T}^{R}(x,y)}
Proof
T
R
(
x
,
y
)
≡
Proof
T
(
x
,
y
)
∧
¬
∃
z
≤
x
[
Proof
T
(
z
,
neg
(
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))],}
その意味は以下の通りである。
¬
Proof
T
R
(
x
,
y
)
≡
Proof
T
(
x
,
y
)
→
∃
z
≤
x
[
Proof
T
(
z
,
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))].}
この変更された証明述語は変更された可証性述語
Pvbl
T
R
(
y
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}
Pvbl
T
R
(
y
)
≡
∃
x
Proof
T
R
(
x
,
y
)
.
{\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {Proof} _{T}^{R}(x,y).}
非形式的にいうと、
Pvbl
T
R
(
y
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}
y
{\displaystyle y}
x
{\displaystyle x}
y
{\displaystyle y}
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
Pvbl
T
R
(
#
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}
Pvbl
T
(
#
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}
ϕ
{\displaystyle \phi }
T
{\displaystyle T}
¬
ϕ
{\displaystyle \neg \phi }
Pvbl
T
(
#
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}
Pvbl
T
R
(
#
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}
T
{\displaystyle T}
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
Pvbl
T
R
(
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )}
¬
Pvbl
T
R
(
neg
(
ϕ
)
)
{\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))}
n
,
m
{\displaystyle n,m}
ϕ
{\displaystyle \phi }
¬
ϕ
{\displaystyle \neg \phi }
n
<
m
{\displaystyle n<m}
m
<
n
{\displaystyle m<n}
T
{\displaystyle T}
対角化補題（英語版 ） を使って、
ρ
{\displaystyle \rho }
T
{\displaystyle T}
ρ
{\displaystyle \rho }
¬
Pvbl
T
R
(
#
ρ
)
{\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
ロッサー文 である。
ロッサーの定理
T
{\displaystyle T}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
¬
ρ
{\displaystyle \neg \rho }
これを証明するために、まずある論理式
y
{\displaystyle y}
e
{\displaystyle e}
Proof
T
R
(
e
,
y
)
{\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}
T
{\displaystyle T}
Proof
T
R
(
e
,
y
)
{\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}
T
{\displaystyle T}
Proof
T
(
e
,
y
)
{\displaystyle \operatorname {Proof} _{T}(e,y)}
e
{\displaystyle e}
z
{\displaystyle z}
z
{\displaystyle z}
T
{\displaystyle T}
¬
Proof
T
(
z
,
(neg
(
y
)
)
)
{\displaystyle \neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y)))}
T
{\displaystyle T}
Pvbl
T
R
(
y
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}
T
{\displaystyle T}
加えて、
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
T
{\displaystyle T}
e
{\displaystyle e}
T
{\displaystyle T}
ϕ
{\displaystyle \phi }
Proof
T
R
(
e
,
y
)
{\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}
T
{\displaystyle T}
Pvbl
T
R
(
#
ϕ
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}
(1)の証明はゲーデルによる第一不完全性定理の証明と似ている:
T
{\displaystyle T}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
Pvbl
T
R
(
#
ρ
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\rho )}
T
{\displaystyle T}
¬
ρ
{\displaystyle \neg \rho }
T
{\displaystyle T}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
T
{\displaystyle T}
ρ
{\displaystyle \rho }
(2)の証明も特定の形の
Proof
T
R
{\displaystyle \operatorname {Proof} _{T}^{R}}
T
{\displaystyle T}
¬
ρ
{\displaystyle \neg \rho }
T
{\displaystyle T}
Pvbl
T
R
(
neg
#
(
ρ
)
)
{\displaystyle \operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))}
T
{\displaystyle T}
¬
Pvbl
T
R
(
#
ρ
)
{\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}
T
{\displaystyle T}
ρ
{\displaystyle \rho }
T
{\displaystyle T}
¬
ρ
{\displaystyle \neg \rho }
T
{\displaystyle T}
T
{\displaystyle T}
¬
ρ
{\displaystyle \neg \rho }
出典 外部リンク
![{\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))],}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f00be62ed956de3762c6997532740f54433d6a17)
![{\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))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d2409c36c0f20efcea981829e8cb5afcd0b790ef)
