§E16.30Löb の定理

最終更新

Gödel 文は「自分は証明可能でない」と述べる文の固定点であり、無矛盾な理論はこれを証明しない。では、逆向きの固定点、すなわち「自分は証明可能である」と述べる文はどうなるか。Henkin が提出したこの問いに、Löb はその文が実際に証明可能であると答えた。さらに Löb の議論は、より一般の定理を与える。理論が「ある文が証明可能ならばその文は成り立つ」という含意を証明することができるのは、その文をすでに証明している場合に限る、という定理である。本記事では、これを導出可能性条件と対角線補題だけから証明する。

1 引き継ぐ設定

理論TT、証明述語、および記法は§E16.24 定義 1.1のものをそのまま用いる。すなわちLA={0,S,+,×}L_A=\{0,S,+,\times\}、PA⊆TPA\subseteq T、TTの公理を列挙する決定的プログラムを一つ固定し、標準的な証明述語Prf⁡T\operatorname{Prf}_Tから

Prov⁡T(y):=∃p Prf⁡T(p,y),□Tφ:=Prov⁡T(⌜φ⌝)\operatorname{Prov}_T(y):=\exists p\,\operatorname{Prf}_T(p,y), \qquad \Box_T\varphi:=\operatorname{Prov}_T(\ulcorner\varphi\urcorner)

と定める。□T\Box_Tは算術式の略記であり、言語へ様相演算子を加えるものではない。矛盾文と無矛盾性文も§E16.24 定義 1.2のとおり⊥:=0=S0\bot:=0=S0、Con⁡T:=¬□T⊥\operatorname{Con}_T:=\neg\Box_T\botとする。

本記事の証明で中心となる上流の結果は次の二つである。このほか、古典命題論理の派生則と演繹定理（§E16.10 補題 2.1、§E16.10 定理 5.1）、等号の対称律（§E16.10 補題 4.1）、Robinson 算術の公理（§E16.15 定義 2.1）、一階論理の健全性（§E16.10 定理 6.1）、証明述語の標準モデルでの正確性（§E16.21 定理 5.4）、標準モデルがQQのモデルであること（§E16.15 定理 2.2）を用いる。比較と境界の記述では、Gödel 文の定義と非証明（§E16.23 定義 2.1、§E16.23 定理 2.2）、Tarski の真理定義不能性定理（§E16.22 定理 3.1）、および第二不完全性定理（§E16.24 定理 10.1）を引用する。

  • §E16.24 定理 7.2の三条件。任意の固定したLAL_A文φ,ψ\varphi,\psiについて、T⊢φT\vdash\varphiならばT⊢□TφT\vdash\Box_T\varphi（D1）、T⊢□T(φ→ψ)→(□Tφ→□Tψ)T\vdash\Box_T(\varphi\to\psi)\to(\Box_T\varphi\to\Box_T\psi)（D2）、T⊢□Tφ→□T□TφT\vdash\Box_T\varphi\to\Box_T\Box_T\varphi（D3）である。
  • §E16.22 定理 2.1の固定点。自由変数が高々xxである任意のLAL_A論理式θ(x)\theta(x)に対して、Q⊢χ↔θ(⌜χ⌝)Q\vdash\chi\leftrightarrow\theta(\ulcorner\chi\urcorner)を満たす文χ\chiが存在する。同値がQQ内で成り立つことは、標準モデルにおける真偽を論じるときに用いる。Q⊆TQ\subseteq TであるからT⊢χ↔θ(⌜χ⌝)T\vdash\chi\leftrightarrow\theta(\ulcorner\chi\urcorner)でもある。

TTの無矛盾性は仮定しない。無矛盾性を用いる箇所は、用いる命題ごとに明示する。

2 Henkin の問い

定義 2.1.§E16.22 定理 2.1をθ(x):=Prov⁡T(x)\theta(x):=\operatorname{Prov}_T(x)へ適用して得る文をHHと書き、Henkin 文 (Henkin sentence) と呼ぶ。すなわちHHは

