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

From ProofWiki
Jump to navigation Jump to search


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}$.


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}$.