Soundness and Completeness of Semantic Tableaus

Theorem

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

Let $T$ be a completed semantic tableau for $\mathbf A$.

Then $\mathbf A$ is unsatisfiable iff $T$ is closed.

Corollary 1

$\mathbf A$ is satisfiable if and only if $T$ is open.

Corollary 2

$\mathbf A$ is a tautology if and only if $\neg \mathbf A$ has a closed tableau.

Proof

The two directions of this theorem are respectively addressed on:

Soundness Theorem for Semantic Tableaus
Completeness Theorem for Semantic Tableaus

$\blacksquare$