Soundness and Completeness of Gentzen Proof System

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


Sources