Definition:Gentzen Proof System/Instance 1/Beta-Rule
Jump to navigation
Jump to search
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}$. |
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.2$: Definition $3.2$