Extended Soundness Theorem of Propositional Calculus

Theorem

Let $\mathbf H$ be a countable set of logical formulas.

Let $\mathbf A$ be a logical formula.

If $\mathbf H \vdash \mathbf A$, then $\mathbf H \models \mathbf A$.

Proof

We are given $\mathbf H$ and $\mathbf A$.

If $\mathbf H \vdash \mathbf A$, then there exists a tableau proof for it.

Thus we have a tableau confutation of $\mathbf H \cup \left\{{\neg \mathbf A}\right\}$.

So, by Tableau Confutation means No Model‎, $\mathbf H \cup \left\{{\neg \mathbf A}\right\}$ has no model.

That is, no model of $\mathbf H$ is also a model of $\neg \mathbf A$.

So if $\mathcal M$ is a model of $\mathbf H$, $\mathcal M$ is also a model of $\mathbf A$.

Thus, by definition of logical consequence, $\mathbf H \models \mathbf A$.

$\blacksquare$

Also see

The Extended Completeness Theorem of Propositional Calculus in which is proved:

If $\mathbf H \models \mathbf A$, then $\mathbf H \vdash \mathbf A$.

Sources

• H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability (1996): $\S 1.8$: Theorem $1.8.3$