Provable by Gentzen Proof System iff Negation has Closed Tableau

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

$\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 iff:

$\bar U$ has a closed semantic tableau

where $\bar U$ is the set comprising the logical complements of all WFFs in $U$.