Löbの定理

同義語：レーブの定理Löb's theorem

概要

前提知識: Gödelの不完全性定理, 対角化補題, 一階述語論理

算術の理論 $T$ が「$\varphi$ が $T$ から証明できるならば $\varphi$ は正しい」と自分について主張できるのは、どんな $\varphi$ のときか。Löb の定理は、これが $\varphi$ 自身を $T$ が証明できるときに限ることを主張する。$\varphi$ が $T$ で証明できることを表す算術の文を $\square\varphi$ と書くと、適当な条件（導出可能性条件）のもとで
$$ T\vdash\square\varphi\to\varphi\quad\Longrightarrow\quad T\vdash\varphi $$
が成り立つ。証明は、対角化補題で「私が証明できるならば $\varphi$」と述べる文を作り、その文の性質を $T$ の中でたどることによる。
$\varphi$ を矛盾 $\bot$ にとると、$\square\bot\to\bot$ は「$T$ は無矛盾である」と読めるので、Löb の定理は第2不完全性定理を特別な場合として含む（cor-lob-second）。また「私は証明できる」と述べる文は実際に証明できる（cor-lob-henkin）。Löb の定理は $T$ の中でも成り立ち（thm-lob-formalized）、その形 $\square(\square\varphi\to\varphi)\to\square\varphi$ は証明可能性を様相として扱う論理の公理になる。

設定

算術の言語を $L_A=\{0,S,+,\cdot,<\}$、その標準的な構造を $\mathfrak N$、$n\in\mathbb N$ の数項を $\underline n$、論理式 $\varphi$ の Gödel 数を $\#\varphi$、その数項を $\ulcorner\varphi\urcorner$ とする（Gödelの不完全性定理の記事の節「設定」、対角化補題の記事の節「設定」と同じ）。Robinson の算術 $\mathsf Q$ と「$\mathsf Q$ を含む」の意味は Gödelの不完全性定理の記事の定義「Robinson の算術と Peano 算術」による。$0=S0$ を $\bot$ と書く。$\mathsf Q\vdash\lnot\bot$ である。
以下、$T$ は $\mathsf Q$ を含む理論、$\mathrm{P}(y)$ は自由変数が $y$ の中にある論理式とし、文 $\varphi$ について
$$ \square\varphi:=\mathrm{P}(\ulcorner\varphi\urcorner) $$
とおく。$\square\varphi$ も文であり、$\square\square\varphi$ は $\mathrm{P}(\ulcorner\mathrm{P}(\ulcorner\varphi\urcorner)\urcorner)$ を表す。

導出可能性条件

$\mathrm{P}$ についての次の 3 条件を、$T$ に対する 導出可能性条件 という（$\varphi,\psi$ は任意の文）。

(D1) $T\vdash\varphi$ ならば $T\vdash\square\varphi$。
(D2) $T\vdash\square(\varphi\to\psi)\to(\square\varphi\to\square\psi)$。
(D3) $T\vdash\square\varphi\to\square\square\varphi$。
(D1)〜(D3) を満たす $\mathrm{P}$ を、$T$ の 証明可能性述語 とよぶ。

条件は Gödelの不完全性定理の記事の定義「導出可能性条件」と同じである。(D1) は「証明できる文については、証明できることも証明できる」、(D2) は「前件肯定を $T$ の中で行える」、(D3) は「(D1) を $T$ の中で行える」という条件である。
標準的な例は次のとおりである。$T$ が決定可能な公理系なら、「$x$ は $T$ からの導出の番号で、その最後の論理式の番号が $y$」という関係を $\mathsf Q$ で表現する論理式 $\mathrm{Pr}_T(x,y)$ をとり、$\mathrm{Prov}_T(y):=\exists x\,\mathrm{Pr}_T(x,y)$ とおく。この $\mathrm{Prov}_T$ は (D1) を満たす（Gödelの不完全性定理の記事の補題「証明可能性の表現」の 1）。Peano 算術 $\mathsf{PA}$ について、自然に作った $\mathrm{Prov}_{\mathsf{PA}}$ が (D2)・(D3) も満たすことは、この記事では証明しない（OLT26 §37.6、pp. 587–588。同書でも証明は省かれている）。
(D1)・(D2) からすぐに次が従う。

証明可能性述語の単調性

$\mathrm{P}$ が (D1)・(D2) を満たすとする。文 $\varphi,\psi,\chi$ について次が成り立つ。

$T\vdash\varphi\to\psi$ ならば $T\vdash\square\varphi\to\square\psi$。
$T\vdash\varphi\to(\psi\to\chi)$ ならば $T\vdash\square\varphi\to(\square\psi\to\square\chi)$。

