\begin{definition}[Definition:Gentzen Proof System/Instance 1/Beta-Rule/Notation]
Let $\mathscr G$ be instance 1 of a Gentzen proof system.
Let $\mathbf B$ be a $\beta$-formula, with $\mathbf B_1, \mathbf B_2$ as in the table of $\beta$-formulas.
In a tableau proof, the $\beta$-rule can be used as follows:
{{begin-axiom}}
{{axiom|lc = '''Pool:'''
       |t  = Empty.
}}
{{axiom|lc = '''Formula:''' 
       |t  = $U_1 \cup \set {\mathbf B}$.
}}
{{axiom|lc = '''Description:''' 
       |t  = $\beta$-Rule.
}}
{{axiom|lc = '''Depends on:''' 
       |t  = The line containing $U_1 \cup \set {\mathbf B_1, \mathbf B_2}$.
}}
{{axiom|lc = '''Abbreviation:''' 
       |t  = $\beta \circ$, where $\circ$ is the binary logical connective such that $\mathbf B {{=}} \mathbf B_1 \circ \mathbf B_2$ or $\mathbf B {{=}} \neg \paren {\mathbf B_1 \circ \mathbf B_2}$.
}}
{{end-axiom}}
Category:Definitions/Mathematical Logic
Category:Definitions/Propositional Logic
\end{definition}