Formalist understanding of metalogical proofs

Question

How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.

Answer 1

Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $\Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $\text{ZFC} \vdash \Phi$.

This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.

Method B. Through conservation results. There is a system $\text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $\text{WKL}_0$ of second-order arithmetic with the following properties:

1. $\text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).

2. There is a finitistic proof that any $\Pi^0_2$ sentence of arithmetic that is provable in $\text{WKL}_0$ is provable in the finitistic system $\text{PRA}$. This kind of metatheorem is known as a `conservation result'.

So a formalist can work in $\text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $\Pi^0_2$ sentence that she proves is already finitistically provable. Because statements viewed as meaningful in finitism are going to be at worst $\Pi^0_2$, this means that any meaningful statement she proves from $\text{WKL}_0$ can be proved finitistically, and hence can be "accepted".

This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $\text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $\Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.