# Gentzen system

## Introduction

A Gentzen system, attributed to the German logician Gerhard Gentzen, is a variant form of a deductive system. Like a deductive system, a Gentzen system has axioms and inference rules. But, unlike a deductive system, the basic building blocks in a Gentzen system are expressions called sequents, not formulas   .

More precisely, given a language  $L$ of well-formed formulas, a deductive system consists of a set of formulas called axioms, and a set of inference rules, which are pairs of sets of formulas. In a Gentzen system, the formulas are replaced by sequents, which are defined as expressions of the form

 $\Delta\Rightarrow\Gamma,$

where $\Delta$ and $\Gamma$ are finite sequences  of formulas in $L$. The empty sequence is allowed, and is usually denoted by $\varnothing$, $\lambda$, or blank space. In the sequent above, $\Delta$ is called the antecedent  , and $\Gamma$ the succedent. A formula in a sequent is a formula that occurs either in the antecedent or the succedent of the sequent, and a subformula in a sequent is a subformula of some formula in the sequent.

Notation: for any sequence $\Delta$ of formulas, we write

 $\Delta:=\Delta_{1},A,\Delta_{2}$

to mean that $A$ is a formula in $\Delta$. $\Delta_{1}$ and $\Delta_{2}$ are subsequences of $\Delta$, one before $A$, and the other after $A$, both of which may be empty.

## Axioms

As discussed above, axioms of a Gentzen system are sequents. Typically, they are of the following form:

 $\Delta_{1},A,\Delta_{2}\Rightarrow A$

In the case of classical propositional or predicate logic where $\perp$ is the nullary logical connective denoting falsity,

 $\perp\Rightarrow$

is also an axiom. In addition  , when converting a Hilbert system into a Gentzen system, axioms take the form

 $\Rightarrow B,$

where $B$ is an axiom in the Hilbert system.

## Rules of Inference

Rules of inferences have the form

 ${X_{1}\quad X_{2}\quad\cdots\quad X_{n}\over Y}$

where $X_{1},\ldots,X_{n}$ and $Y$ are sequents of the rule. The $X$’s are called the premises, and $Y$ the conclusion. The inference rules of a Gentzen system can be grouped into two main kinds:

• structural rule: a rule is structural if either,

1. (a)

given any premise, every formula in it is also a formula in the conclusion, or

2. (b)

every formula in the conclusion is also a formula in some premise.

In the former case, if there is a formula $B$ in the conclusion not in any of the premises, then $B$ is said to be introduced by the rule. In the later case, if there is a formula $A$ in one of the premises not in the conclusion, then $A$ is said to be eliminated. Some examples of this kind of rules are:

• weakening rules

 ${\Delta_{1},\Delta_{2}\Rightarrow\Gamma\over\Delta_{1},A,\Delta_{2}\Rightarrow% \Gamma}\qquad\mbox{or}\qquad{\Delta\Rightarrow\Gamma_{1},\Gamma_{2}\over\Delta% \Rightarrow\Gamma_{1},B,\Gamma_{2}}$
• contraction rules

 ${\Delta_{1},A,A,\Delta_{2}\Rightarrow\Gamma\over\Delta_{1},A,\Delta_{2}% \Rightarrow\Gamma}\qquad\mbox{or}\qquad{\Delta\Rightarrow\Gamma_{1},B,B,\Gamma% _{2}\over\Delta\Rightarrow\Gamma_{1},B,\Gamma_{2}}$
• exchange rules

 ${\Delta_{1},A,B,\Delta_{2}\Rightarrow\Gamma\over\Delta_{1},B,A,\Delta_{2}% \Rightarrow\Gamma}\qquad\mbox{or}\qquad{\Delta\Rightarrow\Gamma_{1},A,B,\Gamma% _{2}\over\Delta\Rightarrow\Gamma_{1},B,A,\Gamma_{2}}$
• cut rule

 ${\Delta_{1}\Rightarrow\Gamma_{1},A,\Gamma_{2}\qquad\Delta_{2},A,\Delta_{3}% \Rightarrow\Gamma_{3}\over\Delta_{1},\Delta_{2},\Delta_{3}\Rightarrow\Gamma_{1% },\Gamma_{2},\Gamma_{3}}$

where $A$ is called a cut formula.

• logical rule: if it is not a structural rule. In other words, for every premise $X_{i}$, there is at least one formula, say $A_{i}$, in it not in the conclusion $Y$, and a formula $B$ in $Y$ not in any of $X_{i}$’s. Typically, $Y$ is obtained from the $X_{i}$’s via a logical connective. An example of a logical rule is the following:

 ${A,\Delta\Rightarrow\Gamma,B\over\Delta\Rightarrow\Gamma,A\to B}$

## Deductions

Deductions   in a Gentzen system $G$ are finite trees, whose nodes are labeled by sequents. In any deduction, the label of any of its leaves is an axiom. In addition, given any node with label $Y$, its immediate predecessors are nodes with labels $X_{1},\ldots,X_{n}$, such that

 ${X_{1}\quad X_{2}\quad\cdots\quad X_{n}\over Y}$

is a rule of inference in $G$. A sequent $X$ is said to be deducible if there is a deduction whose root has label $X$. A formula $A$ is called a theorem if the sequent $\Rightarrow A$ is deducible.

Remarks.

## References

• 1 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press (2000)
 Title Gentzen system Canonical name GentzenSystem Date of creation 2013-03-22 19:13:20 Last modified on 2013-03-22 19:13:20 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 17 Author CWoo (3771) Entry type Topic Classification msc 03F07 Classification msc 03F03 Classification msc 03B99 Classification msc 03F05 Synonym sequent system Related topic Sequent Related topic HilbertSystem Related topic NaturalDeduction Defines antecedent Defines succedent Defines structural rule Defines logical rule Defines weakening rule Defines contraction rule Defines cut rule Defines exchange rule Defines cut formula