レーブの定理のソースを表示

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

:もし
:<math>\mathit{PA} \vdash {\mathrm{Prov}(P) \rightarrow P}</math>
:ならば
:<math>\mathit{PA} \vdash P</math>

レーブの定理の直接的な帰結([[対偶 (論理学)|対偶]])は、''P''がPAで証明可能でない場合、「''P''がPAで証明可能ならば、''P''である」はPAで証明可能でないということである。例えば、「<math>1+1=3</math>がPAで証明可能ならば、<math>1+1=3</math>である」はPAでは証明可能でない<ref>PAが矛盾していない限り(その場合、<math>1+1=3</math>を含むすべての文が証明可能である)。</ref>。

レーブの定理は、1955年にそれを定式化した[[マルティン・レーブ|マルティン・フーゴー・レーブ]]にちなんで名付けられた{{sfn|Löb|1955}}。これは[[カリーのパラドックス]]に関連している<ref>{{cite web |last1=Neel |first1=Krishnaswami |title=Löb's theorem is (almost) the Y combinator |url=https://semantic-domain.blogspot.com/2016/05/lobs-theorem-is-almost-y-combinator.html |website=Semantic Domain |access-date=9 April 2024 |ref=neel}}</ref>。

==証明可能性論理におけるレーブの定理==
[[証明可能性論理]]は、[[ゲーデルの不完全性定理]]で使用される符号化の詳細を[[様相論理]]の言語を使って抽象化するものであり、具体的には与えられた体系における<math>\phi</math>の証明可能性を様相{{tooltip|<math>\Box \phi</math>|四角形はボックスを意図しており、ブラウザが別のグリフの表示に失敗したわけではない。}}を用いて表現する。

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

:<math>\Box(\Box P\rightarrow P)\rightarrow \Box P</math>

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

:もし
:<math>\vdash \Box P \rightarrow P</math>
:ならば
:<math>\vdash P</math>

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

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

===様相論理式===
様相論理式 (modal formula)の文法として、以下を仮定する。
# <math>X</math>が{{仮リンク|命題変数|en|Propositional variable}}であれば、<math>X</math>は論理式である。
# <math>K</math>が命題定数であれば、<math>K</math>は論理式である。
# <math>A</math>が論理式であれば、<math>\Box A</math>は論理式である。
# <math>A</math>と<math>B</math>が論理式であれば、<math>\neg A</math>、<math>A \rightarrow B</math>、<math>A \wedge B</math>、<math>A \vee B</math>、<math>A \leftrightarrow B</math>も論理式である。

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

===様相不動点===
<math>F(X)</math>が命題変数<math>X</math>を1つだけ持つ様相論理式であれば、<math>F(X)</math>の様相不動点は次のような文<math>\Psi</math>である。
:<math>\vdash \Psi \leftrightarrow F(\Box \Psi)</math>

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

===様相推論規則===
様相不動点の存在に加えて、証明可能性演算子<math>\Box</math>に対する以下の推論規則を仮定する。これらは{{仮リンク|ヒルベルト＝ベルナイス証明可能性条件|en|Hilbert–Bernays provability conditions}}として知られている。

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

===レーブの定理の証明===

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

<math>P</math>を任意の様相文とする。

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

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

==例==
レーブの定理の直接的な帰結は、''P''がPAで証明可能でない場合、「''P''がPAで証明可能ならば、''P''は真である」はPAで証明可能でないということである。PAが無矛盾であるとして(ただし、PAはPAが無矛盾であることを知らない)、以下に簡単な例をいくつか挙げる。
* 「<math>1+1=3</math>がPAで証明可能ならば、<math>1+1=3</math>である」はPAでは証明可能でない。なぜなら、<math>1+1=3</math>はPAでは証明可能でない(偽であるため)からである。
* 「<math>1+1=2</math>がPAで証明可能ならば、<math>1+1=2</math>である」はPAで証明可能である。「Xならば、<math>1+1=2</math>である」という形式の文はすべて証明可能である。
* 「[[パリス＝ハーリントンの定理#強化版有限ラムゼーの定理|強化版有限ラムゼーの定理]]がPAで証明可能ならば、強化版有限ラムゼーの定理が成り立つ」はPAで証明可能でない。なぜなら、「強化版有限ラムゼーの定理が成り立つ」はPAでは証明可能でない(標準モデルにおいて真であるにもかかわらず)からである。

{{仮リンク|信念論理|en|Doxastic logic}}において、レーブの定理は、形式系が''{{仮リンク|信念論理#推論者の種別|en|Doxastic logic#Types of reasoners|label=反射的(reflexive)}}''な「{{仮リンク|4型|en|Doxastic logic#Increasing levels of rationality}}」の推論者として分類されるならば、その形式系は''謙虚'' (modest) でもある必要があることを示している。つまり、そのような推論者は、Pを信じるときのみ「私がPを信じるならばPである」と信じる{{sfn|Smullyan|1986}}。

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

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

==注釈==
{{Reflist}}

==参考文献==
* {{cite book | last = Boolos | first = George S. | author-link = George Boolos | title = The Logic of Provability | publisher = [[ケンブリッジ大学出版局]] (Cambridge University Press) | year = 1995 | isbn = 978-0-521-48325-4 | url-access = registration | url = https://archive.org/details/logicofprovabili0000bool }}
* {{cite book | last = Hinman | first = P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | year = 2005 | isbn = 978-1-56881-262-5 }}
* {{cite book | last1 = Japaridze | first1 = Giorgi | last2 = De Jongh | first2 = Dick | year = 1998 | chapter = Chapter VII - The Logic of Provability | title = Handbook of Proof Theory | series = Studies in Logic and the Foundations of Mathematics | editor-last = Buss | editor-first = Samuel R. | editor-link = Samuel Buss | publisher = [[エルゼビア]] (Elsevier) | volume = 137 | pages = 475–546 | doi = 10.1016/S0049-237X(98)80022-0 | doi-access = free }}
* {{cite journal | last = Lindström | first = Per | author-link = Per Lindström | date = June 2006 | volume = 35 | issue = 3 | pages = 225–230 | title = Note on Some Fixed Point Constructions in Provability Logic | doi = 10.1007/s10992-005-9013-8 | journal = {{仮リンク|Journal of Philosophical Logic|en|Journal of Philosophical Logic}} | s2cid = 11038803 }}
* {{cite journal | last = Löb | first = Martin | author-link = Martin Löb | title = Solution of a Problem of Leon Henkin | journal = {{仮リンク|Journal of Symbolic Logic|en|Journal of Symbolic Logic}} | volume = 20 | issue = 2 | year = 1955 | pages = 115–118 | doi = 10.2307/2266895 | jstor = 2266895 | s2cid = 250348262 }}
* {{cite conference | last = Smullyan |first = Raymond M. | author-link = レイモンド・スマリヤン | year = 1986 | title = Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA) | publisher = Morgan Kaufmann Publishers Inc. | location = San Francisco (CA) | pages = 341–352 | chapter-url = https://dl.acm.org/doi/pdf/10.5555/1029786.1029818 | chapter = Logicians who reason about themselves | doi = 10.1016/B978-0-934613-04-0.50028-4 | isbn=9780934613040 }}

==外部リンク==
* {{Cite web
|url= https://planetmath.org/lobstheorem
|title= Löb's theorem
|date= 22 March 2013
|at= [[PlanetMath]]
|access-date= 14 December 2023
}}
* {{SEP|logic-provability|Provability Logic|Rineke (L.C.) Verbrugge|2017}}
* {{Cite web
|url= https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/the-cartoon-guide-to-loeb-s-theorem
|title= The Cartoon Guide to Löb’s Theorem
|last= Yudkowsky
|first= Eliezer
|author-link= Eliezer Yudkowsky
|date= 17 August 2008
|access-date= 14 December 2023
}}

{{DEFAULTSORT:れえぶのていり}}
[[Category:数理論理学]]
[[Category:数学基礎論の定理]]
[[Category:メタ定理]]
[[Category:証明可能性論理]]
[[Category:公理]]
[[Category:数学に関する記事]]