Premium
Where can we really prove instances of the Paris‐Harrington principle?
Author(s) -
Freund Anton
Publication year - 2016
Publication title -
pamm
Language(s) - English
Resource type - Journals
ISSN - 1617-7061
DOI - 10.1002/pamm.201610440
Subject(s) - decidability , calculus (dental) , mathematical economics , mathematics , automated theorem proving , discrete mathematics , computer science , algorithm , medicine , dentistry
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)