Soundness and Completeness of Gentzen Proof System

Jump to: navigation, search

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:

$\blacksquare$