Doesn't the Gödel theorem say that such proof cannot be found for all conceivable systems; but that for any particular system, a proof could in principle be found?
I think it's something like this: you can't prove the consistency of a formal system using that same formal system, unless it is in fact inconsistent, but you can model a formal system from inside a larger formal system and then prove things like consistency about the smaller system from inside the larger one. But then the consistency of the larger system is unproven and you're stuck with an endless regress into ever larger FS's as you pursue the chimera.
Weirdly enough, as Gentzen showed, you can use a theory that is "sideways" to first-order logic, neither strictly more powerful nor weaker nor equivalent in power, to demonstrate the consistency of first-order logic. Strong normalization theorems are used for typed lambda calculi like the Calculus of Inductive Constructions to show consistency, as well.