Q⊢H↔□THQ\vdash H\leftrightarrow\Box_TH

を満たす文である。Q⊆TQ\subseteq TであるからT⊢H↔□THT\vdash H\leftrightarrow\Box_THでもある。

§E16.23 定義 2.1の Gödel 文GTG_Tはθ(x):=¬Prov⁡T(x)\theta(x):=\neg\operatorname{Prov}_T(x)の固定点であり、T⊢GT↔¬□TGTT\vdash G_T\leftrightarrow\neg\Box_TG_Tを満たす。Henkin 文は否定を外した固定点である。

注意 2.2 (Henkin 文の真偽は素朴には決まらない).§E16.22 定理 2.1は固定点の同値をQQ内で与え、§E16.15 定理 2.2により標準モデルはQQのモデルである。従って§E16.10 定理 6.1の健全性により、標準モデルではHHと□TH\Box_THの真偽が一致する。さらに§E16.21 定理 5.4により、□TH\Box_THが標準モデルで真であることとT⊢HT\vdash Hは同値である。従って、HHが標準モデルで真であることとT⊢HT\vdash Hは同値である。すなわち「HHは真である」と「HHは証明可能である」は同じ主張に帰着し、どちらか一方を仮定しても他方が出るだけである。この素朴な言い換えだけからは、HHが証明可能であるか否かは決まらない。Gödel 文の場合には、具体的証明の内部化を経由して、固定点の条件と無矛盾性からT⊬GTT\nvdash G_Tを導くことができた（§E16.23 定理 2.2）。同じ議論を Henkin 文へ適用することはできない。HHの証明可能性を仮定しても矛盾が生じないからである。実際、次節以降でT⊢HT\vdash Hを証明する。

3 固定点が与える内部含意

以下の補題、定理、および系では、いずれもLAL_A文φ\varphiを各主張の中で固定する。

補題 3.1.φ\varphiを任意の固定したLAL_A文とする。§E16.22 定理 2.1をθ(x):=Prov⁡T(x)→φ\theta(x):=\operatorname{Prov}_T(x)\to\varphiへ適用し、

T⊢ψ↔(□Tψ→φ)(F)T\vdash\psi\leftrightarrow(\Box_T\psi\to\varphi) \tag{F}

を満たす文ψ\psiを取る。このとき

T⊢□Tψ→□TφT\vdash\Box_T\psi\to\Box_T\varphi

である。

証明. (F) の左から右への含意により

T⊢ψ→(□Tψ→φ)(1)T\vdash\psi\to(\Box_T\psi\to\varphi) \tag{1}

である。D1 を (1) へ適用すると

T⊢□T(ψ→(□Tψ→φ))(2)T\vdash\Box_T\bigl(\psi\to(\Box_T\psi\to\varphi)\bigr) \tag{2}

を得る。D2 を文の対ψ\psiと□Tψ→φ\Box_T\psi\to\varphiへ適用すると

T⊢□T(ψ→(□Tψ→φ))→(□Tψ→□T(□Tψ→φ))T\vdash \Box_T\bigl(\psi\to(\Box_T\psi\to\varphi)\bigr) \to\bigl(\Box_T\psi\to\Box_T(\Box_T\psi\to\varphi)\bigr)

であり、(2) と modus ponens により

T⊢□Tψ→□T(□Tψ→φ)(3)T\vdash\Box_T\psi\to\Box_T(\Box_T\psi\to\varphi) \tag{3}

を得る。次に、D2 を文の対□Tψ\Box_T\psiとφ\varphiへ適用すると

T⊢□T(□Tψ→φ)→(□T□Tψ→□Tφ)(4)T\vdash \Box_T(\Box_T\psi\to\varphi) \to(\Box_T\Box_T\psi\to\Box_T\varphi) \tag{4}

である。(3) と (4) を命題論理で合成すると

