Soundness and Completeness of Gentzen Proof System

Theorem

Let $\mathscr G$ be instance 1 of a Gentzen proof system.

Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.

Then $\mathscr G$ is a sound and complete proof system for $\mathrm{BI}$.

Proof

This is an immediate consequence of:

• Provable by Gentzen Proof System iff Negation has Closed Tableau
• Soundness and Completeness of Semantic Tableaus

$\blacksquare$

Sources

• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.2.1$: Theorem $3.8$