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

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\mathcal L$ be the language of propositional logic.

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


The $\alpha$-rule allows for introducing an $\alpha$-formula in the conclusion.

Its precise formulations is as follows:


$(\alpha)$: For any $\alpha$-formula $\mathbf A$ and associated $\mathbf A_1, \mathbf A_2$ from the table of $\alpha$-formulas:

Given $U_1 \cup \left\{{\mathbf A_1}\right\}$ and $U_2 \cup \left\{{\mathbf A_2}\right\}$, one may infer $U_1 \cup U_2 \cup \left\{{\mathbf A}\right\}$.


Notation

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

Pool:    Empty.             
Formula:    $U_1 \cup U_2 \cup \left\{ {\mathbf A}\right\}$.             
Description:    $\alpha$-Rule.             
Depends on:    The lines containing $U_1 \cup \left\{ {\mathbf A_1}\right\}$ and $U_2 \cup \left\{ {\mathbf A_2}\right\}$.             
Abbreviation:    $\alpha \circ$, where $\circ$ is the binary logical connective such that $\mathbf A = \mathbf A_1 \circ \mathbf A_2$ or $\mathbf A = \neg \left({\mathbf A_1 \circ \mathbf A_2}\right)$, or $\neg \neg$ in the case that $\mathbf A = \neg \neg \mathbf A_1$.             


Sources