11:56 2003/06/25
証明可能な自己参照型命題の存在
記：斎藤吉彦
「ホーキングの苦悩命題は決定不能か？」の議論では証明可能な自己参照型命題の存在が暗に示されただけであった。ここではその存在の証明を与える。
公理系をペアノ算術とする。
ゲーデルの対角線定理によって、次の事を満たす論理式Φが存在する。
（１） Φ←→Pr（Φ）は証明可能
ここで、Prはペアノ算術における可証性述語で、Pr(A）は「論理式Aは証明可能を意味する」論理式である。
レーブの定理（数学基礎論講義・田中一之著・日本評論者 １０４ページ）より
（２） ”Pr(Φ）→Φは証明可能” ⇔ ”Φは証明可能”
（１）（２）よりΦは証明可能。
Q.E.D.