Consider the statement: "ZFC is consistent". Normally this is considered at first sight as a statement in the metatheory. But if we follow Kunen's (informally) description of what the metatheory is (i.e., finitistic reasoning), there seem to be some problems to place that statement precisely at the metatheoretical level.

First of all, since ZFC is not finitely axiomatizable, it seems the metatheory fails to absorb the theory ZFC as a whole, and instead we should first develop some finitely axiomatizable fragment of set theory within which we can correctly formulate the theory ZFC.

But suppose we work with a finitely axiomatizable theory T. Does it make sense now to ask in the metatheory whether T is consistent? At first sight, the consistency of a theory as a concept supposes we can quantify over all possible formal proofs within the theory and assert that none of them actually ends in contradiction. But isn't this a set-theoretical analysis? Shouldn't we first develop some set theory and only then define set-theoretically the concept of consistency?

Of course if T happens to have a finite model, we are inclined to assert, in the metatheory, that we can never find a proof of a contradiction. But instead of saying that T is consistent, shouldn't we just say that T has a finite model? Or is the conclusion of consistency from this a valid finitistic reasoning that should be part of the metatheory?

Finally, what if T does not have a finite model? It seems to me that some intuitionistic approach should be taken in the metatheory, in the sense that concepts such as inconsistency are meaningless unless we can actually find a specific proof of a contradiction.