lo.logic - What assumptions and methodology do metaproofs of logic theorems use and employ?

Here is some more information for the first question. I think that to prove the meta theorems in mathematics, in particular, soundness, completeness, incompleteness, heuristic logic does not exhaust the meta principles being used. Some meta principles relating to heuristic set theory or heuristic category theory must to be used as well. That is because when we talk about a model and a statements true in a model we need to have some notion of set or something equivalent.

It is difficult to understand these meta principles, so we need to cast them into the language of formal logic, formal set theory. I choose Zermelo Fraenkel set theory here. The formal counter part of your question can be considered the question which axioms of set theory necessary for the proof of the formalized version of the theorems. The choice of Zermerlo Fraenkel set theory is in a sense general enough. You might decide that category theory is the genuine language of mathematics but to phrase and prove soundness, completeness, you need to use something of equal strength. The expression may change with different choices of mathematical language, but the mathematical phenomenon remains invariant.

The following is not a very precise answer ( I did not checked the material carefully). I think this might be an approximation to the answer that you want:

Soundness for First Order Logic: We need classical logic, ZF {Powerset,Replacement, Infinity}. The checking of Soundness is basically mechanical so we don't need much.

Completeness for First Order Logic: Need all these thing and some weak version of choice, may be Konig lemma. The proof of completness is basically cook up a model of the theory base on the language. We need to add in many constant to make the theory have Henkin property, and this is an iterated process, so we need choice somewhere. I don't think we need power set.

First incompleteness: We need axiom of foundation and axiom of power set in the universe of set and the identification of theory of natural number with theory of $omega$ with the respectively defined +, x, <. I don't think we need choice here.

Second incompleteness: We still need axiom of founation (PA still must be enumerated by $omega$ in this situation). I don't think we need power set anymore.

To have the precise answer, we can always look closely at the steps of the proof or search the existing material.