Formal logic systems, how do we prove theorems about them? One of the reasons for the existence of formal logic systems is to establish the foundations of mathematics. To have all theories constructed and proven using particular syntactic rules based on a proof theory.
If so, how do we prove that a formal logic system satisfies a certain property, Soundness for example?
We can't use the rules of deduction defined in our formal logic system on itself (we haven't established its validity yet), so we have to write a proof in "human" language before we can use the system.
How can this make sense? Foundations of mathematics now rely on "human" informal language proofs at its base.
 A: Informal language is (informally) considered as a "shortcut" that can be, in principle, translated to formal logic. So, in theory, we're never relying on human language, though in practice, one rarely actually writes a formal proof (though there are large-scale project for doing exactly this using the help of computers).
In the beginning of the 20th century, some people though that it is important to lay mathematics on a formal foundation; other people disagreed. From the point of view of the acting mathematician, foundations are only needed if they're your specialty. Occasionally they come into play, and they definitely cannot be ignored - math has turned into such a game - but they're normally left in the shadow.
At any rate, the dream was shattered by Gödel, who proved that a non-trivial (in some exact sense) proof system cannot prove its own consistency, let alone the consistency of a stronger system. So for all we know, math is inconsistent as usually thought of. Will that be so bad? Not really. Perhaps some "foundations" stuff will have to be revised, but $\sin^2\alpha + \cos^2\alpha = 1$ will stay true nonetheless.
When people do prove theorems about proof systems, they always "work" in a stronger proof system, which can be taken formally as some subset of ZFC in most cases (but we shouldn't really care most of the time). This is why we can only prove unconditional results about weak proof systems. Stronger results are relative, for example all forcing arguments.
Finally, a last plea from me to you: please don't take this formal stuff too seriously. While entertaining and fruitful, it is only one way to look at math. Save the thought and reconsider in a few years. (As an aside, I'm a logic and set theory fan myself.)
