It is completely standard to study formalized metatheories. Historically, this is particularly of interest from the point of view of mathematical finitism - most proof systems for first-order logic are completely finitistic, based only on symbol manipulation, and so their formalization is somewhat straightforward.
Formalization of the metatheory is also of interest to help us see the mathematical techniques required to prove theorems of logic such as the completeness theorem.
Rather than making a formal metatheory that quantifies directly over strings, as suggested in the question, it has been more common to work with Primitive Recursive Arithmetic, whose basic objects are natural numbers. There is a tight link between formulas and natural numbers, as I explained in this answer. PRA is often studied as a quantifier-free theory, with a large collection of function-building symbols; it is typically considered to be "the" formal standard for a finitistic theory.
We know for example, that a formalized version of the incompleteness theorem is provable in PRA.
PRA cannot talk about infinite sets, and so cannot talk about infinite models. To look at logical theorems such as the completeness theorem, we need to move to slightly stronger theories. We could use ZFC set theory, but that is far more than we need to study the countable logical theories that arise in practice. It has been common to use theories of second-order arithmetic, which can talk about both natural numbers and sets of natural numbers, to study the completeness theorem. We know that, in this context, the completeness theorem for countable theories is equivalent to a theory of second-order arithmetic known as $\mathsf{WKL}_0$, relative to a weaker base theory.
The way to get into this subject is to first learn quite a bit of proof theory, after you have a strong background in basic mathematical logic. There are not any resources I am aware of that are readable without quite a bit of background. Even introductory proof theory texts often assume quite a bit of mathematical maturity and exposure to mathematical logic, and are written at a graduate level. So there is no royal road to the area, unfortunately, although much beautiful work has been done.
To get a small sense of what exists, you can read about the formalization of the incompleteness theorem in Smorynski's article in the Handbook of Mathematical Logic. That article only describes one part of a much larger body of work, however. The overall body of work on formalized metatheories is spread out in many places, and described from many points of view. You can find some of these in the Handbook of Proof Theory, and in the following texts:
- Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic, Springer, 1998
- Stephen G. Simpson, Subsystems of Second-Order Arithmetic, Springer, 1999
- Ulrich Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer, 2008
All of these are intended for graduate or postgraduate mathematicians.
Yes, it is clearly possible - as in the comments, for example $A$ might prove $\lnot \text{Con}(\text{ZFC})$ and $B$ might prove $\text{Con}(\text{ZFC})$.
But, in some sense, this is only kind of example. Assume that $A$ and $B$ are consistent theories each of which is strong enough to work with the same formalized provability predicate $\text{Pr}_C$ for some effective theory $C$, so $\text{Pr}_C$ is the same in the language of $A$ and the language of $B$.
Also assume that $A \vdash \text{Pr}_C(\phi)$ and $B \vdash \lnot \text{Pr}_C(\phi)$ for some sentence $\phi$ in the language of $C$.
Then $A \cup B \vdash \text{Pr}_C(\phi) \land \lnot \text{Pr}_C(\phi)$, so
$A\cup B$ is inconsistent. This means that there is a finite subset $A'$ of $A$ and a finite subset $B'$ of $B$ so that $A' \cup B'$ is inconsistent, so $A' \vdash \lnot \bigwedge B'$. Hence, if the situation above happens, there are particular axioms of $A$ that are incompatible with particular axioms of $B$.
This means, in particular, that the situation will never happen with the usual hierarchy of foundational theories, because these are all compatible with each other.
Now, continue with the assumptions in the second paragraph. Because $\psi \equiv \text{Pr}_C(\phi)$ is a $\Sigma^0_1$ statement, then if it is true then it is true in every model of arithmetic, even nonstandard models. This means that, if $\psi$ is true then the only way for $B \vdash \lnot \psi$ to happen is for $B$ to be inconsistent. We assumed otherwise, so $\psi$ is false. This means that, for the situation in the second paragraph to happen, $\phi$ is not provable in $C$. Thus $\psi$ is false in every $\omega$-model of arithmetic, and so $A$ has no $\omega$-models.
That is exactly the kind of situation we get from the example in the first paragraph, where $\text{Con}(\text{ZFC})$ holds in every $\omega$-model and a theory that proves $\lnot \text{Con}(\text{ZFC})$ has no $\omega$-models.
Best Answer
If this is referring to A Course in Mathematical Logic by John Bell and Moshé Machover (round about p.8), then you are perhaps making heavy weather of a fairly simple point.
Suppose, for example, we are interested in the propositional calculus. It evidently doesn't matter exactly what style of arrow we use in the object language as its conditional (or whether we use a horseshoe rather than an arrow), etc. That's agreed on all sides. The question is how should we handle the point when dealing with propositional logic?
One option is to start with a fixed object language, do the meta-theory for the logic of arguments as presented in this fixed object language, then say at the end "and obviously, the same applies to any variant object-language which shares such-and-such features."
Or we can take Bell and Machover's neater(?) line and build in generality from the start. So we allow for lots of variations in our object languages. And when talking about propositional arguments in one language or another we augment our English metalanguage with a symbol '$\to$' (for example) to denote the conditional symbol in the object language. But we go on to say with Bell and Machover that "What the latter symbol actually looks like is of no importance, and the reader may give free range to his imagination." If you like, this is to give a rather more abstract characterization of the object language.
This second approach is very common. At some point we need to get into the story the fact that shape of symbols (choice of fonts, italics vs bold, etc) are irrelevant to logic. To repeat: roughly speaking, we either take a fixed object language, do the meta-theory for that, then generalize -- or we do what Bell and Machover do, which is to take the meta-theory to be general from the start.
You pays your money and you makes your choice.