Tableau Rule Agreement Lemma

theorempropositional-logic

Intuition

Formal Statement

Let $\sigma$ be a labeled node on a finite tableau $P$. Let $P^{\prime }$ be tableau formed by decomposing $\sigma$ on $P$. For any valuation $V$: $V$ agrees with the signed formula labelling $\sigma$ if and only if $V$ agrees with all of the signed formulas in $P^{\prime }$ on at least one of the branches below $\lambda$.

Corollaries