# Definition:Gentzen Proof System

## Definition

**Gentzen proof systems** are a class of proof systems for propositional and predicate logic.

Their characteristics include:

- The presence of few axioms and many rules of inference.
- Use of formal, sequent-like notation involving the turnstile $\vdash$.
- Proofs whose structure can be viewed as rooted trees.

Specific instances may deviate from this general scheme at some points.

### Instance 1

This instance of a Gentzen proof system is used in:

Let $\mathcal L$ 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$ iff $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 \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\}$.

##### $\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 \left\{{\mathbf B_1, \mathbf B_2}\right\}$, one may infer $U_1 \cup \left\{{\mathbf B}\right\}$.

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