Right, but the point here is that we're not just talking about extensions of the system, we're talking about true but unprovable statements—that is, statements

Right, but the point here is that we're not just talking about extensions of the system, we're talking about true but unprovable statements—that is, statements that are true in the standard model of arithmetic but not provable in PA (or whatever other arithmetic theory strikes your fancy). This is why Turing looked not at single formal theories but at a hierarchy of consistency extensions of the initial theory. In other words, the game changes from formal provability to informal provability, and from provability relative to a set of axioms to absolute provability. Turing showed (very roughly) that given a tree of consistency extensions (which branches only at limit stages) every Pi_1 sentence was decided at some point a with |a| = ω + 1. Feferman then proved in the 1960s that there is a path through the tree of ordinal notations that decides every Pi_2 sentence. These are completeness results, albeit for progressions of formal systems rather than individual systems. So certainly the puzzle can never be completed within a single formal system, but by restricting to sentences of limited complexity, there is an ordinal-time operation which decides each sentence (obviously there are numerous philosophical problems with this, although I'm afraid my expertise in this area is extremely limited so I can only give a sketch of the issues involved).