[FOM] nonconstructive proofs

[Harvey Friedman]

The nowadays usual proof of Kruskal's theorem is highly nonconstructive.
There are known constructive proofs, in reasonable senses, but they appear
considerably more involved.

THEOREM 1 (Kruskal). Among any infinite sequence of finite trees, one is inf
preserving embeddable in a later one.

Here are some more concrete and simpler situations. The usual proof of the
following is also highly nonconstructive, and there are also constructive
proofs, that seem considerably more involved.

THEOREM 2. In any sufficiently long finite sequence x_1,...,x_n from
{1,2,3}, there exists 1 <= i < j <= n/2 such that x_i,...,x_2i is a
subsequence of x_j,...,x_2j.

THEOREM 3. In any sufficiently long finite sequence x_1,...,x_n from
{1,...,k}, there exists 1 <= i < j <= n/2 such that x_i,...,x_2i is a
subsequence of x_j,...,x_2j.

Harvey Friedman