レーブの定理

数理論理学におけるレーブの定理 (Löb's theorem) は、ペアノ算術 (PA) (またはPAを含む任意の形式体系)において、任意の論理式Pについて、「PがPAで証明可能ならばPである」ことがPAで証明可能ならば、PはPAで証明可能であることを述べている。Prov(P)が論理式Pが証明可能であることを意味する場合、レーブの定理をより形式的に表現すると次のようになる。

もし

${\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}}$

ならば

${\displaystyle {\mathit {PA}}\vdash P}$

レーブの定理の直接的な帰結(対偶)は、PがPAで証明可能でない場合、「PがPAで証明可能ならば、Pである」はPAで証明可能でないということである。例えば、「${\displaystyle 1+1=3}$がPAで証明可能ならば、${\displaystyle 1+1=3}$である」はPAでは証明可能でない^[1]。

レーブの定理は、1955年にそれを定式化したマルティン・フーゴー・レーブにちなんで名付けられた^[2]。これはカリーのパラドックスに関連している^[3]。

証明可能性論理におけるレーブの定理

証明可能性論理は、ゲーデルの不完全性定理で使用される符号化の詳細を様相論理の言語を使って抽象化するものであり、具体的には与えられた体系における${\displaystyle \phi }$の証明可能性を様相${\displaystyle \Box \phi }$を用いて表現する。

すると、レーブの定理を以下の公理として形式化できる。

${\displaystyle \Box (\Box P\rightarrow P)\rightarrow \Box P}$

これは、ゲーデル＝レーブ (Gödel–Löb) の公理GLとして知られている。これは、次のような推論規則によって形式化されることもある。

もし

${\displaystyle \vdash \Box P\rightarrow P}$

ならば

${\displaystyle \vdash P}$

様相論理 K4 (あるいは、公理スキーマ4 (${\displaystyle \Box A\rightarrow \Box \Box A}$)は冗長であるため単にK)に上記の公理GLを追加した結果得られる証明可能性論理GLは、証明可能性論理において最も集中的に研究されている体系である。

レーブの定理の様相論理による証明

レーブの定理は、証明可能性演算子(${\displaystyle /Box}$)に関するいくつかの基本的な規則(K4体系)と様相不動点の存在のみを用いて、様相論理内で証明することができる。

様相論理式

様相論理式 (modal formula)の文法として、以下を仮定する。

1. ${\displaystyle X}$が命題変数（英語版）であれば、${\displaystyle X}$は論理式である。
2. ${\displaystyle K}$が命題定数であれば、${\displaystyle K}$は論理式である。
3. ${\displaystyle A}$が論理式であれば、${\displaystyle \Box A}$は論理式である。
4. ${\displaystyle A}$と${\displaystyle B}$が論理式であれば、${\displaystyle \neg A}$、${\displaystyle A\rightarrow B}$、${\displaystyle A\wedge B}$、${\displaystyle A\vee B}$、${\displaystyle A\leftrightarrow B}$も論理式である。

様相文(modal sentence)とは、命題変数を含まない様相論理式のことである。${\displaystyle \vdash A}$は、${\displaystyle A}$が定理であることを意味する。

様相不動点

${\displaystyle F(X)}$が命題変数${\displaystyle X}$を1つだけ持つ様相論理式であれば、${\displaystyle F(X)}$の様相不動点は次のような文${\displaystyle \Psi }$である。

${\displaystyle \vdash \Psi \leftrightarrow F(\Box \Psi )}$

1つの自由変数を持つすべての様相論理式に対して、このような不動点が存在すると仮定する。これはもちろん自明な仮定ではないが、${\displaystyle \Box }$をペアノ算術における証明可能性として解釈すれば、様相不動点の存在は対角線補題から導かれる。

様相推論規則

様相不動点の存在に加えて、証明可能性演算子${\displaystyle \Box }$に対する以下の推論規則を仮定する。これらはヒルベルト＝ベルナイス証明可能性条件（英語版）として知られている。

1. (必然化規則) ${\displaystyle \vdash A}$から${\displaystyle \vdash \Box A}$を結論づける: これは非形式的には、Aが定理であればAが証明可能であることを意味する。
2. (内部必然化法則) ${\displaystyle \vdash \Box A\rightarrow \Box \Box A}$: Aが証明可能であれば、それが証明可能であることが証明可能である。
3. (ボックス分配律) ${\displaystyle \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}$: この規則は、証明可能性演算子の内部でモーダスポネンスの適用を可能にする。AがBを含意することが証明可能であり、Aが証明可能であれば、Bも証明可能である。

レーブの定理の証明

証明の大部分は仮定${\displaystyle \Box P\to P}$を使用しないので、理解を容易にするために以下の証明は${\displaystyle \Box P\to P}$に依存する部分を最後の方に分離して記載する。

${\displaystyle P}$を任意の様相文とする。

