レーブの定理

数式については、以下の文法を前提とします。

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}$

様相文とは、この構文において命題変数を含まない式である。表記法${\displaystyle \vdash A}$は、${\displaystyle A}$これは定理である。

もし${\displaystyle F(X)}$これは、命題変数が1つだけの様相論理式です。${\displaystyle X}$すると、モーダル固定点${\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が定理であれば、それは証明可能であるという意味です。
2. （内的必然性）${\displaystyle \vdash \Box A\rightarrow \Box \Box A}$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 \Psi }$そのため${\displaystyle \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)}$。
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 \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}$" と${\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 }$内部必然性ルール。
8. ${\displaystyle \vdash \Box \Psi \rightarrow \Box P}$6と7から。ここから、仮説を用いる証明の部分に入ります。
9. と仮定する${\displaystyle \vdash \Box P\rightarrow P}$大まかに言えば、もし${\displaystyle P}$証明可能であれば、それは実際に真実である。これは正当性の主張である。
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 {証明} _{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\}}$矛盾しているならば、PA は${\displaystyle \neg P\to \bot {}}$これは、${\displaystyle P}$。
   2. しかし、${\displaystyle \{{\mathit {PA}},\neg P\}}$すでに知っている${\displaystyle \neg \mathrm {証明} _{PA}(P)}$それは矛盾だ。
   3. したがって、${\displaystyle \{{\mathit {PA}},\neg P\}}$一貫性がある。
3. ゲーデルの第二不完全性定理によれば、これは${\displaystyle \{{\mathit {PA}},\neg P\}}$一貫性がない。
4. したがって、PAは証明する${\displaystyle \neg P\to \bot {}}$これは、${\displaystyle P}$。