Semantic Tableau Algorithm is Decision Procedure for Tautologies

Theorem

The Semantic Tableau Algorithm is a decision procedure for tautologies.

Proof

Let $\mathbf A$ be a WFF of propositional logic.

The Semantic Tableau Algorithm applied to $\neg \mathbf A$ yields a completed tableau for $\neg \mathbf A$.

By Soundness and Completeness of Semantic Tableaus: Corollary $2$, this completed tableau decides if $\mathbf A$ is a tautology.

$\blacksquare$

Sources

• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.7$: Corollary $2.70$