Soundness and Completeness of Semantic Tableaus/Corollary 1
Jump to navigation
Jump to search
Corollary to Soundness and Completeness of Semantic Tableaus
Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed semantic tableau for $\mathbf A$.
Then $\mathbf A$ is satisfiable if and only if $T$ is open.
Proof
$\mathbf A$ is satisfiable if and only if it is not unsatisfiable.
By the Soundness and Completeness of Semantic Tableaus, $\mathbf A$ is satisfiable if and only if $T$ is not closed.
Since $T$ is completed, this is the case if and only if $T$ is open.
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.7$: Corollary $2.68$