I got off on the wrong foot with my proof attempt yesterday by stupidly thinking I could dodge diagonalization by computable approximation; I guess the thing I had read somewhere was the (not computably realizable) fact that if you keep taking the smallest theory (i.e. Turing machine) consistent with the data so far, and which terminates on all inputs so far (that being the noncomputable part), you'll eventually be always right. Here's another thought, though: choose up front a sound proof system P that has a terminating proof-checking procedure. On the nth step, start enumerating P-provably terminating Turing machines and running them on inputs 0..n-1. As soon as you get a g that is consistent with f(0)..f(n-1), guess g(n) as your prediction of f(n). As long as f is P-provably terminating, you'll eventually always make guesses consistent with it. The moral of diagonalizing here is that the guessing procedure itself can't possibly be P-provably terminating, right?