No, not quite. Roughly speaking, he's asking about the computational complexity of solving problems (producing proofs of statements in first-order predicate lo

No, not quite. Roughly speaking, he's asking about the computational complexity of solving problems (producing proofs of statements in first-order predicate logic) with a given bound N on the size of the solution. This is computable becaue the number of solutions (i.e., proofs) of length <= N is finite, and one can in principle just enumerate them all and check. Goedel's question is how the running time of producing a solution of size <= N (or finding that there is no solution of size <= N) grows with N, with the thinking that if no proof of a reasonable size can be found, one might as well not bother looking anymore.