Formalist understanding of metalogical proofs 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.
 A: 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:


*

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

*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. 
