Secuencias de una función computable

Question

¿Existe alguna función computable $f(n)$, que dada cualquier entero $n$, se haya demostrado que devuelve ya sea $0$ o $1$ en tiempo finito, y para la cual se haya demostrado que la afirmación "$f(1), f(2), f(3),\ldots$ contiene secuencias arbitrariamente largas de $0$'s" es indemostrable en PA o ZFC?

Si no, ¿existe alguna prueba de la existencia o no existencia de tal función?

Editar: ¿Existe alguna que también sea moralmente indemostrable?

Answer 1

Sea $G$ una oración de Gödel (con significado intuitivo "No puedo ser demostrado"), y tomemos $$f(n)=\cases{0&\text{si }G\text{ tiene una demostración con número de Gödel }

Answer 2

Sea $G(n)$ la secuencia Goodstein con primer elemento $n$, y tome $$f(n)=\cases{0&\text{si }0 \ \text{es un elemento de} \ G(n) \\1&\text{en otro caso.} }$$

EDICIÓN: ZFC demuestra que la afirmación $\unicode{8220}f(n)=0\text{ para todo }n\unicode{8221}$ y también demuestra que esa afirmación no puede ser demostrada en PA. Sin embargo, esto solo podría no implicar que PA no pueda demostrar la afirmación más débil $\unicode{8220}f(1),f(2),f(3),\ldots$ contiene secuencias de $0\text{s}$ de longitud arbitraria.$\unicode{8221} Dado que no sé si PA puede de hecho demostrar la última (más débil) afirmación, no estoy seguro de si mi respuesta anterior es correcta después de todo.