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

From ProofWiki
Jump to navigation Jump to search

Definition

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:

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