Find an infinite sequence of statements so that truthness of all sequence elements is unprovable Let us consider a function $f: \mathbb N \to \left\{0, 1\right\}$ with finite description length (i.e. describable by a finite length program for a Turing machine) satisfying the following conditions:


*

*$f(n)$ is computable in finite time for any $n,$ that means that it is possible to prove that the program for a Turing machine that calculates $f(n)$ always halts;

*It is impossible to compute in finite time $\prod\limits_{n=1}^{\infty} f(n),$ i.e. there is no program for a Turing machine that in finite time checks the fact that $\forall n: f(n) = 1$ and outputs $1$ in this case and $0$ otherwise.


The questions are:


*

*Is it possible to prove that such function exists or does not exist?

*If it is possible, are there some concrete examples?



Here are some my thoughts.
One possible candidate for such function is $f(n) = I[a_n = 1]$ where $\left\{a_n\right\}$ is Collatz sequence and $I[\cdot]$ is the indicator function. However for me it is not clear is it possible to prove Collatz conjecture to be unprovable or we couldn't even prove that unprovability.
I would appreciate any reading recommendations on this topic.
 A: There are some problems with your function. First, notice that in (1) it's not actually the same to say "$f(n)$ is computable in finite time for every $n$" and "it is provable that the Turing machine computing $f$ halts on every input". A good counterexample is the Turing machine which, regardless of its input, searches for a proof of a contradiction from Peano Arithmetic; this Turing machine always fails to halt (provided PA is consistent) but that fact can't be proven in Peano Arithmetic.
In (2), $\prod_{n=1}^{\infty}f(n)$ is a single number (either $1$ or $0$). A single number is always computable, in this case either by the Turing machine that always outputs $0$ or by the machine that always outputs $1$. Now, we may not be able to decide which one is the right one, but that's a provability question rather than a computability one. In general, in order for it to make sense to say something is noncomputable, you need it to be infinite - usually, an infinite sequence.
On the other hand, you can have this: a sequence of binary functions $f_i$ for $i = 0,1,2,\ldots$ so that each $f_i$ is computable, but the sequence $p_i = \prod_{n=1}^{\infty}f_i(n)$ is not. For a natural example, let $f_i(n) = 0$ if the $i$th Turing machine halts before stage $n$ and $1$ otherwise. Then $p_i$ is $0$ if the $i$th Turing machine halts or $1$ if it doesn't; that makes computing the $p_i$ equivalent to computing the Halting Problem.