T⊢□Tψ→(□T□Tψ→□Tφ)(5)T\vdash\Box_T\psi\to(\Box_T\Box_T\psi\to\Box_T\varphi) \tag{5}

を得る。一方、D3 をψ\psiへ適用すると

T⊢□Tψ→□T□Tψ(6)T\vdash\Box_T\psi\to\Box_T\Box_T\psi \tag{6}

である。(5) と (6) を命題論理で合成すると、表示した結論を得る。この導出ではφ\varphiについて何も仮定しておらず、TTの無矛盾性も用いていない。▨

この補題が本記事の中心である。以下の定理と系は、この含意と、固定点 (F) の右から左への含意と、D1 の三つだけから得る。

4 Löb の定理

定理 4.1 (Löb の定理).φ\varphiを任意の固定したLAL_A文とする。メタ理論で

T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphi

ならば、メタ理論で

T⊢φT\vdash\varphi

である。

証明.T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphiと仮定する。補題 3.1のψ\psiを取るとT⊢□Tψ→□TφT\vdash\Box_T\psi\to\Box_T\varphiであるから、仮定と命題論理により

T⊢□Tψ→φ(7)T\vdash\Box_T\psi\to\varphi \tag{7}

を得る。(F) の右から左への含意はT⊢(□Tψ→φ)→ψT\vdash(\Box_T\psi\to\varphi)\to\psiであるから、(7) と modus ponens により

T⊢ψT\vdash\psi

である。D1 を適用するとT⊢□TψT\vdash\Box_T\psiを得る。これと (7) へ modus ponens を適用するとT⊢φT\vdash\varphiである。▨

注意 4.2 (仮定と結論はいずれもメタ理論の主張である). Löb の定理の仮定T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphiと結論T⊢φT\vdash\varphiは、どちらもTTにおける導出の存在を述べるメタ理論の主張である。定理はTT内の含意(□Tφ→φ)→φ(\Box_T\varphi\to\varphi)\to\varphiを主張していない。この含意は一般にはTTの定理ではない。実際、T=PAT=PAとφ:=⊥\varphi:=\botを取ると、この含意はCon⁡PA→⊥\operatorname{Con}_{PA}\to\botすなわち¬Con⁡PA\neg\operatorname{Con}_{PA}を与えるが、PAPAはこれを証明しない。TT内で成り立つ形は□T(□Tφ→φ)→□Tφ\Box_T(\Box_T\varphi\to\varphi)\to\Box_T\varphiであり、次節で別に証明する。この区別は D1 の場合と同じであり、外から内への規則と内部の含意を混同してはならない。

5 形式化された Löb の定理

Löb の定理の仮定と結論を、いずれもTTの内部の証明可能性として述べた形も成り立つ。

定理 5.1 (形式化された Löb の定理).φ\varphiを任意の固定したLAL_A文とする。このとき

T⊢□T(□Tφ→φ)→□TφT\vdash \Box_T(\Box_T\varphi\to\varphi)\to\Box_T\varphi

である。

証明.補題 3.1のψ\psiを取る。同補題のT⊢□Tψ→□TφT\vdash\Box_T\psi\to\Box_T\varphiから、命題論理により

T⊢(□Tφ→φ)→(□Tψ→φ)(8)T\vdash(\Box_T\varphi\to\varphi)\to(\Box_T\psi\to\varphi) \tag{8}

である。実際、□Tφ→φ\Box_T\varphi\to\varphiと□Tψ\Box_T\psiを仮定すると、同補題により□Tφ\Box_T\varphiを得、仮定した含意によりφ\varphiを得る。

(F) の右から左への含意(□Tψ→φ)→ψ(\Box_T\psi\to\varphi)\to\psiと (8) を合成すると

T⊢(□Tφ→φ)→ψ(9)T\vdash(\Box_T\varphi\to\varphi)\to\psi \tag{9}

