§E19.30Löb の定理

最終更新

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

1 引き継ぐ設定

理論TT、証明述語、および記法は§E19.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は算術式の略記であり、言語へ様相演算子を加えるものではない。矛盾文と無矛盾性文も§E19.24 定義 1.2のとおり⊥:=0=S0\bot:=0=S0、Con⁡T:=¬□T⊥\operatorname{Con}_T:=\neg\Box_T\botとする。

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

  • §E19.24 定理 7.2の三条件。任意の固定したLAL_A文φ,ψ\varphi,\psiについて、T⊢φT\vdash\varphiならばT⊢□TφT\vdash\Box_T\varphi（§E19.24 定理 7.2 (D1)）、T⊢□T(φ→ψ)→(□Tφ→□Tψ)T\vdash\Box_T(\varphi\to\psi)\to(\Box_T\varphi\to\Box_T\psi)（§E19.24 定理 7.2 (D2)）、T⊢□Tφ→□T□TφT\vdash\Box_T\varphi\to\Box_T\Box_T\varphi（§E19.24 定理 7.2 (D3)）である。
  • §E19.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.§E19.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でもある。

§E19.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 文は、¬Prov⁡T(x)\neg\operatorname{Prov}_T(x)から否定を外した論理式Prov⁡T(x)\operatorname{Prov}_T(x)の固定点である。

注意 2.2.§E19.22 定理 2.1により固定点の同値がQQ内で得られ、§E19.15 定理 2.2により標準モデルはQQのモデルである。従って§E19.10 定理 6.1の健全性により、標準モデルではHHと□TH\Box_THの真偽が一致する。さらに§E19.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を導くことができた（§E19.23 定理 2.2）。同じ議論を Henkin 文へ適用することはできない。HHの証明可能性を仮定しても矛盾が生じないからである。実際、次節以降でT⊢HT\vdash Hを証明する。

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

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

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

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

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

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

である。

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

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

である。§E19.24 定理 7.2 (D1)を式 (3.1.1)へ適用すると

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

を得る。§E19.24 定理 7.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)

であり、式 (3.1.2)と modus ponens により

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

を得る。次に、§E19.24 定理 7.2 (D2)を文の対□Tψ\Box_T\psiとφ\varphiへ適用すると

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

である。式 (3.1.3)と式 (3.1.4)を命題論理で合成すると

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

を得る。一方、§E19.24 定理 7.2 (D3)をψ\psiへ適用すると

T⊢□Tψ→□T□TψT\vdash\Box_T\psi\to\Box_T\Box_T\psi(3.1.6)\text{(3.1.6)}

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

上の補題が本記事の中心である。以下の定理と系は、同補題の含意T⊢□Tψ→□TφT\vdash\Box_T\psi\to\Box_T\varphiと、固定点式 (F)の右から左への含意と、§E19.24 定理 7.2 (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ψ→φT\vdash\Box_T\psi\to\varphi(4.1.1)\text{(4.1.1)}

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

T⊢ψT\vdash\psi

である。§E19.24 定理 7.2 (D1)を適用するとT⊢□TψT\vdash\Box_T\psiを得る。これと式 (4.1.1)へ 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であり、次節で別に証明する。この区別は§E19.24 定理 7.2 (D1)の場合と同じであり、外から内への規則と内部の含意を混同してはならない。

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

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

定理 5.1.φ\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ψ→φ)T\vdash(\Box_T\varphi\to\varphi)\to(\Box_T\psi\to\varphi)(5.1.1)\text{(5.1.1)}

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

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

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

を得る。§E19.24 定理 7.2 (D1)を式 (5.1.2)へ適用するとT⊢□T((□Tφ→φ)→ψ)T\vdash\Box_T\bigl((\Box_T\varphi\to\varphi)\to\psi\bigr)であり、§E19.24 定理 7.2 (D2)を文の対□Tφ→φ\Box_T\varphi\to\varphiとψ\psiへ適用して modus ponens を用いると

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

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

注意 5.2.T⊢□Tφ→φT\vdash\Box_T\varphi\to\varphiと仮定すると、§E19.24 定理 7.2 (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と§E19.24 定理 7.2 (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が無矛盾ならば、§E19.23 定理 2.2によりT⊬GTT\nvdash G_Tである。一方、Henkin 文については無矛盾性を仮定せずにT⊢HT\vdash Hが成り立つ。固定点の内側の否定の有無だけで、結論が正反対になる。また、固定点の同値はQQ内で成り立ち、標準モデルはQQのモデルであるから、T⊢HT\vdash Hと§E19.21 定理 5.4を合わせるとHHは標準モデルで真である。ここでTTが標準モデルで健全であることは仮定していない。用いたのはQQの健全性だけである。

7 Löb の定理からの第二不完全性定理の導出

系 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を得る。

一方、§E19.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 (第二不完全性定理の直接証明との違い).§E19.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は§E19.24 定理 7.2 (D1)・§E19.24 定理 7.2 (D2)・§E19.24 定理 7.2 (D3)と§E19.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が無矛盾ならば§E19.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)が必要である。§E19.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}が真理図式を満たすことが要求される。ところが§E19.22 定理 3.1により、標準モデルの真理を表す算術式は存在しない。従って、この形の議論を算術の内部で実行することはできない。

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

