Soundness and Completeness of Semantic Tableaus

From ProofWiki
Jump to navigation Jump to search


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.


The two directions of this theorem are respectively addressed on:

Soundness Theorem for Semantic Tableaus
Completeness Theorem for Semantic Tableaus