I know the soundness of a first order language is proved in natural language by natural language deduction rules. For example, to prove $\phi \implies \phi \lor \psi $ is correct, we construct the following deduction sequence in natural language:
- model m and assignment s satisfy $\phi$
- model m and assignment s satisfy $\phi$ or $\psi$ (a deduction rule in natural language)
- model m and assignment s satisfy $ \phi \lor \psi $
We use a natural language deduction rule that is similar to the FOL deduction rule being proved ( $\phi \implies \phi \lor \psi $) to derive from 1) to 2). But I did not see a proof for the natural language deduction rules themselves. I don't think the natural language deduction rules do not need some kind of proof, as you know, people had used the deduction rule: for all $x$, $P(x) \implies$ there exists $x$, $P(x)$, for thousands of years until it's proved wrong by modern logic.
Until Frege, it was common to assume that a phrase such as "all flying dragons are blue" implies the existence of a flying dragon. Remarkably, Lewis Carroll in one of his books on logic games uses the universal quantifier in this way (this was only a few decades before Frege). Notice, however, that most logic books start with a specific list of logical transformations and formalisations of metalanguage rules that are allowed. These certainly don't include Lewis Carroll's trick. The confidence we have in such systems is the result of extensive practice that did not result in contradictions; there is no absolute guarantee that this is so. So, the rules of deduction in the metatheory are assumed to be correct because we haven't run into trouble with them. This is of course connected to the famous quandry with Hilbert's program.