Provable by Gentzen Proof System iff Negation has Closed Tableau
Let $\mathscr G$ be instance 1 of a Gentzen proof system.
Let $\mathbf A$ be a WFF of propositional logic.
- $\neg \mathbf A$ has a closed semantic tableau
where $\neg \mathbf A$ is the negation of $\mathbf A$.
- $\bar U$ has a closed semantic tableau