レーブの定理
(Löb's theorem から転送)
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2024/05/04 07:33 UTC 版)
数理論理学におけるレーブの定理 (Löb's theorem) は、ペアノ算術 (PA) (またはPAを含む任意の形式体系)において、任意の論理式Pについて、「PがPAで証明可能ならばPである」ことがPAで証明可能ならば、PはPAで証明可能であることを述べている。Prov(P)が論理式Pが証明可能であることを意味する場合、レーブの定理をより形式的に表現すると次のようになる。
- ^ PAが矛盾していない限り(その場合、を含むすべての文が証明可能である)。
- ^ Löb 1955.
- ^ “Löb's theorem is (almost) the Y combinator”. Semantic Domain. 2024年4月9日閲覧。
- ^ Smullyan 1986.
- ^ Lindström 2006.
- 1 レーブの定理とは
- 2 レーブの定理の概要
- 3 例
- 4 逆: レーブの定理から様相不動点の存在を導く
- レーブの定理のページへのリンク