エーレンフォイヒト・ミッシェルスキーの加速定理
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:11 UTC 版)
「ゲーデルの加速定理」の記事における「エーレンフォイヒト・ミッシェルスキーの加速定理」の解説
帰納的理論 T {\displaystyle T} と文 φ {\displaystyle \varphi } について T + ¬ φ {\displaystyle T+\neg \varphi } は決定不可能であると仮定する。したがってとくに φ {\displaystyle \varphi } は T {\displaystyle T} で証明できない。この条件を満たす例としては、ロビンソン算術と加法や乗法の交換法則、ペアノ算術とグッドスタインの定理やパリス・ハーリントンの定理（英語版）、ZFと選択公理や決定性公理、ZFCと連続体仮説や巨大基数公理などがある。 T {\displaystyle T} における証明と T + φ {\displaystyle T+\varphi } における証明の複雑性を比較したい。ただし証明の複雑性を測る関数 | ⋅ | {\displaystyle |\cdot |} は静的複雑性測度の条件を満たすものとする。すなわち、証明の複雑さの上限を固定する毎に、その複雑さ未満の証明は有限個に限られ、かつそのような証明全体の成す有限集合を（与えられた上限から）計算できるものとする。理論 T ′ {\displaystyle T'} における文 ψ {\displaystyle \psi } の証明の複雑さの最小値を ‖ ψ ‖ T ′ {\displaystyle \Vert \psi \Vert _{T'}} と書くことにする。この証明の最小の複雑さを与える関数は（証明可能な文全体を定義域とする）計算可能関数である。 エーレンフォイヒト（英語版）とミッシェルスキー（英語版）は計算可能性理論を用いて次の加速定理を証明した： 任意の計算可能関数 r {\displaystyle r} に対して、 T {\displaystyle T} で証明可能な文 ψ {\displaystyle \psi } が存在して r ( ‖ ψ ‖ T + φ ) ≤ ‖ ψ ‖ T {\displaystyle r(\Vert \psi \Vert _{T+\varphi })\leq \Vert \psi \Vert _{T}} が成り立つ。 例えば r ( x ) = 2 x {\displaystyle r(x)=2x} とすると 2 ‖ ψ ‖ T + φ ≤ ‖ ψ ‖ T {\displaystyle 2\Vert \psi \Vert _{T+\varphi }\leq \Vert \psi \Vert _{T}} より ‖ ψ ‖ T + φ ≤ ‖ ψ ‖ T / 2 {\displaystyle \Vert \psi \Vert _{T+\varphi }\leq \Vert \psi \Vert _{T}/2} となる。つまり証明のサイズが半分に落ちる。同様に、 r {\displaystyle r} を指数関数とすれば、後式の右辺は対数関数となる。このように、増加の激しい関数 r {\displaystyle r} を取る毎に、その逆関数（これは増加が緩やかとなる）に対応した証明の短縮（加速）が起こる。
※この「エーレンフォイヒト・ミッシェルスキーの加速定理」の解説は、「ゲーデルの加速定理」の解説の一部です。
「エーレンフォイヒト・ミッシェルスキーの加速定理」を含む「ゲーデルの加速定理」の記事については、「ゲーデルの加速定理」の概要を参照ください。
- エーレンフォイヒトミッシェルスキーの加速定理のページへのリンク
