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

From ProofWiki
Jump to navigation Jump to search


Let $\mathcal L$ 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 \left\{{\mathbf B_1, \mathbf B_2}\right\}$, one may infer $U_1 \cup \left\{{\mathbf B}\right\}$.


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

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