Extended Soundness Theorem for Propositional Tableaus and Boolean Interpretations

Theorem

That is, for every collection $\mathbf H$ of WFFs of propositional logic and every WFF $\mathbf A$:

$\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ implies $\mathbf H \models_{\mathrm{BI}} \mathbf A$

By definition of tableau proof, $\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ means:

There exists a tableau confutation of $\mathbf H \cup \set {\neg\mathbf A}$.

Therefore, if some boolean interpretation $v$ models $\mathbf H$:

$v \models_{\mathrm{BI}} \mathbf H$

then since $\mathbf H \cup \set {\neg\mathbf A}$ is unsatisfiable:

$v \not\models_{\mathrm{BI}} \neg\mathbf H$

Now by definition of the relation $\models_{\mathrm{BI}}$, it must be that:

$\map v {\neg \mathbf A} = F$

$\map v {\mathbf A} = T$

which is to say $v \models_{\mathrm{BI}} \mathbf A$.

Hence:

$v \models_{\mathrm{BI}} \mathbf H$ implies $v \models_{\mathrm{BI}} \mathbf A$

that is, $\mathbf A$ is a $\mathrm{BI}$-semantic consequence of $\mathbf H$:

$\mathbf H \models_{\mathrm{BI}} \mathbf A$

which was to be shown.

$\blacksquare$