I am sketching here a proof of Harvey Friedman‘s result mentioned in lecture. The proof will not be needed for the rest of the course, but it is a nice argument that you may enjoy reading.

Recall that a sequence has **property ** iff there are no integers such that the sequence is a subsequence of .

Here, we are using the notion of subsequence where terms must appear in order but are not required to be consecutive: A sequence is a **subsequence** of iff there are indices such that

Theorem (H. Friedman, 2001).For any positive integer there is a longest finite sequence in letters with property .

(Of course, once we know that the theorem is true, we can proceed as in lecture and define as the length of this longest sequence.)