Definition:Gentzen Proof System/Instance 1
Definition
This instance of a Gentzen proof system is used in:
Let $\LL$ be the language of propositional logic.
The Gentzen system applies to sets of propositional formulae.
The intuition behind the system is that a set $U$ represents its disjunction.
$\mathscr G$ has the following axioms and rules of inference:
Axioms
A set $U$ of propositional formulae is an axiom of $\mathscr G$ if and only if $U$ contains a complementary pair of literals.
The invocation of an axiom may be denoted by:
- $\vdash U$
Rules of Inference
Let $U_1, U_2$ be sets of propositional formulae.
$\mathscr G$ has two rules of inference, the $\alpha$-rule and the $\beta$-rule:[1]
$\alpha$-Rule
$(\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 \set {\mathbf A_1}$ and $U_2 \cup \set {\mathbf A_2}$, one may infer $U_1 \cup U_2 \cup \set {\mathbf A}$.
$\beta$-Rule
$(\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}$.
Invocations of these rules in a proof can be denoted as:
- $(\alpha) \dfrac {\vdash U_1, \mathbf A_1 \hspace{3em} \vdash U_2, \mathbf A_2} {\vdash U_1, U_2, \mathbf A} \hspace{3em}
(\beta) \dfrac {\vdash U_1, \mathbf B_1, \mathbf B_2} {\vdash U_1, \mathbf B}$
This notation suppresses the set notation as a matter of convenience.
Source of Name
This entry was named for Gerhard Karl Erich Gentzen.
Notes
- ↑ In 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.), the meanings of $\alpha$-formula and $\beta$-formula are interchanged at this point compared to their earlier appearances. This is done because of a later connection with semantic tableaus, but can serve only to confuse. Caution needs to be exercised when using this source, because of the context-dependent meaning of these two terms.
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 3.2$: Definition $3.2$