Let f(k) be a recursive function which maps the set of positive integers into itself. Let T be a formalized theory which is axiomatizable and contains Peano's Arithmetic as a subtheory. For example, T could be ZFC or Second order Arithmetic. Could there be a kind of "Incompleteness theorem" that states the following? "If T is consistent, then there always exists a total recursive f(k) such that it cannot be proved in T whether 1/f(1) + 1/f(2) +  + 1/f(k) +  is convergent or divergent".  I was motivated to ask this because of the increasingly complicated test used to determine whether a series of positive real numbers is convergent or divergent. There seems to be some sort of partial ordering among these tests, so that if a test does not work for some particular series, a more complicated testfurther along in the partial orderingmay work.  Note that a recursive series of positive rational numbers (which are not necessarily the reciprocals of integers) can also be accommodated in this framework. Each term of such a series may be expressed as a finite sum of socalled "Egyptian fractions" since these always have a numerator equal to 1.
Let $\phi(n)$ be any bounded formula in the language of arithmetic. The sequence of rational numbers $$a_m = \begin{cases} 1/m & \text{if $\exists n \lt m\,\phi(n)$} \\ 1/2^m & \text{if $\forall n \lt m\,\lnot\phi(n)$} \end{cases}$$ is total computable and "$\sum_m a_m$ diverges" is logically equivalent to $\exists n \phi(n)$ over a PA. Taking $\phi(n)$ such that $\exists n \phi(n)$ is the Rosser sentence of a theory $T$ extending PA, we obtain a provably total sequence of rational numbers $a_m$ such that, if $T$ is consistent, then $T$ neither proves nor refutes that $\sum_m a_m$ is convergent.

$\begingroup$ Very nice. I thought that something like this could be done but was not able to figure it out for myself. $\endgroup$ – Garabed Gulbenkian Feb 6 '16 at 21:37