This is in fact an infinite collection of theorems, one for each formula $\phi(x)$. Gödel's theorem prevents ZFC from proving all of these instances all at the same time. The proof of this metatheorem is by induction on the length of $\phi(x)$. The requirements on the metatheory are very minimal, all you need is enough combinatorics to talk about formulas, proofs, and enough induction to make sense of it all. This is by far the most common flavor of "meta" in logic. There really is not much to it. Most logicians don't worry about the metatheory in this context. Indeed, like most mathematicians, logicians usually believe in the natural numbers with full induction.

However, sometimes there is need for a much stronger metatheory. The metatheory of Model Theory is usually taken to be ZFC. Gödel's Completeness Theorem is a nice contrasting example.

Recall that a theory is consistent if one cannot derive a contradiction form it, while a theory is satisfiable if it has a model. The consistency of a theory is a purely syntactic notion. When the theory is effective, consistency can be expressed in simple arithmetical terms in a manner similar to the one discussed above. However, satisfiability is not at all of this form since the models of a theory are typically infinite structures. This is why this theorem is usually stated in ZFC. For the Completeness Theorem, one can often get by with substantially less. For example, the system WKL₀ of second-order arithmetic suffices to prove the Completeness Theorem for countable theories, but such a weak metatheory would be nothing more than a major inconvenience for model theorists.

• Forcing is a way to extend a countable transitive model of ZFC' to a larger model of ZFC' with different properties. Here ZFC' is a finite approximation to ZFC, which makes this statement non-vacuous because of the Reflection Principle above.

• Forcing is a way to talk about truth in an alternate universe of sets. Here, the alternate universe is often taken to be a Boolean-valued model, formalized within the original universe.

• Forcing is an effective way to transform a contradiction some type of extensions of ZFC into contradictions within ZFC itself. Here, ZFC could be replaced by an extension of ZFC.

Finally, the idea of analyzing which systems prove the consistency of other systems is very common in logic. In Set Theory, these systems often take the form of large cardinal axioms. In Second-Order Arithmetic these systems often take the form of comprehension principles. In First-Order Arithmetic these systems often take the form of induction principles. Together these form an incredibly long consistency strength hierarchy stretching from extremely weak basic arithmetical facts to incredibly deep large cardinal axioms. A significant part of logic deals with studying this hierarchy.

This is in fact an infinite collection of theorems, one for each formula $\phi(x)$. Gödel's theorem prevents ZFC from proving all of these instances at the same time. The proof of this metatheorem is by induction on the length of $\phi(x)$. The requirements on the metatheory are very minimal, all you need is enough combinatorics to talk about formulas, proofs, and enough induction to make sense of it all. This is by far the most common flavor of "meta" in logic. There really is not much to it. Most logicians don't worry about the metatheory in this context. Indeed, it is often irrelevant and, like most mathematicians, logicians usually believe in the natural numbers with full induction.

However, sometimes there is need for a much stronger metatheory. For example, the metatheory of Model Theory is usually taken to be ZFC. Gödel's Completeness Theorem is a nice contrasting example.

Recall that a theory is consistent if one cannot derive a contradiction form it, while a theory is satisfiable if it has a model. The consistency of a theory is a purely syntactic notion. When the theory is effective, consistency can be expressed in simple arithmetical terms in a manner similar to the one discussed above. However, satisfiability is not at all of this form since the models of a theory are typically infinite structures. This is why this theorem is usually stated in ZFC. For the Completeness Theorem, one can often get by with substantially less. For example, the system WKL₀ of second-order arithmetic suffices to prove the Completeness Theorem for countable theories (that exist in the metaworld in question), but such a weak metatheory would be nothing more than a major inconvenience for model theorists.

• Forcing is a way to extend a countable transitive model of ZFC' to a larger model of ZFC' with different properties. Here ZFC' is a finite approximation to ZFC, which makes this statement non-vacuous in ZFC because of the Reflection Principle above.

• Forcing is a way to talk about truth in an alternate universe of sets. Here, the alternate universe is often taken to be a Boolean-valued model, formalized within the original universe.

• Forcing is an effective way to transform a contradiction some type of extensions of ZFC into contradictions within ZFC itself. Here, ZFC could be replaced by an extension of ZFC.

Finally, the idea of analyzing which systems prove the consistency of other systems is very common in logic. In Set Theory, these systems often take the form of large cardinal axioms. In Second-Order Arithmetic these systems often take the form of comprehension principles. In First-Order Arithmetic these systems often take the form of induction principles. Together these form an incredibly long consistency strength hierarchy stretching from extremely weak basic arithmetical facts to incredibly deep large cardinal axioms. A very significant part of logic deals with studying this hierarchy and, as Andrej Bauer commented, logicians are usually very aware of where they are sitting in this hierarchy when proving metatheorems.