An intuitionistic proof of Kruskal's theorem (Q1879322)

Vazsonyi's conjecture says that the collection of all finite trees is well-quasi-ordered by the relation of embeddability, that is, for every infinite sequence \(\alpha(0),\alpha(1),\alpha(2),\dots\) of finite trees there exist \(i, j\) such that \(i < j\) and \(\alpha(i)\) embeds into \(\alpha(j)\). In 1960, Kruskal established an even stronger result that he called the Tree Theorem. The paper under review presents a detailed proof of an intuitionistic version of Kruskal's Theorem; moreover, it discusses a number of intuitionistic variants of many other classical Ramseyan theorems. With few exceptions, the proofs of the results do not exceed the bounds of the system of intuitionistic analysis \textbf{FIM} of Kleene and Vesley. Contents: Dickson's lemma; Almost full relations; Some induction principles and Brouwer's Thesis; Ramsey's Theorem; The Finite Sequence Theorem; Vazsonyi's conjecture for binary trees; Higman's Theorem; Vazsonyi's conjecture and the Tree Theorem; Minimal-bad-sequence arguments; The principle of open induction; Concluding remarks.