数学基礎論・数理論理学　その9

なんか議論が錯綜しているようなのでまとめると、
健全(論理式が、証明可能⇒真)、完全(論理式が、真⇒証明可能)。

述語論理は健全かつ完全。

述語論理に新公理を追加したPAは健全だが完全でない。
つまり恒真なのに証明不可能な論理式が存在する。

この論理式が存在することを主張するのが第1不完全性定理。
ここでいう不完全とは、論理式に否定記号を付けても付けなくても証明できないってこと。
この定理の仮定で無矛盾が必要な理由は、矛盾してたらどんな論理式でも証明できるから。

で、その論理式が「PAは無矛盾。」だと主張するのが第2不完全性定理。