Provable by Gentzen Proof System iff Negation has Closed Tableau
Jump to navigation
Jump to search
Theorem
Let $\mathscr G$ be instance $1$ of a Gentzen proof system.
Formula
Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is a $\mathscr G$-theorem if and only if:
- $\neg \mathbf A$ has a closed semantic tableau
where $\neg \mathbf A$ is the negation of $\mathbf A$.
Set of Formulas
Let $U$ be a set of WFFs of propositional logic.
Then:
- $U$ is a $\mathscr G$-theorem
- $\bar U$ has a closed semantic tableau
where $\bar U$ is the set comprising the logical complements of all WFFs in $U$.