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 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
where and are finite sequences of formulas in . The empty sequence is allowed, and is usually denoted by , , or blank space. In the sequent above, is called the antecedent, and 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 of formulas, we write
to mean that is a formula in . and are subsequences of , one before , and the other after , both of which may be empty.
As discussed above, axioms of a Gentzen system are sequents. Typically, they are of the following form:
In the case of classical propositional or predicate logic where is the nullary logical connective denoting falsity,
where is an axiom in the Hilbert system.
Rules of Inference
Rules of inferences have the form
structural rule: a rule is structural if either,
given any premise, every formula in it is also a formula in the conclusion, or
every formula in the conclusion is also a formula in some premise.
In the former case, if there is a formula in the conclusion not in any of the premises, then is said to be introduced by the rule. In the later case, if there is a formula in one of the premises not in the conclusion, then is said to be eliminated. Some examples of this kind of rules are:
where is called a cut formula.
logical rule: if it is not a structural rule. In other words, for every premise , there is at least one formula, say , in it not in the conclusion , and a formula in not in any of ’s. Typically, is obtained from the ’s via a logical connective. An example of a logical rule is the following:
Deductions in a Gentzen system 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 , its immediate predecessors are nodes with labels , such that
Initially, Gentzen invented the sequent system to analyze the other deductive system he introduced: natural deduction. In fact, sequents can be thought of as abbreviated forms of natural deductions, where the left hand side stands for assumptions (leaves), and right hand side the conclusion (root), and the body of the deduction tree is ignored. Furthermore, if we interpret sequents as formulas themselves, a Gentzen system is really just a deductive system for natural deductions.
In some logical systems, where the exchange rules are automatically assumed, the antecedent and succedent that make up s sequent can be thought of as multisets instead of finite sequences, of formulas, since multisets are just finite sequences modulo order. Furthermore, if the weakening and contraction rules are automatically assumed, then the multisets can be reduced to sets (where multiplicities of elements are forgotten). In classical propositional logic, for example, the sequent can be thought of as the formula , where is the conjunction of formulas in , and is the disjunction of formulas in .
A given logical system may have several distinct but deductively equivalent Gentzen systems. For example, any Gentzen system for classical propositional logic with structural rules can be converted into one without any structural rules.
- 1 A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press (2000)
|Date of creation||2013-03-22 19:13:20|
|Last modified on||2013-03-22 19:13:20|
|Last modified by||CWoo (3771)|