Soundness and Completeness of Semantic Tableaus

From ProofWiki
Jump to: navigation, search

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$


Sources