# Are there any consistency proofs for propositional or first-order logic?

Take for example the Hilbert-style axiomatizations of the propositional and first-order calculus. Since a crucial point when operating with a proof system is that no contradictions must be found in it, it seems to me reasonable to look for a consistency proof of those calculus. But I googled it and I could not find anything about it.

So, my question is:

Is there a consistency proof for propositional and first-order logic?

and if there is,

How is this proof carried out?

the reason I ask this is because, since the tools for any proof is an logical apparatus itself, a consistency proof of a logical system X seems to assume that X is already consistent! Or this proof is carried out using second-order logic such like Gentzen's consistency proof of PA?

I appreciate if you shed some light into these topics or indicate some reference on the subject.

Thanks!

In particular, once you know a logic to be sound, you know it cannot prove both $\varphi$ and $\neg\varphi$, except from an inconsistent theory.
In particular, if you're considering the empty theory over some logical language, you can take the model with one element, where every relation symbol is always true. Then for any $\varphi$ you can think of it will be easy to find out whether it is true in this trivial model -- and depending on whether it is or not, either $\neg\varphi$ or $\varphi$ will be unprovable in the logic, because you know it doesn't prove anything that is false in any model.