Finished Propositional Tableau has Finished Branch or is Confutation

Theorem

Let $\struct {T, \mathbf H, \Phi}$ be a finished propositional tableau.

Then one of the following holds:

$T$ has a finished branch

$T$ is a tableau confutation.

Proof

Suppose $T$ has no finished branch.

Then since $T$ is finished, every branch of $T$ is contradictory.

Hence $T$ is a tableau confutation.

$\blacksquare$

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.10$: Completeness
• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.11$: Compactness: Corollary $1.11.4$