[FOM] Avoiding patterns/RCA/WKL

[Alasdair Urquhart]

I don't think you need WKL to prove the existence of an
infinite square-free word.  The monograph "Combinatorics
on Words" by M. Lothaire proves this result on pp. 23-26.
Lothaire first constructs the infinite word of Thue-Morse
by a simple recursive procedure.  Then an infinite
square-free word is constructed on p. 26 via a
substitution.  WKL doesn't seem to be needed.

On Mon, 12 Nov 2012, pax0 at seznam.cz wrote:

> It is well-known that there is an infinite word not containing a square (avoiding the pattern xx)
> over the three letter alphabet {0,1,2}.
> My question is: Do we need WKL over RCA for this result?
> The intuition is that there is a finitely branching tree of square-free prefixes in which we have to find an infinite branch.
> But is WKL really used here?
> Thank you, Jan Pax