\begin{definition}[Definition:Labeled Tree for Propositional Logic]
A '''labeled tree for propositional logic''' is a system containing:
* A rooted tree $T$;
* A countable set $\mathbf H$ of WFFs of propositional logic;
* A WFF $\Phi \left({t}\right)$ attached to each non-root node $t$ of $T$.
Such a structure can be denoted $\left({T, \mathbf H, \Phi}\right)$.
\end{definition}