# Soundness and Completeness of Semantic Tableaus/Corollary 2

Jump to navigation
Jump to search

## Corollary to Soundness and Completeness of Semantic Tableaus

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

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

## Proof

By Tautology iff Negation is Unsatisfiable, $\mathbf A$ is a tautology if and only if $\neg \mathbf A$ is unsatisfiable.

By the Soundness and Completeness of Semantic Tableaus, this amounts to the existence of a closed tableau for $\neg \mathbf A$.

$\blacksquare$

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 2.7$: Corollary $2.69$