Definition:Finished Branch of Propositional Tableau

Definition

Let $T$ be a propositional tableau.

Let $\Gamma$ be a branch of $T$.

Then $\Gamma$ is finished if and only if:

$(1): \quad \Gamma$ is not contradictory

$(2): \quad$ Every non-basic WFF on $\Gamma$ is used at some node of $\Gamma$.

That is, $\Gamma$ is finished if and only if the set $\Delta$ of WFFs of propositional logic which occur along $\Gamma$ is a finished set‎.

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.10$: Completeness: Lemma $1.10.1$