Gödel's paper on formally undecidable propositions  raised the possibility that finite combinatorial theorems could be discovered which are independent of powerful axiomatic systems such as first-order Peano Arithmetic. An important advance was made by J. Paris in the late 1970's; building on joint work with L. Kirby, he used model-theoretic techniques to investigate arithmetic incompleteness and proved theorems of finite combinatorics which were unprovable in Peano Arithmetic . The Paris-Harrington paper  gives a self-contained presentation of the proof that a straightforward variant of the familiar finite Ramsey Theorem is independent of Peano Arithmetic. In this paper, we consider a simple finite corollary of a theorem of infinite combinatorics of Erdös and Rado  and show it to be independent of Peano Arithmetic. This formulation avoids the Paris-Harrington notion of relatively large finite set and deals with a generalized notion of partition. This shift of focus also provides for simplifications in the proofs and directly yields a level-by-level analysis for subsystems of Peano Arithmetic analogous to that in . We have tried to provide a treatment of the proof whose organization and brevity make it suitable for expository purposes. These results were first discussed in 1982, and almost all the details worked out by a year later. We would like to thank Peter Clote for his later interest and involvement in this web of ideas. © 1987.
Kanamori, A., & McAloon, K. (1987). On Gödel incompleteness and finite combinatorics. Annals of Pure and Applied Logic, 33(C), 23–41. https://doi.org/10.1016/0168-0072(87)90074-1