Definition:Alpha-Formula
Definition
Let $\mathbf A$ be a WFF of propositional logic that is not a literal.
Then $\mathbf A$ is an $\alpha$-formula if and only if 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$.
Table of $\alpha$-Formulas
From Classification of $\alpha$-Formulas, we obtain the following table of $\alpha$-formulas $\mathbf A$ and corresponding $\mathbf A_1$ and $\mathbf A_2$:
$\qquad \begin{array}{ccc} \hline \mathbf A & \mathbf A_1 & \mathbf A_2 \\ \hline \neg \neg \mathbf A_1 & \mathbf A_1 & \\ \mathbf A_1 \land \mathbf A_2 & \mathbf A_1 & \mathbf A_2 \\ \neg \paren {\mathbf A_1 \lor \mathbf A_2} & \neg \mathbf A_1 & \neg \mathbf A_2 \\ \neg \paren {\mathbf A_1 \implies \mathbf A_2} & \mathbf A_1 & \neg \mathbf A_2 \\ \neg \paren {\mathbf A_1 \mathbin \uparrow \mathbf A_2} & \mathbf A_1 & \mathbf A_2 \\ \mathbf A_1 \mathbin \downarrow \mathbf A_2 & \neg \mathbf A_1 & \neg \mathbf A_2 \\ \mathbf A_1 \iff \mathbf A_2 & \mathbf A_1 \implies \mathbf A_2 & \mathbf A_2 \implies \mathbf A_1 \\ \neg \paren {\mathbf A_1 \oplus \mathbf A_2} & \mathbf A_1 \implies \mathbf A_2 & \mathbf A_2 \implies \mathbf A_1 \\ \hline \end{array}$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.2$