1：(D1) により $T\vdash\square(\varphi\to\psi)$ であり、(D2) の $T\vdash\square(\varphi\to\psi)\to(\square\varphi\to\square\psi)$ と前件肯定により $T\vdash\square\varphi\to\square\psi$ である。
2：1 を $\psi\to\chi$ に使うと $T\vdash\square\varphi\to\square(\psi\to\chi)$ である。(D2) により $T\vdash\square(\psi\to\chi)\to(\square\psi\to\square\chi)$ なので、命題論理により $T\vdash\square\varphi\to(\square\psi\to\square\chi)$ である。$\square$

Löb の定理

$T$ を $\mathsf Q$ を含む理論とし、$\mathrm{P}$ を $T$ の証明可能性述語（(D1)〜(D3) を満たす）とする。文 $\varphi$ について、
$$ T\vdash\square\varphi\to\varphi $$
ならば $T\vdash\varphi$ である。

対角化で作る文の性質をたどる

$\psi(y):=\bigl(\mathrm{P}(y)\to\varphi\bigr)$ とおく。$\varphi$ は文なので、$\psi$ の自由変数は $y$ の中にある。対角化補題の定理「対角化補題」により、文 $\theta$ で
$$ T\vdash\theta\leftrightarrow(\square\theta\to\varphi) $$
となるものがある。$T$ の中で次の順に導く。

不動点の左から右の向きにより $T\vdash\theta\to(\square\theta\to\varphi)$。
1 に lem-lob-mono の 2 を使うと $T\vdash\square\theta\to(\square\square\theta\to\square\varphi)$。
(D3) により $T\vdash\square\theta\to\square\square\theta$。2 と合わせて、命題論理により $T\vdash\square\theta\to\square\varphi$。
仮定 $T\vdash\square\varphi\to\varphi$ と 3 により $T\vdash\square\theta\to\varphi$。
不動点の右から左の向き $T\vdash(\square\theta\to\varphi)\to\theta$ と 4 により $T\vdash\theta$。
5 に (D1) を使うと $T\vdash\square\theta$。4 と合わせて $T\vdash\varphi$。
$\square$

仮定 $T\vdash\square\varphi\to\varphi$ を使ったのは 4 だけであり、1〜3 は任意の文 $\varphi$ について成り立つ。$T$ の無矛盾性は仮定していない。$T$ が公理化可能であることも仮定した形の定理と同じ証明が OLT26 Theorem 37.10（p. 590、証明 pp. 591–592）にある。上の証明は公理化可能性を使っていない。逆向きは自明で、$T\vdash\varphi$ ならどんな文 $\chi$ についても $T\vdash\chi\to\varphi$ である。

直感

$\theta$ は「私が証明できるならば $\varphi$」と述べる文である。証明は次の推論を、真理を証明可能性に置き換えて $T$ の中で行ったものである。「$\theta$ を仮定すると、$\theta$ の言い分（$\theta$ ならば $\varphi$）と合わせて $\varphi$ が出る。こうして『$\theta$ ならば $\varphi$』が示されたが、それはまさに $\theta$ なので $\theta$ が成り立ち、したがって $\varphi$ が成り立つ」。この推論を真理についてそのまま行うと、任意の主張 $\varphi$ が正しいことになってしまう（OLT26 p. 591 は同じ筋の発見的な説明を与えている）。Löb の定理では、仮定 $\square\varphi\to\varphi$ が「証明できれば正しい」という部分を補い、結論は「$\varphi$ が正しい」ではなく「$\varphi$ が証明できる」になる。

系

第2不完全性定理

$T$ と $\mathrm{P}$ を thm-lob-main のとおりとし、$\mathrm{Con}:=\lnot\square\bot$ とおく。$T$ が無矛盾ならば $T\not\vdash\mathrm{Con}$ である。

$T\vdash\lnot\square\bot$ とすると、恒真式 $\lnot A\to(A\to B)$ により $T\vdash\square\bot\to\bot$ である。thm-lob-main により $T\vdash\bot$ となる。$T$ は $\mathsf Q$ を含むので $T\vdash\lnot\bot$ でもあり、$T$ は矛盾する。$\square$

$\mathrm{P}=\mathrm{Prov}_T$ のとき $\mathrm{Con}$ は Gödelの不完全性定理の記事の $\mathrm{Con}_T$ であり、cor-lob-second は同記事の定理「第2不完全性定理」と同じ主張である。あちらは Gödel 文を経由して証明し、ここでは Löb の定理から 2 行で導いた（OLT26 p. 592 にも同じ注意がある）。

自分の証明可能性を主張する文

$T$ と $\mathrm{P}$ を thm-lob-main のとおりとする。文 $\delta$ が $T\vdash\delta\leftrightarrow\square\delta$ を満たすならば $T\vdash\delta$ である。

