\begin{definition}[Definition:Finished Set of WFFs of Propositional Logic]
Let $\Delta$ be a set of WFFs of propositional logic.
Then $\Delta$ is '''finished''' {{iff}}:
* $\Delta$ is not contradictory
* For each WFF $\mathbf C \in \Delta$, either $\mathbf C$ is basic or one of the following is true:
** $\mathbf C$ has the form $\neg \neg \mathbf A$ where $\mathbf A \in \Delta$
** $\mathbf C$ has the form $\paren {\mathbf A \land \mathbf B}$ where both $\mathbf A \in \Delta$ and $\mathbf B \in \Delta$
** $\mathbf C$ has the form $\neg \paren {\mathbf A \land \mathbf B}$ where either $\neg \mathbf A \in \Delta$ or $\neg \mathbf B \in \Delta$
** $\mathbf C$ has the form $\paren {\mathbf A \lor \mathbf B}$ where either $\mathbf A \in \Delta$ or $\mathbf B \in \Delta$
** $\mathbf C$ has the form $\neg \paren {\mathbf A \lor \mathbf B}$ where both $\neg \mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
** $\mathbf C$ has the form $\paren {\mathbf A \implies \mathbf B}$ where either $\neg \mathbf A \in \Delta$ or $\mathbf B \in \Delta$
** $\mathbf C$ has the form $\neg \paren {\mathbf A \implies \mathbf B}$ where both $\mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
** $\mathbf C$ has the form $\paren {\mathbf A \iff \mathbf B}$ where either:
*** both $\mathbf A \in \Delta$ and $\mathbf B \in \Delta$, or:
*** both $\neg \mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$;
** $\mathbf C$ has the form $\neg \paren {\mathbf A \iff \mathbf B}$ where either:
*** both $\mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
** or:
*** both $\neg \mathbf A \in \Delta$ and $\mathbf B \in \Delta$.
\end{definition}