22/04/30 10:13:50.59 .net
>>790のつづき
で
「任意の命題について、それが証明可能か否か
判定できるアルゴリズムが存在する」と
「任意の命題について、それがトートロジー（恒真命題）であるとき
その証明を返すような手続きが存在する」の違い
ワカリマスカ？
実は
「任意の命題について、それがトートロジーでないとき
それを教えてくれる手続き」
が存在しないんですよ
ま、命題の充足判定の裏返しですけどね
トートロジーでない命題⇔その否定が充足可能な命題
ですから
命題論理ならNP完全ですけど、
述語論理なら決定不能問題です
ついでにいうと、おおざっぱにいえば
「恒真なら証明可能」は述語論理の完全性定理
「恒真でないなら決定不能」は不完全性定理
ですけどね どっちもゲーデ