Another proof of the intuitionistic Ramsey theorem (Q685402)

The intuitionistic version of Ramsey's theorem mentioned in the title of this paper says the following: If \(R\) and \(S\) are almost full binary relations on the set \(\mathbb{N}\) of natural numbers, their intersection \(R\cap S\) will be almost full. Here a relation \(R\) is called almost full if and only if for any strictly increasing infinite sequence \(\alpha(0), \alpha(1), \alpha(2),\dots\) of natural numbers one may (effectively) find \(i\), \(j\) in \(\mathbb{N}\) such that \(i<j\) and \(\alpha(i) R\alpha (j)\). This theorem was formulated and proved by the reviewer and \textit{M. Bezem} [J. Lond. Math. Soc., II. Ser. 47, No. 2, 193-211 (1993; Zbl 0729.03034)]. The author gives a new and nice argument for this theorem, similar to the one contained in his earlier paper: ``A direct proof of the intuitionistic Ramsey theorem'' [Lect. Notes Comput. Sci. 530, 164-172 (1991; Zbl 0794.03086)]. The present paper should probably be seen as a mature version of this earlier one. In fact, both papers contain the author's second proof of the intuitionistic Ramsey theorem, as this theorem, as shown by the reviewer and Bezem, also follows easily from the main result of the author's paper: ``An analysis of Ramsey's theorem'' [Inf. Comput. 110, 297-304 (1994)] In his earlier paper [loc. cit.], the author couches his argument in the language of traditional intuitionistic analysis, although he prefers a terminology that should appeal to a theoretical computer scientist. He also sketches how to obtain another version of the theorem. In his view, such a version is desirable for two reasons. First, as suggested by \textit{P. Martin-Löf} [Notes on constructive mathematics (1970; Zbl 0273.02021)], it would be better to avoid the use of Brouwer's thesis. Secondly, the author prefers not to mention (``unobservable'') infinite sequences of natural numbers. In the paper under review this new version is given in full detail, the most important step being an appropriate change in the definition of ``almost full'' and the author even omits the earlier version. I must admit that I find the earlier version easier to understand, but this may be due to old habits and stiffness of mind. Like the reviewer and Bezem, the author generalizes Ramsey's theorem to \(n\)-ary relations. He might have gone further and used his argument to prove an intuitionistic version of the so-called clopen Ramsey theorem. The argument given by the reviewer and Bezem does not admit of such a straightforward generalization. The author states that his argument is ``essentially the same'' as the classical argument that he sketches in Section 1.2 of his paper. I don't agree. These words might give the wrong impression that it is easy to find the new argument from the classical one.