Finished Propositional Tableau has Finished Branch or is Confutation
Jump to navigation
Jump to search
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$