Extended Completeness Theorem of Propositional Calculus

Theorem

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

Let $\mathbf A$ be a logical formula.

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

Proof

Suppose $\mathbf A$ is a semantic consequence of $\mathbf H$.

Then $\mathbf H \cup \left\{{\neg \mathbf A}\right\}$ has no models.

By the Finite Main Lemma, this set has a tableau confutation, which is a tableau proof of $\mathbf A$ from $\mathbf H$.

$\blacksquare$

Also see

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

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

Sources

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