を得る。D1 を (9) へ適用するとT⊢□T((□Tφ→φ)→ψ)T\vdash\Box_T\bigl((\Box_T\varphi\to\varphi)\to\psi\bigr)であり、D2 を文の対□Tφ→φ\Box_T\varphi\to\varphiとψ\psiへ適用して modus ponens を用いると

T⊢□T(□Tφ→φ)→□Tψ(10)T\vdash\Box_T(\Box_T\varphi\to\varphi)\to\Box_T\psi \tag{10}

である。(10) と補題 3.1のT⊢□Tψ→□TφT\vdash\Box_T\psi\to\Box_T\varphiを命題論理で合成すると、表示した結論を得る。▨

注意 5.2 (形式化された形は Löb の定理を含む).T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphiと仮定すると、D1 によりT⊢□T(□Tφ→φ)T\vdash\Box_T(\Box_T\varphi\to\varphi)である。定理 5.1と modus ponens によりT⊢□TφT\vdash\Box_T\varphiを得、仮定した含意からT⊢φT\vdash\varphiである。従って定理 4.1は定理 5.1と D1 から得ることもできる。二つの証明は同じ補題を共有しており、独立な経路ではない。

6 Henkin の問いへの答え

系 6.1.定義 2.1の Henkin 文HHについてT⊢HT\vdash Hである。

証明. 固定点の条件T⊢H↔□THT\vdash H\leftrightarrow\Box_THの右から左への含意によりT⊢□TH→HT\vdash\Box_TH\to Hである。定理 4.1をφ:=H\varphi:=Hについて適用するとT⊢HT\vdash Hを得る。▨

注意 6.2 (Gödel 文との対照).TTが無矛盾ならば、§E16.23 定理 2.2によりT⊬GTT\nvdash G_Tである。一方、Henkin 文については無矛盾性を仮定せずにT⊢HT\vdash Hが成り立つ。固定点の内側の否定の有無だけで、結論が正反対になる。また、固定点の同値はQQ内で成り立ち、標準モデルはQQのモデルであるから、T⊢HT\vdash Hと§E16.21 定理 5.4を合わせるとHHは標準モデルで真である。ここでTTが標準モデルで健全であることは仮定していない。用いたのはQQの健全性だけである。

7 第二不完全性定理を系として導き直す

系 7.1.TTが無矛盾ならばT⊬Con⁡TT\nvdash\operatorname{Con}_Tである。

証明. 背理法のためT⊢Con⁡TT\vdash\operatorname{Con}_Tと仮定する。Con⁡T\operatorname{Con}_Tは¬□T⊥\neg\Box_T\botであり、古典命題論理では¬A\neg AからA→BA\to Bを導くことができるので

T⊢□T⊥→⊥T\vdash\Box_T\bot\to\bot

である。定理 4.1をφ:=⊥\varphi:=\botについて適用するとT⊢⊥T\vdash\bot、すなわちT⊢0=S0T\vdash0=S0を得る。

一方、§E16.15 定義 2.1の (Q1) の全称閉包∀x (Sx≠0)\forall x\,(Sx\ne0)はTTの公理であり、x:=0x:=0の具体化と等号の対称律によりT⊢¬(0=S0)T\vdash\neg(0=S0)である。従ってTTは0=S00=S0とその否定をともに証明し、矛盾する。これは仮定に反する。よってT⊬Con⁡TT\nvdash\operatorname{Con}_Tである。▨

注意 7.2 (第二不完全性定理の直接証明との違い).§E16.24 定理 10.1は、Gödel 文の固定点を経由し、内部含意Con⁡T→GT\operatorname{Con}_T\to G_Tを導いたうえで、第一不完全性定理が与える外的事実T⊬GTT\nvdash G_Tと衝突させた。本節の証明はφ:=⊥\varphi:=\botに対する固定点を経由し、第一不完全性定理を用いていない。結論は同じであるが、用いる上流の結果が異なる。

