I don't really know much about formal logic. But there is a kind-of-philosophical question that has always been bothering me. It seems to me that, in the context of mathematical logic, we are permitted to use mathematics and "common" logic to reason about logical systems we study. I want to know if my understanding is correct. More precisely, I want to know the answers to the following (very vague) questions.

Consider a statement A about a deduction system $\mathcal{D}$. For instance, A is the statement that a certain formula is formally provable from $\mathcal{D}$.

(1) Is it true that this statement A and a proof of it are on the meta-mathematical level?

(2) What are the rules that we are permitted to use to prove statement A? I will illustrate this by an example: in proving Goedel's Completeness Theorem, mathematical induction (a mathematical construct, supposedly having some mathematical content, at least meta-mathematically) and proof-by-contradiction (a logical construct) are apparently being used. Base upon this example, let me rephrase question (2) in the following smaller parts:

(2.a) Is there an agreement among practitioners of mathematical logic on the kinds of ordinary mathematics that are allowed?

(2.b) Consider a certain piece of mathematics, denoted by $\mathcal{M}$, together with the collection $\mathfrak{F}(\mathcal{M})$ of formalizations\axiomatizations of $\mathcal{M}$. Is it a sensible question to ask about the dependencies of the deduction system $\mathcal{D}$ upon each $\mathcal{F}\in\mathfrak{F}(\mathcal{M})$ based on the results about $\mathcal{D}$ that are deducible from $\mathcal{M}$? Here, the word "deducible" should be taken to mean "meta-mathematically deducible" if the answer to (1) is yes. More specifically, can we make sense of the following diagram or perhaps the reversed arrow?

$\{\text{dependencies of }\mathcal{D}\text{ on }\mathcal{F}\in\mathfrak{F}(\mathcal{M})\}\longrightarrow\{\text{results }A\text{ about }\mathcal{D}\text{ deducible from }\mathcal{M}\}$.

If we can, what kind of structures do these things have? This is the place in my question where I think category theory or homotopy theory might be relevant.

(2.c) As for the logical constructs, it seems we are allowed to use usual, everyday logic. But if we were to prove something about a formal logical system that is somewhat intuitionistic where proof-by-contradiction is not formally available, it would lead to a philosophical problem of using a meta-mathematical reasoning framework (everyday human logic, so to speak) where proof-by-contradiction is allowed to deduce results about a formal system where proof-by-contradiction is not allowed.

I would really appreciate it if you could also give me some references.