\begin{definition}[Definition:Gentzen Proof System/Instance 1/Alpha-Rule]
Let $\LL$ be the language of propositional logic.
Let $\mathscr G$ be instance 1 of a Gentzen proof system.
The '''$\alpha$-rule''' allows for introducing an $\alpha$-formula in the conclusion.
Its precise formulations is as follows:
$(\alpha)$: For any $\alpha$-formula $\mathbf A$ and associated $\mathbf A_1, \mathbf A_2$ from the table of $\alpha$-formulas:
::Given $U_1 \cup \set {\mathbf A_1}$ and $U_2 \cup \set {\mathbf A_2}$, one may infer $U_1 \cup U_2 \cup \set {\mathbf A}$.
\end{definition}