Sound Proof System is Consistent

From ProofWiki
Jump to navigation Jump to search


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.


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.