\begin{definition}[Definition:Alpha-Formula]
Let $\mathbf A$ be a WFF of propositional logic that is not a literal.
Then $\mathbf A$ is an '''$\alpha$-formula''' {{iff}} either:
:$\mathbf A = \neg \neg \mathbf A_1$
for some WFF $\mathbf A_1$, or:
:$\mathbf A$ is semantically equivalent to a conjunction $\mathbf A_1 \land \mathbf A_2$
for some WFFs $\mathbf A_1, \mathbf A_2$.
\end{definition}