[FOM] Avoiding patterns/RCA/WKL

[Alberto Marcone]

Il 12/11/2012 21:08, pax0 at seznam.cz ha scritto:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

I think the answer to Jan's question is negative.
http://en.wikipedia.org/wiki/Squarefree_word lists several explicit 
definitions of square-free words. Some of these (e.g. the one starting 
from the Thue–Morse sequence) are computable, and I expect (although I 
did not check the details) that everything is provable in RCA_0.

Best wishes,
Alberto
-- 
Alberto Marcone                            alberto.marcone at dimi.uniud.it
Dip. di Matematica e Informatica
Universita' di Udine                                tel: +39-0432-558482
via delle Scienze 206                               fax: +39-0432-558499
33100 Udine
Italy                       http://users.dimi.uniud.it/~alberto.marcone/