The Kolakoski challenge

[José Manuel Rodriguez Caballero]

Engaged in the philosophical topic concerning determinism versus free will, the artist and recreational mathematician William Kolakoski [2] defined a sequence [1] in symbols 1 and 2, which coincides with the sequence of its run-length encoding (the initial term is frequently chosen to be 1, but this is not essential). Such a sequence was previously studied by the mathematician Rufus Oldenburger [3]. The first terms of this sequence are:

1,2,2,1,1,2,1,2,2,1,2,2,1,1,2,1,1,2,2,1,2,1,1,2,1,2,2,1,1...

It is unknown whether or not the frequency of symbols 1’s converge. My question is the following: 

Is there an axiomatic theory in which the question concerning the convergence of the frequency of the symbol 1 in the Kolakoski sequence can be expressed, but the answer cannot be deduced from the axioms?

I am thinking in something like the fact that Goodstein theorem can be formulated in first-order Peano arithmetic, but it cannot be proved in this system [4].

Kind regards,
Jose M.

References
[1] https://oeis.org/A000002

[2] https://en.m.wikipedia.org/wiki/William_Kolakoski

[3] Oldenburger, Rufus (1939). Exponent trajectories in symbolic dynamics, Trans. Amer. Math. Soc. 46: 453–466.

[4] KIRBY, Laurie et PARIS, Jeff. Accessible Independence Results for Peano Arithmetic. Bulletin of the London Mathematical Society, 1982, vol. 14, no 4, p. 285-293.

Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200126/a2d935c2/attachment.html>