1. 様相不動点の存在を論理式${\displaystyle F(X)=X\rightarrow P}$に適用する。すると、${\displaystyle \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)}$となるような文${\displaystyle \Psi }$が存在することがわかる。
2. ${\displaystyle \vdash \Psi \rightarrow (\Box \Psi \rightarrow P)}$ 〔1より〕。
3. ${\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))}$ 〔2と必然化規則により〕。
4. ${\displaystyle \vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)}$ 〔3とボックス分配律より〕。
5. ${\displaystyle \vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)}$ 〔${\displaystyle A=\Box \Psi }$および${\displaystyle B=P}$としてボックス分配律を適用することにより〕。
6. ${\displaystyle \vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)}$ 〔4と5より〕。
7. ${\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi }$ 〔6と内部必然化規則により〕。
8. ${\displaystyle \vdash \Box \Psi \rightarrow \Box P}$ 〔6と7より〕。
   
   ここから、証明の仮定を使用する部分に入る。
   
   
9. ${\displaystyle \vdash \Box P\rightarrow P}$と仮定する。大雑把に言えば、${\displaystyle P}$が証明可能であれば、それは実際には真であるという定理である。これは健全性 (soundness) の主張である。
10. ${\displaystyle \vdash \Box \Psi \rightarrow P}$ 〔8と9より〕。
11. ${\displaystyle \vdash (\Box \Psi \rightarrow P)\rightarrow \Psi }$ 〔1より〕。
12. ${\displaystyle \vdash \Psi }$ 〔10と11より〕。
13. ${\displaystyle \vdash \Box \Psi }$ 〔12と必然化規則により〕。
14. ${\displaystyle \vdash P}$ 〔13と10より〕。

より非公式には、証明を次のように概説できる。

1. 仮定より${\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} _{PA}(P)\rightarrow P}}$なので、${\displaystyle {\mathit {PA}}\vdash {\neg P\rightarrow \neg \mathrm {Prov} _{PA}(P)}}$も成り立ち、これは${\displaystyle \{{\mathit {PA}},\neg P\}\vdash {\neg \mathrm {Prov} _{PA}(P)}}$を意味する。
2. ここで、ハイブリッド理論${\displaystyle \{{\mathit {PA}},\neg P\}}$について以下の推論ができる。
   1. ${\displaystyle \{{\mathit {PA}},\neg P\}}$が矛盾している(inconsistent)と仮定すると、PAから${\displaystyle \neg P\to \bot {}}$が証明でき、これは${\displaystyle P}$と同じである。
   2. しかし、${\displaystyle \{{\mathit {PA}},\neg P\}}$について${\displaystyle \neg \mathrm {Prov} _{PA}(P)}$とわかっているので、矛盾が生じる。
   3. したがって、${\displaystyle \{{\mathit {PA}},\neg P\}}$は無矛盾(consistent)である。
3. ゲーデルの第2不完全性定理により、これは${\displaystyle \{{\mathit {PA}},\neg P\}}$が矛盾していることを意味する。
4. したがって、PAから${\displaystyle \neg P\to \bot {}}$が証明でき、これは${\displaystyle P}$と同じである。

例

レーブの定理の直接的な帰結は、PがPAで証明可能でない場合、「PがPAで証明可能ならば、Pは真である」はPAで証明可能でないということである。PAが無矛盾であるとして(ただし、PAはPAが無矛盾であることを知らない)、以下に簡単な例をいくつか挙げる。

• 「${\displaystyle 1+1=3}$がPAで証明可能ならば、${\displaystyle 1+1=3}$である」はPAでは証明可能でない。なぜなら、${\displaystyle 1+1=3}$はPAでは証明可能でない(偽であるため)からである。
• 「${\displaystyle 1+1=2}$がPAで証明可能ならば、${\displaystyle 1+1=2}$である」はPAで証明可能である。「Xならば、${\displaystyle 1+1=2}$である」という形式の文はすべて証明可能である。
• 「強化版有限ラムゼーの定理がPAで証明可能ならば、強化版有限ラムゼーの定理が成り立つ」はPAで証明可能でない。なぜなら、「強化版有限ラムゼーの定理が成り立つ」はPAでは証明可能でない(標準モデルにおいて真であるにもかかわらず)からである。

信念論理（英語版）において、レーブの定理は、形式系が反射的(reflexive)（英語版）な「4型（英語版）」の推論者として分類されるならば、その形式系は謙虚 (modest) でもある必要があることを示している。つまり、そのような推論者は、Pを信じるときのみ「私がPを信じるならばPである」と信じる^[4]。

ゲーデルの第2不完全性定理は、レーブの定理において偽の文${\displaystyle \bot }$をPに代入することによって導かれる。

逆: レーブの定理から様相不動点の存在を導く

様相不動点の存在からレーブの定理を導けるだけでなく、その逆も導ける。レーブの定理が公理(スキーマ)として与えられた場合、pが様相化された任意の論理式A(p)に対して、(互いに証明可能な文を同一視した)不動点${\displaystyle p\leftrightarrow A(p)}$の存在が導かれる^[5]。したがって、正規様相論理において、レーブの公理は公理スキーマ4 (${\displaystyle \Box A\rightarrow \Box \Box A}$)および様相不動点の存在の連言と同値である。