Completeness Theorem for Hilbert Proof System Instance 2 and Boolean Interpretations

 It has been suggested that this article or section be renamed. One may discuss this suggestion on the talk page.

Theorem

That is, for every WFF $\mathbf A$:

$\models_{\mathrm{BI}} \mathbf A$ implies $\vdash_{\mathscr H_2} \mathbf A$

Also see

The Soundness Theorem for Hilbert Proof System Instance 2 and Boolean Interpretations in which it is proved that:

If $\vdash \mathbf A$ then $\models \mathbf A$.