現実的には証明できない命題
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:11 UTC 版)
「ゲーデルの加速定理」の記事における「現実的には証明できない命題」の解説
具体的な例を見るために、最短の形式的証明がとてつもなく長大となる文を構成しよう。形式化された対角線論法によって φ「この文は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」 なる内容的意味を持つ文を構成する。（ここで「グーゴルプレックス個の記号からなる」という部分を取り除くと不完全性定理の決定不能な文が得られる。）コーディングを工夫すれば φ がΣ1論理式となるようにできる。φ はペアノ算術から証明可能である：もし証明不能なら「高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」が標準模型で真なので、Σ1完全性より φ は証明可能である。これは不合理。したがって φ は証明可能である。するとΣ1健全性より φ は標準模型で真である。つまり「φ は高々グーゴルプレックス個の記号からなる（ペアノ算術からの）形式的証明を持たない」から、φ の形式的証明はグーゴルプレックス個よりも多くの記号から構成される。 φはより強い体系ではもっと短い形式的証明を持つ：例えばペアノ算術に自身の無矛盾性を表す公理 Con(PA) を追加した体系を用いればよい。（追加された公理は不完全性定理よりペアノ算術からは証明不能である。）すると、上の背理法による議論を体系内で実行することができ、より短い形式的証明が得られる： ¬φ と仮定する。ここから ProvablePA(φ) を得る。他方で ¬φ に形式化されたΣ1完全性を適用すれば ProvablePA(¬φ) を得る。ここに形式化されたモーダス・ポネンスを適用すれば ProvablePA(⊥) すなわち ¬Con(PA) を得る。公理 Con(PA) とモーダス・ポネンスによって矛盾 ⊥ を得る。背理法によって（仮定なしで） φ を得る。 以上の議論におけるペアノ算術は、別のより強い無矛盾な体系に置き換えられる。またグーゴルプレックスもその体系で（短く）記述できる別の任意の数字に置き換えられる。 ハービー・フリードマンは上のような性質を満たすような明示的で自然な例をいくつか見つけた。それはペアノ算術やほかの形式的体系における文であり、その最短の証明は非常に長い。例えば、以下の主張 「ある自然数 n {\displaystyle n} が存在して、もし根付き木からなる列 T 1 , … , T n {\displaystyle T_{1},\ldots ,T_{n}} で T k {\displaystyle T_{k}} が高々 k + 10 {\displaystyle k+10} 頂点からなるとき、 ある木はそれより後の木へ同相的に埋め込める（英語版）」 はペアノ算術において証明可能だが、その最短の証明は少なくとも長さ A ( 1000 ) {\displaystyle A(1000)} を持つ。ここで A ( 0 ) = 1 {\displaystyle A(0)=1} かつ A ( n + 1 ) = 2 A ( n ) {\displaystyle A(n+1)=2^{A(n)}} である。この主張はクラスカルの定理の特別な場合であり、二階算術においてより短い証明を持つ。 ペアノ算術に上記の主張の否定を付け加えたならば、矛盾した理論であって、その最短の矛盾（の証明）が想像を絶するほどに長いものが得られる。上記の主張を φ {\displaystyle \varphi } とおく。いま P A + ¬ φ {\displaystyle PA+\neg \varphi } から矛盾に至る証明が与えられたとする。すると（論理が適切に形式化されている限り）証明の長さを定数倍程度しか増やさない仕方で、 P A {\displaystyle PA} から φ {\displaystyle \varphi } に至る証明が得られる。（例えば、ベースとなる論理体系が帰謬法を推論規則として陽に含む場合、証明の長さは1ステップ分しか増えない。）後者の証明は途轍もなく長いので、前者の証明もまた途轍もなく長い。
※この「現実的には証明できない命題」の解説は、「ゲーデルの加速定理」の解説の一部です。
「現実的には証明できない命題」を含む「ゲーデルの加速定理」の記事については、「ゲーデルの加速定理」の概要を参照ください。
- 現実的には証明できない命題のページへのリンク