9 仮定と主張の境界

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

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

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

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

10 演習

問題 10.1. 以下、φ\varphiはLAL_A文である。必要ならば、T⊢A→BT\vdash A\to BならばT⊢□TA→□TBT\vdash\Box_TA\to\Box_TBであること（§E19.24 定理 7.2 (D1)と§E19.24 定理 7.2 (D2)から従う）を用いてよい。

  1. 文χ\chiがT⊢χ↔□T¬χT\vdash\chi\leftrightarrow\Box_T\neg\chiを満たすならば、T⊢χ↔□T⊥T\vdash\chi\leftrightarrow\Box_T\botであることを示せ。
  2. 補題 3.1のψ\psiについて、T⊢ψ↔(□Tφ→φ)T\vdash\psi\leftrightarrow(\Box_T\varphi\to\varphi)であることを示せ。
  3. T⊢□T(□Tφ→φ)↔□TφT\vdash\Box_T(\Box_T\varphi\to\varphi)\leftrightarrow\Box_T\varphiを示せ。
  4. 文の列をCon⁡0:=(0=0)\operatorname{Con}^0:=(0=0)、Con⁡n+1:=¬□T¬Con⁡n\operatorname{Con}^{n+1}:=\neg\Box_T\neg\operatorname{Con}^nで定める。すべてのnnについてT⊢Con⁡n+1→Con⁡nT\vdash\operatorname{Con}^{n+1}\to\operatorname{Con}^nであることを示し、T⊢Con⁡1↔Con⁡TT\vdash\operatorname{Con}^1\leftrightarrow\operatorname{Con}_Tを示せ。さらに、TTが無矛盾ならばn≥1n\geq1についてT⊬Con⁡nT\nvdash\operatorname{Con}^nであることを示せ。
  5. 論理式Tr⁡(x)\operatorname{Tr}(x)が、すべてのLAL_A文σ\sigmaについてT⊢Tr⁡(⌜σ⌝)↔σT\vdash\operatorname{Tr}(\ulcorner\sigma\urcorner)\leftrightarrow\sigmaを満たすとする。否定を用いない Curry の議論により、TTがすべてのLAL_A文を証明することを示せ。
