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.
Translating constant symbols to variables does not work well, because in most logics where you contemplate formulas with free variables, the intended semantics is that of their universal closure. In those systems you have, for example
$$ p(x) \vDash p(y) \qquad\text{but not}\qquad p(c_0) \vDash p(c_1) $$
because the models that satisfy $p(x)$ are exactly those where $p$ holds for every individual, which are the same models that satisfy $p(y)$.
You can, however, simulate constants using new function and predicate symbols. Construct a new language by adding a fresh variable letter $0$, a single new unary predicate symbol $Z$, and countably many new symbol functions $f_n$, and then translate
- each constant $c_n$ as $f_n(0)$;
- all other parts of terms remain unchanged;
- each atomic formula $p(t_1, \ldots, t_n)$ as
$$ \neg \exists 0\Bigl (Z(0) \land \forall x(Z(x)\to x=0) \land \neg p(t[t_1],\ldots,t[t_n]\Bigr); $$
- and all connectives and quantifiers remain themselves
I hope this qualifies for your concept of a translation $\mathcal L_1\to\mathcal L_2$. If you want to be completely rigid about it, you could "make room" for the new $\{0,Z,f_n\}$ symbols by selecting existing symbols for them and shifting the existing symbols out of the way with the Hilbert's-hotel map as part of the translation, but I'm not going to complicate my notation by making that explicit.
Suppose that for some $\Gamma$, $\varphi$ we have that $t(\Gamma) \vDash_2 t(\varphi)$ and for some model $\mathfrak M$ we have $\mathfrak M\vDash_1 \Gamma$. Then we can construct a new $\mathfrak M_2$ by selecting a single of $\mathfrak M$'s elements to have the $Z$ property, and letting $(f_n)^{\mathfrak M_2}$ map everything to $(c_n)^{\mathfrak M}$ for each $n$.
Then $\mathfrak M_2\vDash_2 t(\psi)$ exactly if $\mathfrak M\vDash_1 \psi$. Now since $\mathfrak M\vDash_1 \Gamma$ we have $\mathfrak M_2\vDash_2 t(\Gamma)$ and then by assumption $\mathfrak M_2 \vDash_2 t(\varphi)$ and then $\mathfrak M\vDash_1 \varphi$.
Conversely, suppose $\Gamma \vDash_1 \varphi$ and we have some $\mathfrak M \vDash_2 t(\Gamma)$. Then,
- either there is a unique $m_0\in\mathfrak M$ that satisfies $Z(m_0)$, and in that case we can construct an $\mathfrak M_1$ by the reverse of the above procedure -- namely, let $(c_n)^{\mathfrak M_1}$ be $f^{\mathfrak M}(m_0)$ -- such that $\mathfrak M_1\vDash_1 \psi$ iff $\mathfrak M\vDash_2 t(\psi)$.
- or there is no such element, in which case the translation of every atomic formula is true in $\mathfrak M$ for all values of the variables. In that case let $\mathfrak M_0$ be the model with a single element where all predicates are true; then $\mathfrak M_0\vDash_1 \psi$ iff $\mathfrak M\vDash_2 t(\psi)$.
(The negations in the translation of atomic formulas are there to allow $\mathfrak M_0$ to work when $p$ is the equality predicate $=$, which we're not allowed to make "always false" when constructing a model -- but we can make it "always true" by selecting a model with a single element).
Best Answer
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.