Wikipedia - ゲーデルの不完全性定理
なんか色々誤解をしてそうなのでWikipedia(en) も読むことにしたい。
Gödel's incompleteness theorems - Wikipedia
これからも追記予定
二つの完全性
syntactically complete: Aもしくは¬Aが証明できる
semantically complete: 全ての恒真式が証明可能
・ゲーデルが述語論理に対して示した完全性: semantical complete
・述語論理はsemanticalにはcompleteだが、syntacticallyにはcompleteではない
・ゲーデル第一不完全性定理での完全性: syntactical completeness
ゲーデル文とロッサー文
第一不完全性定理の証明は ω無矛盾を前提としたゲーデル版と 無矛盾を前提としたロッサー版がある。どちらも、証明も反証もできない文の存在を証明する。
・ゲーデル文「私は証明できない」
・ロッサー文「もし私が証明可能なら、その否定はより短い証明でなされる」
ロッサー版の方がより一般的な内容であるが、算術を含む体系はω無矛盾であるので、ゲーデル版がそのまま使える。
併せて読む: Rosser's trick - Wikipedia