Sound Proof System is Consistent

Theorem

Let $\LL$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\LL$.

Let $\mathscr P$ be a proof system for $\LL$.

Suppose that $\mathscr P$ is sound for $\mathscr M$.

Then $\mathscr P$ is consistent.

Proof

By assumption, some logical formula $\phi$ is not an $\mathscr M$-tautology.

Since $\mathscr P$ is sound for $\mathscr M$, $\phi$ is also not a $\mathscr P$-theorem.

But then by definition $\mathscr P$ is consistent.

$\blacksquare$

Sources

• 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.4$: Conditions for an Axiom System: Theorem $1$