なお本節の証明は定理 4.1を経由しており、その定理 4.1は D1・D2・D3 と§E16.22 定理 2.1に依存する。導出可能性条件と対角線補題の証明はいずれも第二不完全性定理を用いていないので、循環は生じない。本記事が引き継ぐ設定も、証明可能性述語と無矛盾性文の定義だけであり、第二不完全性定理の結論を含まない。

8 反映原理の各例を証明することができないこと

系 8.1.φ\varphiを任意の固定したLAL_A文とする。T⊬φT\nvdash\varphiならば

T⊬□Tφ→φT\nvdash\Box_T\varphi\to\varphi

である。

証明.定理 4.1の対偶である。無矛盾性を仮定していない。▨

注意 8.2 (反映原理を図式として証明することができない). 各文φ\varphiに対する□Tφ→φ\Box_T\varphi\to\varphiを反映の例と呼ぶ。この系は、TTが証明しない文については対応する反映の例も証明しないことを述べる。従って、TTが証明しない文が少なくとも一つ存在する場合には、TTが反映の例をすべて証明することはない。TTが無矛盾ならばこの条件は満たされる。

φ:=⊥\varphi:=\botの場合が第二不完全性定理である。実際、TTが無矛盾ならば、系 7.1の証明で得たT⊢¬⊥T\vdash\neg\botによりT⊬⊥T\nvdash\botである。系によりT⊬(□T⊥→⊥)T\nvdash(\Box_T\bot\to\bot)を得る。同じT⊢¬⊥T\vdash\neg\botにより、TTの内部で□T⊥→⊥\Box_T\bot\to\botと¬□T⊥=Con⁡T\neg\Box_T\bot=\operatorname{Con}_Tは同値であるから、これはT⊬Con⁡TT\nvdash\operatorname{Con}_Tと同値である。φ:=GT\varphi:=G_Tの場合には、TTが無矛盾ならば§E16.23 定理 2.2によりT⊬GTT\nvdash G_Tなので、T⊬(□TGT→GT)T\nvdash(\Box_TG_T\to G_T)である。

「証明可能ならば真である」という言明の各例を、理論が自分自身について図式として証明することはできない。各例をLAL_Aの文として書き下すことはできるが、それらをすべて証明することはできない。この意味で、証明可能性を理論の内部で真理と同じように扱うことはできない。

例 8.3 (真理についての素朴な議論との違い). 自然言語で「この文が真ならばφ\varphiである」と述べる文CCを考える。CCが真であると仮定すると、CCの述べる内容によりφ\varphiを得る。従ってCCが真であることが示されたように見え、もう一度CCの内容を用いるとφ\varphiが任意に従う。これは Curry の逆理である。

この議論を算術の内部で再現するには、真理を表す算術式Tr⁡(x)\operatorname{Tr}(x)が必要である。§E16.22 定理 2.1は任意のTr⁡\operatorname{Tr}についてC↔(Tr⁡(⌜C⌝)→φ)C\leftrightarrow(\operatorname{Tr}(\ulcorner C\urcorner)\to\varphi)を満たすCCを与えるが、逆理の議論はさらにTr⁡(⌜C⌝)↔C\operatorname{Tr}(\ulcorner C\urcorner)\leftrightarrow Cという同値、すなわちTr⁡\operatorname{Tr}が真理図式を満たすことを要求する。ところが§E16.22 定理 3.1により、標準モデルの真理を表す算術式は存在しない。従って、この形の議論を算術の内部で実行することはできない。

Löb の定理は、真理述語を証明可能性述語へ置き換えたときに何が残るかを述べている。Prov⁡T\operatorname{Prov}_Tは算術式として実在し、§E16.22 定理 2.1が固定点を与えるので、対応する議論は実際に実行することができる。ただし結論は「φ\varphiが任意に従う」ではない。得られるのは、TTが□Tφ→φ\Box_T\varphi\to\varphiを証明するならばTTはφ\varphiを証明する、という条件つきの主張である。証明可能性は真理と異なり算術の内部で表すことができる。しかし、そのように表した述語は、自分自身についての反映の例を理論に証明させない。

9 演習

