# 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 iff $\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$