Soundness and Completeness of Semantic Tableaus/Corollary 2

From ProofWiki
Jump to: navigation, search

Corollary to Soundness and Completeness of Semantic Tableaus

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


Then $\mathbf A$ is a tautology iff $\neg \mathbf A$ has a closed tableau.


Proof

By Tautology iff Negation is Unsatisfiable, $\mathbf A$ is a tautology iff $\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