up:: Programming
up:: Math
概要
ゲーデルの不完全性定理 - Wikipedia
Gödel’s incompleteness theorems - Wikipedia
形式主義上では、自然数論の無矛盾性の証明が成立しないことを示した定理。
未だ発見はされていないものの、自然数論が矛盾する可能性があることを示した。もし矛盾がある場合、ある命題とその否定が同時に真であると証明される。
不完全性定理 - 理学のキーワード - 東京大学 大学院理学系研究科・理学部
第一と第二がある。
第一は「数学を矛盾なくどのように形式化しても、証明も反証もできない命題が存在する」という定理。
第二は「どのような形式的体型も、その体系自身が矛盾していないことを証明できない」という定理。
これら定理は再帰的プログラミングに利用されている。
1931年、クルト・ゲーデルによって証明された定理。
前提知識 - 形式主義
形式主義は数学上の推論を抽象的な命題の集合ではなく、純粋な記号操作ととらえる考え。それ自体は対象や性質に迫るものではない。
それは公理と推論法則というルールから導けるゲームと例えられる。ルールを取り換えることで出来る異なるゲームはそれぞれ同等とされる。
同等とは厳密な論理的推論であるということであり、ルールがどうでも関係ない。
この公理と推論法則は、形式的公理系とも呼ばれる。形式的公理系を厳密に言うと、一つの形式体型において議論の前提として置かれる一連の公理の集まり。
ざっくり言うと形式ごとの前提の公理。ルールに当たる。
第一
最小限の算術を含む一貫した形式的システムにおいて、形式的に決定不能な命題が見つかるという定理。
例えばAというシステム内ではAやnotAは定義できない。数学に必要なすべての理論を書きだすことは不可能、という意味でもある。
これの証明はゲーデル文と呼ばれる特別な文を使う。
これは「この文は証明不能である」という意味合いを厳密な論理的推論で表現したもの。もしこの文が真なら証明不能。この文が偽なら矛盾。うそつきのパラドックスみたいなの。
詳しく言う。
初等的な自然数論とはペアノ算術。これは自然数を定義する公理。
一貫した形式的システムとはω無矛盾な公理的理論。
ω無矛盾とは通常の無矛盾より強力な無矛盾。通常の無矛盾は論理式PにおいてPとnotPが同時には成り立たないという性質。ω無矛盾は
第二
ペアノ算術を含む一貫した形式的システムは、その自己一貫性を証明できない。
逆に言うと自己一貫性を定式化できるという形式的システムは、それ自身が矛盾している場合に限り自己一貫性を証明できる。
証明も反証もできない命題の一例。これは第一定理に使った文を「この形式システムは一貫している」に置き換えると分かる。これが真だと、第一定理により存在するはずの証明も反証も不可能な分が存在しないため、矛盾となる。