問題 9.1. 次の問いに答えよ。

  1. Gödel 文と Henkin 文は、それぞれどの論理式の固定点か。結論が正反対になる理由を述べよ。
  2. 補題 3.1の証明で、D1、D2、D3 はそれぞれどの段で用いられているか。
  3. 定理 4.1の仮定と結論が、いずれもTT内の含意ではない理由を述べよ。
  4. 第二不完全性定理を Löb の定理から導く際に、TTの無矛盾性を用いる箇所を特定せよ。
  5. Curry の逆理を算術の内部で再現することができない理由を述べよ。
解答 (確認問題の解答).
  1. Gödel 文は¬Prov⁡T(x)\neg\operatorname{Prov}_T(x)の固定点、Henkin 文はProv⁡T(x)\operatorname{Prov}_T(x)の固定点である。Gödel 文では、具体的証明の内部化を経由して、固定点の条件と無矛盾性から非証明が従う。Henkin 文へ同じ議論を適用することはできず、代わりに固定点の条件から□TH→H\Box_TH\to Hが得られるため、Löb の定理を適用することができ、証明可能性が従う。
  2. D1 は (1) から (2) を得る段、D2 は (3) を得る段と (4) を得る段の二度、D3 は (6) を得る段で用いる。
  3. 仮定T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphiは、TTにおける導出の存在を述べるメタ理論の主張である。結論T⊢φT\vdash\varphiも同様である。TT内で成り立つ形は定理 5.1であり、こちらは□T\Box_Tを二重に用いた別の文である。
  4. 無矛盾性は、T⊢⊥T\vdash\botとT⊢¬⊥T\vdash\neg\botがともに成り立つことを矛盾と判定する最後の段だけで用いる。定理 4.1の適用と、Con⁡T\operatorname{Con}_Tから□T⊥→⊥\Box_T\bot\to\botを得る段では用いていない。
  5. 素朴な議論は真理を表す算術式の存在を要求するが、§E16.22 定理 3.1によりそのような式は存在しない。証明可能性述語は実在するので、置き換えた議論は実行することができるが、結論は任意の文の証明可能性ではなく Löb の定理の形になる。

▨

10 境界と次の段階

本記事が証明したのは、固定した標準的な証明可能性述語についての Löb の定理と、その形式化された形、および三つの系である。

□T\Box_Tを様相演算子とみなし、D1・D2・D3 と定理 5.1を公理スキーマとする様相論理の体系、すなわち証明可能性論理 GL は扱わない。GL の Kripke 意味論、算術的完全性定理、および様相論理の固定点定理も扱わない。本単元は、等号を含む一ソートの古典一階論理、直観主義命題論理、単純型付きラムダ計算に限定する。

反映原理の図式全体を加えた理論の性質、ω\omega-無矛盾性を用いる変種、Rosser 型の変種、T+Con⁡TT+\operatorname{Con}_Tの無矛盾性、および真理述語を加えた拡大も扱わない。

対象理論をPAPA以上に限定した理由は、§E16.24 定理 7.2の D2 と D3 の証明が対象理論の帰納法を用いることにある。本記事は導出可能性条件を入力として用いるだけであり、限定を緩めることも強めることもしていない。

参考文献

  1. Martin Hugo Löb, Solution of a Problem of Leon Henkin, The Journal of Symbolic Logic 20 (1955), 115–118.Löb の定理とその証明を参考にした。
  2. George Boolos, The Logic of Provability, Cambridge University Press, 1993.導出可能性条件から Löb の定理を導く筋道と、証明可能性論理を参考にした。
  3. Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic, Perspectives in Logic 3, Cambridge University Press, Cambridge, 2017, originally published 1993.導出可能性条件と Löb の定理を算術理論の枠組みで扱う議論を参考にした。
  4. Peter Smith, An Introduction to Gödel's Theorems, 2nd ed., Cambridge University Press, Cambridge, 2013.Löb の定理と Henkin の問いを参考にした。

前提記事