Provable by Gentzen Proof System iff Negation has Closed Tableau/Formula

From ProofWiki
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