Namespaces
Variants
Actions

Difference between revisions of "Gentzen formal system"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
 +
<!--
 +
g0439801.png
 +
$#A+1 = 51 n = 0
 +
$#C+1 = 51 : ~/encyclopedia/old_files/data/G043/G.0403980 Gentzen formal system
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
A logical calculus which serves for the formalization and study of meaningful proofs that operate by introduction and discharge of hypotheses. Introduced by G. Gentzen [[#References|[2]]]. Gentzen formal systems are subdivided into systems of natural derivations (or natural deduction systems, which imitate the form of ordinary mathematical derivations, and are especially well suited to putting the latter in formal notation) and sequent systems (or logistic systems, which allow the survey of possible proofs of a given formula, obtain results on the normal form of a proof, and their application to [[Proof theory|proof theory]], and to the theory of automated theorem proving). Gentzen formal systems are sometimes identified with systems of sequent type; nevertheless, natural deduction systems may employ sequents (cf. [[Sequent (in logic)|Sequent (in logic)]]), while sequent Gentzen formal systems are sometimes formulated as calculi of formulas rather than of sequents; all Gentzen formal systems are sometimes treated as natural deduction systems, since they reflect to some extent the usual methods of handling logical connectives and assumptions.
 
A logical calculus which serves for the formalization and study of meaningful proofs that operate by introduction and discharge of hypotheses. Introduced by G. Gentzen [[#References|[2]]]. Gentzen formal systems are subdivided into systems of natural derivations (or natural deduction systems, which imitate the form of ordinary mathematical derivations, and are especially well suited to putting the latter in formal notation) and sequent systems (or logistic systems, which allow the survey of possible proofs of a given formula, obtain results on the normal form of a proof, and their application to [[Proof theory|proof theory]], and to the theory of automated theorem proving). Gentzen formal systems are sometimes identified with systems of sequent type; nevertheless, natural deduction systems may employ sequents (cf. [[Sequent (in logic)|Sequent (in logic)]]), while sequent Gentzen formal systems are sometimes formulated as calculi of formulas rather than of sequents; all Gentzen formal systems are sometimes treated as natural deduction systems, since they reflect to some extent the usual methods of handling logical connectives and assumptions.
  
Natural deduction systems comprise rules for the introduction of logical symbols and their discharge. There are few logical axioms (usually one or two). For instance, the natural variant of classical propositional calculus for the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439801.png" /> is defined by the axiom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439802.png" />; by the introduction rules
+
Natural deduction systems comprise rules for the introduction of logical symbols and their discharge. There are few logical axioms (usually one or two). For instance, the natural variant of classical propositional calculus for the language $  \{ \forall , \supset , \neg \} $
 +
is defined by the axiom $  A \rightarrow A $;  
 +
by the introduction rules
 +
 
 +
$$
 +
 
 +
\frac{A, \Gamma \rightarrow B }{\Gamma \rightarrow ( A \supset B) }
 +
\
 +
( \supset  ^ {+} ),\ \
 +
 
 +
\frac{A, \Gamma \rightarrow B \  A, \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow \neg A }
 +
\
 +
( \neg  ^ {+} ),
 +
$$
 +
 
 +
$$
 +
 
 +
\frac{\Gamma \rightarrow A ( b) }{\Gamma \rightarrow \forall x  A ( x) }
 +
  ( \forall  ^ {+} ),
 +
$$
 +
 
 +
where  $  b $
 +
does not occur in  $  \Gamma $
 +
or  $  \forall x  A ( x) $;
 +
by the elimination rules
 +
 
 +
$$
 +
 
 +
\frac{\Gamma \rightarrow A \  \Sigma \rightarrow ( A \supset B) }{\Gamma , \Sigma \rightarrow B }
 +
\
 +
( \supset  ^ {-} ),\ \
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439803.png" /></td> </tr></table>
+
\frac{\Gamma \rightarrow \forall x  A ( x) }{\Gamma \rightarrow A ( t) }
 +
\
 +
( \forall  ^ {-} ),
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439804.png" /></td> </tr></table>
+
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439805.png" /> does not occur in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439806.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439807.png" />; by the elimination rules
+
\frac{\Gamma \rightarrow B \  \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow
 +
\Delta }
 +
  ( \neg  ^ {-} ),\ 
 +
\frac{\Gamma \rightarrow \neg \neg
 +
A }{\Gamma \rightarrow A }
 +
  ( \neg \neg  ^ {-} ),
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439808.png" /></td> </tr></table>
+
where  $  t $
 +
is an arbitrary term; and by structural rules:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g0439809.png" /></td> </tr></table>
+
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398010.png" /> is an arbitrary term; and by structural rules:
+
\frac{\Gamma \rightarrow C }{A, \Gamma \rightarrow C }
 +
\  ( refinement  \textrm{ or }  thinning),
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398011.png" /></td> </tr></table>
+
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398012.png" /></td> </tr></table>
+
\frac{A, A, \Gamma \rightarrow C }{A, \Gamma \rightarrow C }
 +
\  ( contraction ),
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398013.png" /></td> </tr></table>
+
$$
  
The sequent written below the line is said to be the conclusion of the rule, while the sequents above the line are called premises. The axiom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398014.png" /> reflects the introduction of the assumption <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398015.png" />; the rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398016.png" /> illustrates the discharge of an assumption: the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398017.png" /> of the upper sequent depends on the assumption <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398018.png" />, but the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398019.png" /> of the lower sequent no longer depends on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398020.png" />. A natural deduction system is occasionally defined as a calculus of formulas (as distinct from calculi of sequents) with an implicit notation of dependence on the assumptions: a derivation in such a calculus is a tree-like graph, at the vertices of which arbitrary formulas (not necessarily axioms) can be situated, and all the transitions proceed according to derivation rules. These rules are obtained by deleting the antecedents from the respective rules of the natural system described by sequents; discharge of an assumption involves the addition of appropriate conditions; for example,
+
\frac{\Gamma , A, B, \Sigma \rightarrow C }{\Gamma ,\
 +
B, A, \Sigma \rightarrow C }
 +
( rearrangement  \textrm{ or }  permutation).
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398021.png" /></td> </tr></table>
+
The sequent written below the line is said to be the conclusion of the rule, while the sequents above the line are called premises. The axiom  $  A \rightarrow A $
 +
reflects the introduction of the assumption  $  A $;
 +
the rule  $  ( \supset  ^ {+} ) $
 +
illustrates the discharge of an assumption: the formula  $  B $
 +
of the upper sequent depends on the assumption  $  A $,
 +
but the formula  $  A \supset B $
 +
of the lower sequent no longer depends on  $  A $.
 +
A natural deduction system is occasionally defined as a calculus of formulas (as distinct from calculi of sequents) with an implicit notation of dependence on the assumptions: a derivation in such a calculus is a tree-like graph, at the vertices of which arbitrary formulas (not necessarily axioms) can be situated, and all the transitions proceed according to derivation rules. These rules are obtained by deleting the antecedents from the respective rules of the natural system described by sequents; discharge of an assumption involves the addition of appropriate conditions; for example,
  
It is considered that an occurrence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398022.png" /> of a formula in such a derivation depends on an assumption that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398023.png" />, unless <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398024.png" /> is an axiom, is found at a vertex of the derivation above <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398025.png" /> and the assumption <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398026.png" /> is not discharged in the branch leading from the occurrence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398027.png" /> under consideration towards <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398028.png" />. In interpreting a derivation of this kind each occurrence of a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398029.png" /> is transformed to a sequent <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398030.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398031.png" /> is a complete list of assumptions on which the relevant occurrence of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398032.png" /> depends. The connection between natural deduction systems and ordinary (Hilbertian) variants of the corresponding systems is established using the following statement: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398033.png" /> is deducible in the natural deduction system if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398034.png" /> is deducible from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398035.png" /> with fixed variables in an ordinary system.
+
$$
  
Natural deduction systems in their original form are not very suitable for the analytical search for a derivation: attempts to determine the premises and the rules from which a given formula (sequent) may be deduced lead to ambiguities — in principle, this may be the rule for the introduction of the appropriate logical connective or any elimination rule. The set of possible premises in the elimination rules is potentially unlimited (by varying the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398036.png" /> in the rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398037.png" />). It is useful, for this reason, to have rules with the subformula property: The premises contain only the subformulas of the conclusion, while the infinite number of possibilities only occurs in the choice of terms in the rules of the type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398038.png" />. In sequent Gentzen formal systems all formulas have the subformula property or else this property is violated for one rule only — the cut rule
+
\begin{array}{cc}
 +
{}  &[ A]  \\
 +
{}  &\cdot  \\
 +
{}  &\cdot  \\
 +
{}  &\cdot  \\
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398039.png" /></td> </tr></table>
+
\frac{A \  B }{A \& B }
 +
  (\&  ^ {+} ),\  &
 +
\frac{B}{A \supset B }
 +
  ( \supset  ^ {+} ) . \\
 +
\end{array}
  
or another similar rule, e.g. for the rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398040.png" />. Gentzen formal systems with the subformula property are also called cut-free Gentzen formal systems for this reason.
+
$$
 +
 
 +
It is considered that an occurrence  $  V $
 +
of a formula in such a derivation depends on an assumption that  $  D $,
 +
unless  $  D $
 +
is an axiom, is found at a vertex of the derivation above  $  V $
 +
and the assumption  $  D $
 +
is not discharged in the branch leading from the occurrence of  $  D $
 +
under consideration towards  $  V $.
 +
In interpreting a derivation of this kind each occurrence of a formula  $  C $
 +
is transformed to a sequent  $  \Gamma \rightarrow C $,
 +
where  $  \Gamma $
 +
is a complete list of assumptions on which the relevant occurrence of the formula  $  C $
 +
depends. The connection between natural deduction systems and ordinary (Hilbertian) variants of the corresponding systems is established using the following statement:  $  \Gamma \rightarrow C $
 +
is deducible in the natural deduction system if and only if  $  C $
 +
is deducible from  $  \Gamma $
 +
with fixed variables in an ordinary system.
 +
 
 +
Natural deduction systems in their original form are not very suitable for the analytical search for a derivation: attempts to determine the premises and the rules from which a given formula (sequent) may be deduced lead to ambiguities — in principle, this may be the rule for the introduction of the appropriate logical connective or any elimination rule. The set of possible premises in the elimination rules is potentially unlimited (by varying the formula  $  A $
 +
in the rule  $  ( \supset  ^ {-} ) $).
 +
It is useful, for this reason, to have rules with the subformula property: The premises contain only the subformulas of the conclusion, while the infinite number of possibilities only occurs in the choice of terms in the rules of the type  $  ( \forall  ^ {-} ) $.
 +
In sequent Gentzen formal systems all formulas have the subformula property or else this property is violated for one rule only — the cut rule
 +
 
 +
$$
 +
 
 +
\frac{\Gamma \rightarrow A \  A, \Sigma \rightarrow \Delta }{\Gamma , \Sigma \rightarrow \Delta }
 +
 
 +
$$
 +
 
 +
or another similar rule, e.g. for the rule $  ( \neg  ^ {-} ) $.  
 +
Gentzen formal systems with the subformula property are also called cut-free Gentzen formal systems for this reason.
  
 
===Example.===
 
===Example.===
A cut-free variant of the classical predicate calculus LK. The deducible objects are arbitrary sequents, consisting of formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398041.png" />. The axiom is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398042.png" />.
+
A cut-free variant of the classical predicate calculus LK. The deducible objects are arbitrary sequents, consisting of formulas in $  \{ \supset , \neg , \forall \} $.  
 +
The axiom is $  A \rightarrow A $.
  
 
Succedent rules:
 
Succedent rules:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398043.png" /></td> </tr></table>
+
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398044.png" /></td> </tr></table>
+
\frac{A, \Gamma \rightarrow B }{\Gamma \rightarrow ( A \supset B) }
 +
\
 +
(\rightarrow \supset ),\ \
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398045.png" /> does not occur in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398046.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398047.png" />.
+
\frac{A, \Gamma \rightarrow \Delta }{\Gamma \rightarrow \Delta , \neg A }
 +
\
 +
(\rightarrow \neg ),
 +
$$
 +
 
 +
$$
 +
 
 +
\frac{\Gamma \rightarrow \Delta , A ( b) }{\Gamma \rightarrow \Delta , \forall x  A ( x) }
 +
  (\rightarrow \forall ),
 +
$$
 +
 
 +
where $  b $
 +
does not occur in $  \Gamma $
 +
and $  \forall x  A ( x) $.
  
 
Antecedent rules:
 
Antecedent rules:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398048.png" /></td> </tr></table>
+
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398049.png" /></td> </tr></table>
+
\frac{\Gamma \rightarrow \Delta , A }{\neg A, \Gamma \rightarrow \Delta }
 +
\
 +
( \neg \rightarrow ),\ \
 +
 
 +
\frac{A  ( t), \Gamma \rightarrow \Delta }{\forall x  A ( x), \Gamma \rightarrow \Delta }
 +
\
 +
( \forall \rightarrow ),
 +
$$
 +
 
 +
$$
 +
 
 +
\frac{\Gamma \rightarrow \Delta , A \  B, \Gamma \rightarrow \Delta }{A \supset B,\  \Gamma \rightarrow \Delta }
 +
  ( \supset \rightarrow ).
 +
$$
  
 
Structural rules: cut, rearrangement, refinement and contraction in the antecedent and in the succedent (cf. [[Sequent (in logic)|Sequent (in logic)]]).
 
Structural rules: cut, rearrangement, refinement and contraction in the antecedent and in the succedent (cf. [[Sequent (in logic)|Sequent (in logic)]]).
Line 56: Line 189:
 
Gentzen formal systems make it possible to express meaningful features of theories with the aid of purely-constructive concepts; thus, a Gentzen formal system of intuitionistic mathematics often differs from the corresponding classical system only in that mono-succedent rather than arbitrary sequents are employed. In cut-free systems consistency (i.e. non-deducibility of the empty sequent) and the deducibility of one of the disjunctive terms of a disjunction (in the intuitionistic case) being deduced are readily shown.
 
Gentzen formal systems make it possible to express meaningful features of theories with the aid of purely-constructive concepts; thus, a Gentzen formal system of intuitionistic mathematics often differs from the corresponding classical system only in that mono-succedent rather than arbitrary sequents are employed. In cut-free systems consistency (i.e. non-deducibility of the empty sequent) and the deducibility of one of the disjunctive terms of a disjunction (in the intuitionistic case) being deduced are readily shown.
  
An important generalization of Gentzen formal systems are semi-formal systems containing rules with an infinite set of premises, such as the rule of infinite induction (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398050.png" />-rule):
+
An important generalization of Gentzen formal systems are semi-formal systems containing rules with an infinite set of premises, such as the rule of infinite induction ( $  \omega $-
 +
rule):
 +
 
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/g/g043/g043980/g04398051.png" /></td> </tr></table>
+
\frac{A ( 0) \dots A ( N) , . . . }{\forall x  A ( x) }
 +
.
 +
$$
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  G. Gentzen,  "Untersuchungen über das logische Schliessen"  ''Math. Z.'' , '''39'''  (1934)  pp. 176–210; 405–431</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  H.B. Curry,  "Foundations of mathematical logic" , McGraw-Hill  (1963)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  D. Prawitz,  "Ideas and results in proof theory"  J.E. Fenstad (ed.) , ''Proc. 2-nd Scand. Logic Symp.'' , North-Holland  (1971)  pp. 235–308</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  G. Gentzen,  "Untersuchungen über das logische Schliessen"  ''Math. Z.'' , '''39'''  (1934)  pp. 176–210; 405–431</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  H.B. Curry,  "Foundations of mathematical logic" , McGraw-Hill  (1963)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  D. Prawitz,  "Ideas and results in proof theory"  J.E. Fenstad (ed.) , ''Proc. 2-nd Scand. Logic Symp.'' , North-Holland  (1971)  pp. 235–308</TD></TR></table>

Latest revision as of 19:41, 5 June 2020


A logical calculus which serves for the formalization and study of meaningful proofs that operate by introduction and discharge of hypotheses. Introduced by G. Gentzen [2]. Gentzen formal systems are subdivided into systems of natural derivations (or natural deduction systems, which imitate the form of ordinary mathematical derivations, and are especially well suited to putting the latter in formal notation) and sequent systems (or logistic systems, which allow the survey of possible proofs of a given formula, obtain results on the normal form of a proof, and their application to proof theory, and to the theory of automated theorem proving). Gentzen formal systems are sometimes identified with systems of sequent type; nevertheless, natural deduction systems may employ sequents (cf. Sequent (in logic)), while sequent Gentzen formal systems are sometimes formulated as calculi of formulas rather than of sequents; all Gentzen formal systems are sometimes treated as natural deduction systems, since they reflect to some extent the usual methods of handling logical connectives and assumptions.

Natural deduction systems comprise rules for the introduction of logical symbols and their discharge. There are few logical axioms (usually one or two). For instance, the natural variant of classical propositional calculus for the language $ \{ \forall , \supset , \neg \} $ is defined by the axiom $ A \rightarrow A $; by the introduction rules

$$ \frac{A, \Gamma \rightarrow B }{\Gamma \rightarrow ( A \supset B) } \ ( \supset ^ {+} ),\ \ \frac{A, \Gamma \rightarrow B \ A, \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow \neg A } \ ( \neg ^ {+} ), $$

$$ \frac{\Gamma \rightarrow A ( b) }{\Gamma \rightarrow \forall x A ( x) } ( \forall ^ {+} ), $$

where $ b $ does not occur in $ \Gamma $ or $ \forall x A ( x) $; by the elimination rules

$$ \frac{\Gamma \rightarrow A \ \Sigma \rightarrow ( A \supset B) }{\Gamma , \Sigma \rightarrow B } \ ( \supset ^ {-} ),\ \ \frac{\Gamma \rightarrow \forall x A ( x) }{\Gamma \rightarrow A ( t) } \ ( \forall ^ {-} ), $$

$$ \frac{\Gamma \rightarrow B \ \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow \Delta } ( \neg ^ {-} ),\ \frac{\Gamma \rightarrow \neg \neg A }{\Gamma \rightarrow A } ( \neg \neg ^ {-} ), $$

where $ t $ is an arbitrary term; and by structural rules:

$$ \frac{\Gamma \rightarrow C }{A, \Gamma \rightarrow C } \ ( refinement \textrm{ or } thinning), $$

$$ \frac{A, A, \Gamma \rightarrow C }{A, \Gamma \rightarrow C } \ ( contraction ), $$

$$ \frac{\Gamma , A, B, \Sigma \rightarrow C }{\Gamma ,\ B, A, \Sigma \rightarrow C } \ ( rearrangement \textrm{ or } permutation). $$

The sequent written below the line is said to be the conclusion of the rule, while the sequents above the line are called premises. The axiom $ A \rightarrow A $ reflects the introduction of the assumption $ A $; the rule $ ( \supset ^ {+} ) $ illustrates the discharge of an assumption: the formula $ B $ of the upper sequent depends on the assumption $ A $, but the formula $ A \supset B $ of the lower sequent no longer depends on $ A $. A natural deduction system is occasionally defined as a calculus of formulas (as distinct from calculi of sequents) with an implicit notation of dependence on the assumptions: a derivation in such a calculus is a tree-like graph, at the vertices of which arbitrary formulas (not necessarily axioms) can be situated, and all the transitions proceed according to derivation rules. These rules are obtained by deleting the antecedents from the respective rules of the natural system described by sequents; discharge of an assumption involves the addition of appropriate conditions; for example,

$$ \begin{array}{cc} {} &[ A] \\ {} &\cdot \\ {} &\cdot \\ {} &\cdot \\ \frac{A \ B }{A \& B } (\& ^ {+} ),\ & \frac{B}{A \supset B } ( \supset ^ {+} ) . \\ \end{array} $$

It is considered that an occurrence $ V $ of a formula in such a derivation depends on an assumption that $ D $, unless $ D $ is an axiom, is found at a vertex of the derivation above $ V $ and the assumption $ D $ is not discharged in the branch leading from the occurrence of $ D $ under consideration towards $ V $. In interpreting a derivation of this kind each occurrence of a formula $ C $ is transformed to a sequent $ \Gamma \rightarrow C $, where $ \Gamma $ is a complete list of assumptions on which the relevant occurrence of the formula $ C $ depends. The connection between natural deduction systems and ordinary (Hilbertian) variants of the corresponding systems is established using the following statement: $ \Gamma \rightarrow C $ is deducible in the natural deduction system if and only if $ C $ is deducible from $ \Gamma $ with fixed variables in an ordinary system.

Natural deduction systems in their original form are not very suitable for the analytical search for a derivation: attempts to determine the premises and the rules from which a given formula (sequent) may be deduced lead to ambiguities — in principle, this may be the rule for the introduction of the appropriate logical connective or any elimination rule. The set of possible premises in the elimination rules is potentially unlimited (by varying the formula $ A $ in the rule $ ( \supset ^ {-} ) $). It is useful, for this reason, to have rules with the subformula property: The premises contain only the subformulas of the conclusion, while the infinite number of possibilities only occurs in the choice of terms in the rules of the type $ ( \forall ^ {-} ) $. In sequent Gentzen formal systems all formulas have the subformula property or else this property is violated for one rule only — the cut rule

$$ \frac{\Gamma \rightarrow A \ A, \Sigma \rightarrow \Delta }{\Gamma , \Sigma \rightarrow \Delta } $$

or another similar rule, e.g. for the rule $ ( \neg ^ {-} ) $. Gentzen formal systems with the subformula property are also called cut-free Gentzen formal systems for this reason.

Example.

A cut-free variant of the classical predicate calculus LK. The deducible objects are arbitrary sequents, consisting of formulas in $ \{ \supset , \neg , \forall \} $. The axiom is $ A \rightarrow A $.

Succedent rules:

$$ \frac{A, \Gamma \rightarrow B }{\Gamma \rightarrow ( A \supset B) } \ (\rightarrow \supset ),\ \ \frac{A, \Gamma \rightarrow \Delta }{\Gamma \rightarrow \Delta , \neg A } \ (\rightarrow \neg ), $$

$$ \frac{\Gamma \rightarrow \Delta , A ( b) }{\Gamma \rightarrow \Delta , \forall x A ( x) } (\rightarrow \forall ), $$

where $ b $ does not occur in $ \Gamma $ and $ \forall x A ( x) $.

Antecedent rules:

$$ \frac{\Gamma \rightarrow \Delta , A }{\neg A, \Gamma \rightarrow \Delta } \ ( \neg \rightarrow ),\ \ \frac{A ( t), \Gamma \rightarrow \Delta }{\forall x A ( x), \Gamma \rightarrow \Delta } \ ( \forall \rightarrow ), $$

$$ \frac{\Gamma \rightarrow \Delta , A \ B, \Gamma \rightarrow \Delta }{A \supset B,\ \Gamma \rightarrow \Delta } ( \supset \rightarrow ). $$

Structural rules: cut, rearrangement, refinement and contraction in the antecedent and in the succedent (cf. Sequent (in logic)).

In comparing sequent and natural deduction systems, succedent rules correspond to introduction rules, while antecedent rules correspond to elimination rules. The cut is employed in modelling the elimination rules in sequent Gentzen formal systems. The subformula property for LK is ensured by Gentzen's theorem (the cut-elimination theorem): For each derivation in LK it is possible to construct a cut-free derivation (of the same sequent). This theorem makes it possible to establish the solvability of quantifier-free systems: using subformulas of a given quantifier-free formula it is possible to construct only a finite number of matching sequents (sequents are matching if they differ only in the order and in the repetitions of terms in the antecedent and in the succedent), from which it is possible in turn to construct only a finite number of "candidates" to yield derivations; the given formula is provable if such candidates include a derivation.

Gentzen formal systems make it possible to express meaningful features of theories with the aid of purely-constructive concepts; thus, a Gentzen formal system of intuitionistic mathematics often differs from the corresponding classical system only in that mono-succedent rather than arbitrary sequents are employed. In cut-free systems consistency (i.e. non-deducibility of the empty sequent) and the deducibility of one of the disjunctive terms of a disjunction (in the intuitionistic case) being deduced are readily shown.

An important generalization of Gentzen formal systems are semi-formal systems containing rules with an infinite set of premises, such as the rule of infinite induction ( $ \omega $- rule):

$$ \frac{A ( 0) \dots A ( N) , . . . }{\forall x A ( x) } . $$

References

[1] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2] G. Gentzen, "Untersuchungen über das logische Schliessen" Math. Z. , 39 (1934) pp. 176–210; 405–431
[3] H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963)
[4] D. Prawitz, "Ideas and results in proof theory" J.E. Fenstad (ed.) , Proc. 2-nd Scand. Logic Symp. , North-Holland (1971) pp. 235–308
How to Cite This Entry:
Gentzen formal system. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Gentzen_formal_system&oldid=13610
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article