ゲーデルの不完全性定理 - funyarara @ Wiki

• ヒルベルト計画
  • 形式的体系の導入
    • 数学を《形式的体系》として表現する
    • すなわち、数学を形式的な記号の列として表現する
  • 無矛盾性の証明
    • 形式的体系に《矛盾がない》事を証明する。
    • すなわち、任意の論理式Ａに対して《Ａと￢Ａの両方は形式的に証明できない》ことを証明する
  • 完全性の証明
    • 形式的体系が《完全である》ことを証明する。
    • すなわち、任意の文Ａに対して、《Ａと￢Ａの少なくとも片方は形式的に証明できる》ことを証明する。

《形式的証明》
論理式 , , ・・・, の有限列の一種で、次の条件を満たすもの。
●は公理である。
●は公理である。または、から推論規則でを導ける。
●は公理である。または、,のどちらか（あるいは両方）から推論規則でを導ける。
●・　・　・
●は公理である。または、それ以前の論理式のどれかから推論規則でを導ける。

• ゲーデルの第一不完全性定理
  • ある条件を満たす形式的体系には、以下の両方が成り立つ文Ａが存在する
    • その形式的体系には、Ａの形式的証明は存在しない。
    • その形式的体系には、￢Ａの形式的証明は存在しない。
• ゲーデルの第二不完全性定理
  • ある条件を満たす形式的体系には、自己の無矛盾性を表現する文の形式的証明は存在しない。