Provable by Gentzen Proof System iff Negation has Closed Tableau/Formula
Jump to navigation
Jump to search
Theorem
Let $\mathscr G$ be instance $1$ of a Gentzen proof system.
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$.
Proof
This is a specific instance of Provable by Gentzen Proof System iff Negation has Closed Tableau: Set of Formulas.
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.2.1$: Theorem $3.6$