Completeness Theorem of Propositional Calculus

Theorem

If a logical formula is a tautology, then it has a tableau proof.

That is:

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

Proof

This is a corollary of the Extended Completeness Theorem of Propositional Calculus:

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

Let $\mathbf A$ be a logical formula.

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

In this case, we have $\mathbf H = \varnothing$.

Hence the result.

$\blacksquare$

Also see

The Soundness Theorem of Propositional Calculus in which is proved:

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

Sources

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