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.



The property you're looking for is generally a consequence of the logic being sound. The soundness theorem for a proof system states that everything it can prove (from a given theory) is true in every interpretation of the logical language (that satisfies each of the theory's axioms).

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.

Note that in order to speak of models in general you need some set theory, but if you specialize the semantics of the theory to the trivial model, you can express everything without needing sets. In addition, the soundness proof of the logic can usually be condensed down to a proof of "everything that can be proved from the empty theory is true about the trivial model" which does not depend on any infinitary set theory.

(This is in particular the case for the usual proof systems for propositional and first-order logic).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.