パリス＝ハーリントンの定理

数理論理学においてパリス・ハーリントンの定理（ぱりすはーりんとんのていり、英: Paris–Harrington theorem）は、ラムゼー理論におけるある規則、すなわち強化版有限ラムゼーの定理が、正しいにもかかわらずペアノ算術の枠内では証明できないという定理である。これは整数に関する正しい命題の中で、算術の用語で表現できるがペアノ算術では証明できない最初の「自然な」例である。そのような命題が存在すること自体はゲーデルの不完全性定理によってすでに知られていた。

強化版有限ラムゼーの定理

強化版有限ラムゼーの定理は自然数と色付けに関する以下の定理である。

• 任意の正整数の組 n, k, m (m ≥ n)に対して、以下の条件を満たす N が存在する: S = {1, 2, 3,..., N} の n 要素の部分集合のそれぞれを k 色を使って色付けしたとき、少なくとも m 要素を持つ S の部分集合 Y で、Y のすべての n 要素の部分集合が同じ色であり、かつ Y の要素数は Y の要素のうち最も小さいものの値以上であるようなものが存在する。

「Y の要素数は Y の要素の最低値以上である」という条件がなければ、この定理は${\displaystyle K_{{\mathcal {P}}_{n}(S)}}$に対し N を

${\displaystyle {\binom {N}{n}}=|{\mathcal {P}}_{n}(S)|\geq R(\,\underbrace {m,m,\ldots ,m} _{k}\,)}$

としたときの有限ラムゼーの定理より導かれる。

さらに、強化版有限ラムゼーの定理は無限ラムゼーの定理から、有限ラムゼーの定理を導出するのとほぼ同じ方法で導出される。証明はコンパクト性定理を用い、二階述語論理の中で行われる。^[1]

パリス・ハーリントンの定理

大雑把に言えば Jeff Paris と Leo Harrington (1977) は、ペアノ代数の中では強化版有限ラムゼーの定理がペアノ代数それ自体の無矛盾性を帰結することを示した。ゲーデルの第二不完全性定理によってペアノ代数はそれ自体の無矛盾性を証明することはできないので、結局、強化版有限ラムゼーの定理はペアノ代数では証明できないということになる。

強化版有限ラムゼーの定理を満たす数 N は n, m, k の計算可能関数であるが、とても速く増加する。それは原始再帰関数ではないが、急速に増加する原始再帰関数でない関数の例としてよく出されるアッカーマン関数のようなものに比べてもはるかに速く増加する。ペアノ代数はアッカーマン関数がすべての値に対して定義されていることを証明することができるが、強化版有限ラムゼーの定理の場合はその増加があまりにも速く、すべての値に対して定義されていることすら証明できない。