> each concrete solution can be expressed in finite length in a formal language with a finite alphabet
Suppose that's the case, the problem is that the resulting language of all the finite proofs can still be infinite and we again cannot enumerate and check all the solutions (since the final set is infinite). Therefore we're short of a method to decide yes/no for each question.
This appears to be exactly the case in the example provided by @ykonstant
> Consider the sequence of yes/no problems P_K = {Is there a solution to Q=0 in [-K,K]^n?} parametrized by a positive integer K.
For each yes/no question, the workload is finite, but for the union of all yes/no questions, the workload is not finite.