Definition:Beta-Formula
Definition
Let $\mathbf B$ be a WFF of propositional logic that is not a literal.
Then $\mathbf B$ is a $\beta$-formula if and only if:
- $\mathbf B$ is semantically equivalent to a disjunction $\mathbf B_1 \lor \mathbf B_2$
for some WFFs $\mathbf B_1, \mathbf B_2$.
Table of $\beta$-Formulas
From Classification of $\beta$-Formulas, we obtain the following table of $\beta$-formulas $\mathbf B$ and corresponding $\mathbf B_1$ and $\mathbf B_2$:
$\qquad \begin{array}{ccc} \hline \mathbf B & \mathbf B_1 & \mathbf B_2\\ \hline \neg \paren {\mathbf B_1 \land \mathbf B_2} & \neg \mathbf B_1 & \neg \mathbf B_2 \\ \mathbf B_1 \lor \mathbf B_2 & \mathbf B_1 & \mathbf B_2 \\ \mathbf B_1 \implies \mathbf B_2 & \neg \mathbf B_1 & \mathbf B_2 \\ \mathbf B_1 \mathbin \uparrow \mathbf B_2 & \neg \mathbf B_1 & \neg \mathbf B_2 \\ \neg \paren {\mathbf B_1 \mathbin \downarrow \mathbf B_2} & \mathbf B_1 & \mathbf B_2 \\ \neg \paren {\mathbf B_1 \iff \mathbf B_2} & \neg \paren {\mathbf B_1 \implies \mathbf B_2} & \neg \paren {\mathbf B_2 \implies \mathbf B_1} \\ \mathbf B_1 \oplus \mathbf B_2 & \neg \paren {\mathbf B_1 \implies \mathbf B_2} & \neg \paren {\mathbf B_2 \implies \mathbf B_1} \\ \hline \end{array}$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.2$