Where can we really prove instances of the Paris‐Harrington principle?

A fundamental question in mathematical logic asks: What are the minimal assumptions and deduction principles required to prove a particular theorem? Now consider the special case of a theorem that can be established by checking a finite number of decidable cases — think of a single instance of the finite Ramsey theorem. In this particular situation the answer to our question is trivial: The theorem can be demonstrated by an explicit verification, thus without the use of any “strong” proof principles. This answer, however, is not very satisfying: An explicit verification may be unfeasible if there is an enormous number of cases to check. At the same time there might be a short and meaningful proof using stronger proof methods. Such a situation suggests a modified question: What are the minimal assumptions and deduction principles required for a reasonably short proof of the given theorem? Our contribution explores this question for instances of the Paris‐Harrington principle. (© 2016 Wiley‐VCH Verlag GmbH & Co. KGaA, Weinheim)