# Definition:Gentzen Proof System/Instance 1/Beta-Rule

## Definition

Let $\LL$ be the language of propositional logic.

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

The $\beta$-rule allows for introducing a $\beta$-formula in the conclusion.

Its precise formulations is as follows:

$(\beta)$: For any $\beta$-formula $\mathbf B$ and associated $\mathbf B_1, \mathbf B_2$ from the table of $\beta$-formulas:

Given $U_1 \cup \set {\mathbf B_1, \mathbf B_2}$, one may infer $U_1 \cup \set {\mathbf B}$.

### Notation

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

 Pool: Empty. Formula: $U_1 \cup \set {\mathbf B}$. Description: $\beta$-Rule. Depends on: The line containing $U_1 \cup \set {\mathbf B_1, \mathbf B_2}$. Abbreviation: $\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}$.