[mietek]

Indeed, the objection is against the method by which this system is supposed to be defined. As you say, we start with an implicit assumption that we don’t have an effective procedure to construct the set of statements that are true in the ambient metatheory. And so, this set exists in a classical sense, or “weakly exists”, and not in a constructive sense.