仮定から $T\vdash\square\delta\to\delta$ なので、thm-lob-main により $T\vdash\delta$ である。$\square$

対角化補題を $\psi:=\mathrm{P}$ に使えば、そのような $\delta$ は存在する。「私は証明できない」と述べる Gödel 文は（$T$ が無矛盾なら）証明できないのに対し、「私は証明できる」と述べる文は必ず証明できる。この問いは Henkin が 1952 年に提起し、Löb が 1955 年に解いた（Ver24 §1）。

証明できない文についての反映

$T$ と $\mathrm{P}$ を thm-lob-main のとおりとする。文 $\varphi$ について、$T\vdash\square\varphi\to\varphi$ であることと $T\vdash\varphi$ であることは同値である。とくに $T$ が無矛盾なら $T\not\vdash\square\bot\to\bot$ である。

$T\vdash\varphi$ なら $T\vdash\square\varphi\to\varphi$ である。逆は thm-lob-main である。後半は $\varphi:=\bot$ とし、$T$ が無矛盾なら $T\not\vdash\bot$ であることによる。$\square$

$\mathfrak N$ を $T$ のモデルにもつ決定可能な公理系 $T$ と $\mathrm P=\mathrm{Prov}_T$ を考えると、$\mathfrak N\models\mathrm{Prov}_T[\#\varphi]$ は $T\vdash\varphi$ と同値であり（Gödelの不完全性定理の記事の補題「証明可能性の表現」の 2）、そのとき健全性により $\mathfrak N\models\varphi$ である。したがって文 $\square\varphi\to\varphi$ はどの $\varphi$ についても $\mathfrak N$ で真である。cor-lob-reflection は、これらの真な文のうち $T$ が証明できるのは、$\varphi$ がもともと証明できるものだけであることを述べている。

理論の中の Löb の定理

thm-lob-main は「$T$ で証明できるならば」という $T$ の外の推論である。同じことが $T$ の中で 1 つの文として証明できる。

Löb の定理の形式化

$T$ と $\mathrm{P}$ を thm-lob-main のとおりとする。すべての文 $\varphi$ について
$$ T\vdash\square(\square\varphi\to\varphi)\to\square\varphi $$
である。

prf-lob-main と同じ不動点 $\theta$（$T\vdash\theta\leftrightarrow(\square\theta\to\varphi)$）をとる。同じ証明の 3 は仮定を使わずに得られたので、
$$ T\vdash\square\theta\to\square\varphi $$
である。これから命題論理により $T\vdash(\square\varphi\to\varphi)\to(\square\theta\to\varphi)$ が従い（$\square\varphi\to\varphi$ と $\square\theta$ を仮定すると $\square\varphi$、したがって $\varphi$ が出る）、不動点の右から左の向きと合わせて
$$ T\vdash(\square\varphi\to\varphi)\to\theta $$
である。lem-lob-mono の 1 により $T\vdash\square(\square\varphi\to\varphi)\to\square\theta$ であり、はじめの式と合わせて $T\vdash\square(\square\varphi\to\varphi)\to\square\varphi$ を得る。$\square$

thm-lob-formalized から thm-lob-main が出る。実際、$T\vdash\square\varphi\to\varphi$ なら (D1) により $T\vdash\square(\square\varphi\to\varphi)$、よって $T\vdash\square\varphi$ であり、仮定と合わせて $T\vdash\varphi$ である。

形式化された第2不完全性定理

$T$ と $\mathrm{P}$ を thm-lob-main のとおりとし、$\mathrm{Con}:=\lnot\square\bot$ とおく。このとき
$$ T\vdash\mathrm{Con}\to\lnot\square\mathrm{Con} $$
である。すなわち $T$ は「$T$ が無矛盾ならば、$T$ は自分の無矛盾性を証明できない」を証明する。

恒真式 $\lnot A\to(A\to B)$ により $T\vdash\lnot\square\bot\to(\square\bot\to\bot)$ である。lem-lob-mono の 1 により $T\vdash\square\mathrm{Con}\to\square(\square\bot\to\bot)$ であり、thm-lob-formalized を $\varphi:=\bot$ に使うと $T\vdash\square(\square\bot\to\bot)\to\square\bot$ である。合わせて $T\vdash\square\mathrm{Con}\to\square\bot$、対偶をとって $T\vdash\lnot\square\bot\to\lnot\square\mathrm{Con}$ である。$\square$

例

Gödel 文と自分の証明可能性を主張する文の比較

$T$ を $\mathsf Q$ を含む無矛盾な理論とし、$\mathrm{P}$ を $T$ の証明可能性述語とする。対角化補題により、$T\vdash\gamma\leftrightarrow\lnot\square\gamma$ となる文 $\gamma$ と、$T\vdash\delta\leftrightarrow\square\delta$ となる文 $\delta$ がある。

$T\vdash\gamma$ とすると、(D1) により $T\vdash\square\gamma$、不動点により $T\vdash\lnot\square\gamma$ となって矛盾する。よって $T\not\vdash\gamma$ である。
$\delta$ には同じ議論が通らない。$T\vdash\delta$ と仮定しても、(D1) と不動点の両方から同じ $T\vdash\square\delta$ が出るだけである。実際には cor-lob-henkin により $T\vdash\delta$ である。
$\gamma$ と $\delta$ は、自分について「証明できない」「証明できる」と述べる点だけが違うが、証明可能性は正反対になる。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
(D1)	$T=\mathsf Q$、$\mathrm{P}(y):=\lnot(y=y)$	$T\vdash\square\bot\to\bot$ から $T\vdash\bot$ が従うこと
(D2)・(D3)	Gödelの不完全性定理の記事の反例の表の 4 行目の $\mathrm{Prov}^\ast_T$	$T\vdash\square^\ast\bot\to\bot$ から $T\vdash\bot$ が従うこと
仮定「$T\vdash\square\varphi\to\varphi$」（$\mathfrak N$ で真であることに弱める）	$T=\mathsf{PA}$、$\mathrm{P}=\mathrm{Prov}_{\mathsf{PA}}$、$\varphi:=\bot$	$T\vdash\varphi$

反例の確かめ

1 行目：$\square\varphi$ は $\lnot(\ulcorner\varphi\urcorner=\ulcorner\varphi\urcorner)$ であり、一階述語論理で $\lnot\square\varphi$ が導出できる。したがって (D2)・(D3) は、前件が否定を導出できる文なので $\mathsf Q$ で導出できる。(D1) は成り立たない。$\mathsf Q\vdash0=0$ だが、$\mathsf Q$ は無矛盾（$\mathfrak N$ がモデル）なので $\mathsf Q\not\vdash\square(0=0)$ である。$\mathsf Q\vdash\lnot\square\bot$ から $\mathsf Q\vdash\square\bot\to\bot$ だが、$\mathsf Q\not\vdash\bot$ である。
2 行目：$T$ を $\mathsf Q$ を含む無矛盾な決定可能な公理系とする。Gödelの不完全性定理の記事の例「反例の確かめ」の 4 行目で、$\mathrm{Prov}^\ast_T$ は (D1) を満たし、$T\vdash\lnot\mathrm{Prov}^\ast_T(\ulcorner\bot\urcorner)$ であることが示されている。$\square^\ast\varphi:=\mathrm{Prov}^\ast_T(\ulcorner\varphi\urcorner)$ とおくと $T\vdash\square^\ast\bot\to\bot$ だが、$T$ は無矛盾なので $T\not\vdash\bot$ である。thm-lob-main により、$\mathrm{Prov}^\ast_T$ は (D2) と (D3) の少なくとも一方を満たさない。
3 行目：$\mathfrak N$ は $\mathsf{PA}$ のモデルなので $\mathsf{PA}\not\vdash\bot$ であり、Gödelの不完全性定理の記事の補題「証明可能性の表現」の 2 により $\mathfrak N\not\models\mathrm{Prov}_{\mathsf{PA}}[\#\bot]$、したがって $\mathfrak N\models\square\bot\to\bot$ である。(D1)〜(D3) は上の節で述べた所在のとおり成り立つ。しかし $\mathsf{PA}\not\vdash\bot$ である。$\mathsf{PA}\not\vdash\square\bot\to\bot$ であることは cor-lob-reflection の後半による。

補足

証明可能性論理：様相論理の体系 $\mathbf K$ に Löb の公理 $\square(\square A\to A)\to\square A$ を加えた体系を $\mathbf{GL}$ という（Ver24 §2.1）。命題変数に算術の文を代入し、$\square$ を $\mathrm{Prov}_{\mathsf{PA}}$ と読む写し方（実現）を考えると、様相論理式 $A$ が $\mathbf{GL}$ の定理であることと、すべての実現で $A$ の写しが $\mathsf{PA}$ から証明できることは同値である（Solovay の算術的完全性定理、1976 年。Ver24 §4.2。この記事では証明しない）。$\mathbf{GL}$ が健全である、すなわち $\mathbf{GL}$ の定理の写しが証明できることの中心は thm-lob-formalized である。Löb の公理が妥当になるフレームの特徴づけは様相論理の記事の注意「一階の性質で書けない対応」にある。
条件の由来：(D1)〜(D3) の形は Löb が同じ論文で定式化した（Ver24 §1）。