\begin{definition}[Definition:Propositional Tableau/Construction]
A propositional tableau with root node $\mathbf H$ can be constructed as follows:
# Start with a rooted tree $T_0$ which consists of a single node, which is the root node, and the hypothesis set $\mathbf H$ at the root.
# Extend the tableau $T_0$ to a tableau $T_1$, and $T_1$ to a tableau $T_2$ and so on, using one of the tableau extension rules.
# At each stage a leaf node $t$ of $T_n$ is chosen, and a WFF $\mathbf C$ which appears on the branch through $t$.
# Build $T_{n+1}$ by adding one, two or four nodes below $t$ according to which rule is determined by the form of $\mathbf C$.
At each stage of the process, we have a finite propositional tableau $T_k$.
If the process continues through all $k \in \N$, the union of the chain of finite tableaus will be an infinite propositional tableau $T$.
\end{definition}