解答 (確認問題の解答).

  1. 右から左を示す。§E19.15 定義 2.1 (Q1)と等号の対称律によりT⊢¬⊥T\vdash\neg\botであり、命題論理によりT⊢⊥→¬χT\vdash\bot\to\neg\chiであるから、T⊢□T⊥→□T¬χT\vdash\Box_T\bot\to\Box_T\neg\chiである。固定点の右から左の含意T⊢□T¬χ→χT\vdash\Box_T\neg\chi\to\chiと合わせてT⊢□T⊥→χT\vdash\Box_T\bot\to\chiを得る。

    左から右を示す。固定点の左から右の含意によりT⊢χ→□T¬χT\vdash\chi\to\Box_T\neg\chiである。§E19.24 定理 7.2 (D3)を¬χ\neg\chiに適用するとT⊢□T¬χ→□T□T¬χT\vdash\Box_T\neg\chi\to\Box_T\Box_T\neg\chiであり、固定点の右から左の含意T⊢□T¬χ→χT\vdash\Box_T\neg\chi\to\chiからT⊢□T□T¬χ→□TχT\vdash\Box_T\Box_T\neg\chi\to\Box_T\chiである。よってT⊢χ→□TχT\vdash\chi\to\Box_T\chiである。§E19.24 補題 8.1をA:=χA:=\chiに適用したT⊢□Tχ→(□T¬χ→□T⊥)T\vdash\Box_T\chi\to(\Box_T\neg\chi\to\Box_T\bot)と、χ→□Tχ\chi\to\Box_T\chi、χ→□T¬χ\chi\to\Box_T\neg\chiを命題論理で合成するとT⊢χ→□T⊥T\vdash\chi\to\Box_T\botである。

  2. 右から左を示す。TTの内部で□Tφ→φ\Box_T\varphi\to\varphiと□Tψ\Box_T\psiを仮定すると、補題 3.1により□Tφ\Box_T\varphiであり、仮定によりφ\varphiである。よってT⊢(□Tφ→φ)→(□Tψ→φ)T\vdash(\Box_T\varphi\to\varphi)\to(\Box_T\psi\to\varphi)であり、式 (F)の右から左の含意と合成してT⊢(□Tφ→φ)→ψT\vdash(\Box_T\varphi\to\varphi)\to\psiを得る。

    左から右を示す。命題論理によりT⊢φ→(□Tψ→φ)T\vdash\varphi\to(\Box_T\psi\to\varphi)であり、式 (F)の右から左の含意によりT⊢φ→ψT\vdash\varphi\to\psiである。よってT⊢□Tφ→□TψT\vdash\Box_T\varphi\to\Box_T\psiである。TTの内部でψ\psiと□Tφ\Box_T\varphiを仮定すると、後者から□Tψ\Box_T\psiを得て、式 (F)の左から右の含意ψ→(□Tψ→φ)\psi\to(\Box_T\psi\to\varphi)によりφ\varphiを得る。演繹定理によりT⊢ψ→(□Tφ→φ)T\vdash\psi\to(\Box_T\varphi\to\varphi)である。したがって、この固定点はψ\psiの取り方によらず、TTの中で□Tφ→φ\Box_T\varphi\to\varphiと同値である。

  3. 左から右は定理 5.1である。右から左について、命題論理によりT⊢φ→(□Tφ→φ)T\vdash\varphi\to(\Box_T\varphi\to\varphi)であるからT⊢□Tφ→□T(□Tφ→φ)T\vdash\Box_T\varphi\to\Box_T(\Box_T\varphi\to\varphi)である。

  4. nnについての帰納法で示す。n=0n=0ではCon⁡0=(0=0)\operatorname{Con}^0=(0=0)はTTの定理であるから、弱化によりT⊢Con⁡1→Con⁡0T\vdash\operatorname{Con}^1\to\operatorname{Con}^0である。T⊢Con⁡n+1→Con⁡nT\vdash\operatorname{Con}^{n+1}\to\operatorname{Con}^nならば、対偶によりT⊢¬Con⁡n→¬Con⁡n+1T\vdash\neg\operatorname{Con}^n\to\neg\operatorname{Con}^{n+1}であり、T⊢□T¬Con⁡n→□T¬Con⁡n+1T\vdash\Box_T\neg\operatorname{Con}^n\to\Box_T\neg\operatorname{Con}^{n+1}である。再び対偶を取るとT⊢¬□T¬Con⁡n+1→¬□T¬Con⁡nT\vdash\neg\Box_T\neg\operatorname{Con}^{n+1}\to\neg\Box_T\neg\operatorname{Con}^n、すなわちT⊢Con⁡n+2→Con⁡n+1T\vdash\operatorname{Con}^{n+2}\to\operatorname{Con}^{n+1}である。

    T⊢0=0T\vdash0=0とT⊢¬⊥T\vdash\neg\botにより、命題論理でT⊢¬(0=0)→⊥T\vdash\neg(0=0)\to\botとT⊢⊥→¬(0=0)T\vdash\bot\to\neg(0=0)を得る。両方に問題文の規則を適用するとT⊢□T¬(0=0)↔□T⊥T\vdash\Box_T\neg(0=0)\leftrightarrow\Box_T\botであり、否定を取ってT⊢Con⁡1↔Con⁡TT\vdash\operatorname{Con}^1\leftrightarrow\operatorname{Con}_Tである。TTが無矛盾ならば系 7.1によりT⊬Con⁡TT\nvdash\operatorname{Con}_Tであり、T⊢Con⁡1T\vdash\operatorname{Con}^1でもない。n≥1n\geq1について、前段の含意を連ねるとT⊢Con⁡n→Con⁡1T\vdash\operatorname{Con}^n\to\operatorname{Con}^1であるから、T⊢Con⁡nT\vdash\operatorname{Con}^nならばT⊢Con⁡1T\vdash\operatorname{Con}^1となって矛盾する。よってT⊬Con⁡nT\nvdash\operatorname{Con}^nである。

  5. LAL_A文φ\varphiを任意に取る。§E19.22 定理 2.1をθ(x):=Tr⁡(x)→φ\theta(x):=\operatorname{Tr}(x)\to\varphiに適用し、T⊢C↔(Tr⁡(⌜C⌝)→φ)T\vdash C\leftrightarrow(\operatorname{Tr}(\ulcorner C\urcorner)\to\varphi)を満たす文CCを取る。仮定T⊢Tr⁡(⌜C⌝)↔CT\vdash\operatorname{Tr}(\ulcorner C\urcorner)\leftrightarrow Cと合わせるとT⊢C↔(C→φ)T\vdash C\leftrightarrow(C\to\varphi)である。TTの内部でCCを仮定すると、左から右の含意によりC→φC\to\varphiを得て、CCと合わせてφ\varphiを得る。演繹定理によりT⊢C→φT\vdash C\to\varphiである。右から左の含意(C→φ)→C(C\to\varphi)\to Cと modus ponens によりT⊢CT\vdash Cであり、T⊢C→φT\vdash C\to\varphiと合わせてT⊢φT\vdash\varphiである。この議論は否定を用いないので、Curry の議論を算術の内部で実行すると、真理図式を満たすTr⁡\operatorname{Tr}をもつ理論はすべての文を証明する。とくに無矛盾なTTにはそのようなTr⁡\operatorname{Tr}が存在しない。Tr⁡\operatorname{Tr}の代わりにProv⁡T\operatorname{Prov}_Tを用いると、Prov⁡T(⌜C⌝)\operatorname{Prov}_T(\ulcorner C\urcorner)とCCの同値が一般にはTTで証明されないので、同じ形の固定点から得られるのは 2 の同値と定理 4.1である。

▨

参考文献

  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 の問いを参考にした。

前提記事