Definition:Gentzen Proof System/Instance 1/Alpha-Rule/Notation

Definition

Let $\mathscr G$ be instance 1 of a Gentzen proof system.

Let $\mathbf A$ be an $\alpha$-formula, with $\mathbf A_1, \mathbf A_2$ as in the table of $\alpha$-formulas.

In a tableau proof, the $\alpha$-rule can be used as follows:

			Pool:					Empty.
			Formula:					$U_1 \cup U_2 \cup \set {\mathbf A}$.
			Description:					$\alpha$-Rule.
			Depends on:					The lines containing $U_1 \cup \set {\mathbf A_1}$ and $U_2 \cup \set {\mathbf A_2}$.
			Abbreviation:					$\alpha \circ$, where $\circ$ is the binary logical connective such that $\mathbf A = \mathbf A_1 \circ \mathbf A_2$ or $\mathbf A = \neg \paren {\mathbf A_1 \circ \mathbf A_2}$, or $\neg \neg$ in the case that $\mathbf A = \neg \neg \mathbf A_1$.