Париc-Харрингтон теоремасы: Пеано арифметикасы шеше алмайтын Рамси теориясының принципі

Theorem that a certain principle in Ramsey theory is true, but not provable in Peano arithmetic
In mathematical logic, the Paris–Harrington theorem states that a certain combinatorial principle in Ramsey theory, namely the strengthened finite Ramsey theorem, which is expressible in Peano arithmetic, is not provable in this system. The combinatorial principle is, however, provable in slightly stronger systems. This result has been described by some (such as the editor of the Handbook of Mathematical Logic in the references below) as the first "natural" example of a true statement about the integers that could be stated in the language of arithmetic, but not proved in Peano arithmetic; it was already known that such statements existed by Gödel's first incompleteness theorem.

Roughly speaking, Jeff Paris and Leo Harrington (1977) showed that the strengthened finite Ramsey theorem is unprovable in Peano arithmetic by showing in Peano arithmetic that it implies the consistency of Peano arithmetic itself. Since Peano arithmetic cannot prove its own consistency by Gödel's second incompleteness theorem, this shows that Peano arithmetic cannot prove the strengthened finite Ramsey theorem. The combinatorial principle can be proven assuming induction up to for a relevant classes of formulas. Alternatively, it can be proven assuming the reflection principle, for the arithmetic theory, for sentences. The reflection principle also implies the consistency of Peano arithmetic. It is provable in second order arithmetic (or the far stronger Zermelo–Fraenkel set theory) and so is true in the standard model. The smallest number N that satisfies the strengthened finite Ramsey theorem is then a computable function of n, m, k, but grows extremely fast. In particular it is not primitive recursive, but it is also far faster growing than standard examples of non primitive recursive functions such as the Ackermann function. It dominates every computable function provably total in Peano arithmetic, which includes functions such as the Ackermann function.