>>58
(引用開始)
>>n階算術の体系で証明可能な命題であって、
>>n+1階算術ではより短い証明を持つもの
英語版のWikipediaにこんなこと書かれてないけど？
(引用終り)

なるほど
良い指摘だね

1）まず、wikipedia仏語版が下記だ
　非公式の説明：”ある与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い、比較的短い主張の明示的な例を構築しました”
2）さらに、より一般に ja.wikipediaの加速定理 の”形式的体系に関する加速定理”の項も見ておいた方がいいだろう
3）なので、”ある与えられた形式体系”→ ”n階算術”に置き換え可能だね
　つまり、 ”n階算術”の中に 「最短の証明が異常に長い」命題があって、それを短くする 加速法が存在する
　上記は、それをn+1階算術として 説明しているようだ
　その記述が正しいかどうかは、算術の専門家に任せるｗ ；ｐ）

大事なことは
人の思考は ”一階述語論理に縛られる必要は、全くない！” ってこと
　
(参考)
fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_d%27acc%C3%A9l%C3%A9ration_de_G%C3%B6del
（google訳）ゲーデルの加速定理
非公式の説明
クルト・ゲーデルは、第一不完全性定理の証明を応用して、与えられた形式体系で証明可能であるが、その体系における最短の証明が異常に長い、比較的短い主張の明示的な例を構築しました。したがって、ステートメントは次のようになります。
「この命題は、ゴーゴルプレックス未満の記号でペアノ公理（単独）を使用して証明することはできません。」
(より正確には、次のセクションで説明するように、適切なゲーデル コードを使用して、Gがシンボルのゴーゴプレックス未満では証明できないことをエンコードするステートメントG ) は確かに真であり、PA で実証することさえできます (ペアノ)算術）;さらに、PA に矛盾がない場合、証明には必然的に複数のシンボルのゴゴプレックスが含まれます。
この議論は、PA よりも強力なコヒーレントシステム(たとえば、ZFC )に一般化されます 。 gogolplex は、システムが (比較的) 少数の記号で記述できる任意の数値 (例えば、グラハム数) に置き換えることができます。
その他の例と結果
Jean-Paul Delahaye は2 、 1971 年に、より強力な結果の実証を指摘し、この現象は、決定不可能な命題を追加できるあらゆる理論で発生することを示しました

ja.wikipedia.org/wiki/%E5%8A%A0%E9%80%9F%E5%AE%9A%E7%90%86
加速定理は、ある問題を解く算法に対し、同じ問題をより早く解く算法（また一般に、使用する資源がより少ない算法）の存在を示す定理である。
形式的体系に関する加速定理
理論 T とその拡大理論 S について「T において証明可能な論理式で
S においてはより簡単に証明できるものが存在する」という形の定理は、計算複雑性に関する加速定理の類比として、同じく加速定理と呼ばれる。その代表的なものとしてはゲーデルの加速定理がある。これら異なるタイプの加速定理の間には或る種の対応が存在する。例えば、ブラムの加速定理の変種であるハルトマニスの加速定理を用いてゲーデルの加速定理が証明できることが知られている