An analysis of Ramsey's theorem (Q1327381)

The main result of this paper may be paraphrased as follows. A collection \(B\) of finite sets of natural numbers is called unavoidable iff every infinite set of natural numbers has a subset in \(B\). Let \(s\) be a fixed natural number, the number of colours. Given a collection \(B\) of finite sets of natural numbers we denote by \(B_ n\) the collection of those sets of natural numbers that, whenever their \(n\)-element-subsets are coloured by \(s\) colours, will always have a homogeneous subset in \(B\), where a homogeneous set is one such that every one of its \(n\)-element- subsets gets one and the same colour. The main theorem of the paper says that, if \(B\) is unavoidable, each \(B_ n\) is unavoidable. Given any number \(k\), we may choose \(B\) to be the collection of those finite sets of natural numbers that have their first element greater than \(k\), and whose number of elements exceeds its first element. We then obtain the famous generalization by \textit{J. Paris} and \textit{L. Harrington} of Ramsey's Theorem [see: ``A mathematical incompleteness in Peano arithmetic'', in: Handbook of mathematical logic (J. Barwise, ed.), 1133- 1142 (1977; Zbl 0443.03001)]. The author gives a beautiful constructive proof of his main theorem (the classical argument by compactness is of course unconstructive), thus answering a question raised by G. Stolzenberg. A main step in the author's argument is his replacement of the notion of ``unavoidable'' by the notion of ``ample''. The latter notion is defined inductively and coincides with the former one in classical mathematics, and also, by Brouwer's bar theorem, in intuitionistic mathematics, but not in the more general context of constructive mathematics. The author's Lemma 7 is a very nice constructive substitute for König's Infinity Lemma, very different from the intuitionistic fan theorem. The author later saw that his result is related to an intuitionistic version of the infinite Ramsey Theorem given by the reviewer and \textit{M. Bezem} [J. Lond. Math. Soc., II. Ser. 47, 193-211 (1993; Zbl 0729.03034)]. He found and published his own proof of the infinite Ramsey Theorem [Theor. Comput. Sci. 115, 63-75 (1993; Zbl 0801.03039)].