Gentzenscher's law

The Gentzensche main clause or section set is a set of mathematical logic , stating that the cut rule in Gentz type calculi permitted is. It is named after Gerhard Gentzen , who established and proved it in 1934.

The cutting rule

The cutting rule is the modus ponens on the metalogical level:

Suppose the sequences and are derivable. The rule of intersection says that you can then move on to the sequence , i.e. H. the formula can then also be derived without . ${\displaystyle \Gamma \vdash A}$ ${\displaystyle A,\Delta \vdash B}$ ${\displaystyle \Gamma ,\Delta \vdash B}$ ${\displaystyle B}$ ${\displaystyle A}$

The Greek letters and stand for lists of formulas that have already been derived. The symbol is used here for derivation . ${\displaystyle \Gamma }$ ${\displaystyle \Delta }$ ${\displaystyle \vdash }$

Evidence sketch

Evidence for this main theorem is now available in simple form. The basic idea is derivations in which the cut rule is used, dissolve (English: cut elimination) that it is not used more.

To do this, a complete induction is carried out using the number of partial formulas in the sectional formula (partial formula induction). ${\displaystyle A}$

Induction start ( ): If it only has a partial formula, i.e. it is not a compound, it must be a prime or atomic formula : ${\displaystyle n=1}$ ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle a}$

${\displaystyle {\frac {\Gamma \vdash a\qquad a,\Delta \vdash \ B}{\Gamma ,\Delta \vdash \ B}}}$ .

In the simplest case, it is not used in the derivation . Then this derivation is also valid without , i.e. H. . But this means that it can be derived without the intersection rule. ${\displaystyle a}$ ${\displaystyle a,\Delta \vdash B}$ ${\displaystyle a}$ ${\displaystyle \Delta \vdash B}$ ${\displaystyle B}$

If, on the other hand, appears in the derivation , you can replace it with the derivation . In this case, too, there is a possibility to derive without the cut rule. ${\displaystyle a}$ ${\displaystyle a,\Delta \vdash B}$ ${\displaystyle a}$ ${\displaystyle \Gamma \vdash a}$ ${\displaystyle B}$

Induction step ( zu ): The induction assumption states that the rule of intersection is valid for the formulas that have n sub-formulas: ${\displaystyle n}$ ${\displaystyle n+1}$ ${\displaystyle A}$

${\displaystyle {\frac {\Gamma \vdash A_{n}\qquad A_{n},\Delta \vdash \ B}{\Gamma ,\Delta \vdash \ B}}}$ .

A case distinction is now made in relation to that in:

${\displaystyle {\frac {\Gamma \vdash A_{n+1}\qquad A_{n+1},\Delta \vdash \ B}{\Gamma ,\Delta \vdash \ B}}}$

newly added logic characters are carried out, so the rule of intersection is replaced by the calculation rules for this character.

In the case of the joiners , this part of the evidence is relatively simple despite the many case distinctions. In the case of the quantifiers , the number of development steps is induced in the dialogical proof.

The (long) non- dialogical proofs additionally use the so-called mixed rule (Mix), which can be proven from the intersection rule:

${\displaystyle {\frac {\Gamma \vdash M\qquad \Delta \vdash \ B}{\Gamma ,(\Delta -M)\vdash B}}}$ .

${\displaystyle M}$is called a mixed formula and describes the formula sequence that arises when you delete each one that occurs . ${\displaystyle \Delta -M}$ ${\displaystyle \Delta }$ ${\displaystyle M}$

Consistency

The calculi to which the main theorem applies are free of contradictions.

One line of thought of consistency is as follows: Be (read: false or falsum) by definition not inferable. Then there is nothing else than the deducibility of The negation is this special case of the subjunction . ${\displaystyle \bot }$ ${\displaystyle A\vdash \bot }$ ${\displaystyle \neg A.}$

If we now insert (for ): into the intersection rule: ${\displaystyle B}$ ${\displaystyle \bot }$

${\displaystyle {\frac {\Gamma \vdash A\qquad \Gamma ,A\vdash \ \bot }{\Gamma \vdash \ \bot }}}$

so from the deducibility of and the (just mentioned) of (both together are a contradiction in the premises) the deducibility of the inerivable that which cannot be. would - because of the eliminability of the rule of intersection - also be a valid sequence in the calculus itself, which is by definition not possible. It is typical for these proofs of freedom from contradiction that in a derivation only partial formulas of those formulas appear that appear in the derived end sequence (i.e. under the line). ${\displaystyle A}$ ${\displaystyle \neg }$ ${\displaystyle A}$ ${\displaystyle \bot }$ ${\displaystyle \Gamma \vdash \ \bot }$ ${\displaystyle \bot }$

Proofs of freedom from contradictions in mathematics are carried out by including, like Gerhard Gentzen, the transfinite induction or, like Kurt Schütte and Paul Lorenzen , the so-called rule , in the proofs of the main theorem (complete semi-formalism). ${\displaystyle \omega }$

Importance and uses

The removal of sections is not only a way of proving the validity of the cut rule, but, conversely, a very useful mathematical-logical tool, for example when proving the interpolation theorem of Craig and Schütte . The ability to carry out proofs based on resolution is very powerful ( machine-aided proof ). The execution of a Prolog program (i.e. what happens while the Prolog program is running) can be interpreted as a cut-free calculus derivation.

However, if one carries out proofs in gentz type calculi that avoid the cut (analytic proofs), these are usually longer than when using the cut rule. In his article "Don't Eliminate Cut!" the mathematician and logician George Boolos showed that there is a formula that can be derived in about one page with the help of the section, while it would take longer than the entire lifetime of the universe to write a derivation that does not require a section.

By applying the cut rule, modal logic statements can be justified if the corresponding logical statements are true. The knowledge that must always be assumed in the modal logic can in this case be cut away. Gentzen's law also serves as a foundation for modal logic, because this is how modal logic truth can be defined.

The so-called tightened law is similar to Herbrand's theorem . It is about the role of the quantifiers in a proof.

swell

1. ↑ Inhetveen 2003 ( dialogical proof), p. 197; Heindorf 1994, p. 105; Lorenzen 2000 (dialogical proof), p. 81
2. ↑ see Gentzen and Heindorf
3. ↑ This is the basic idea of ​​Paul Lorenzen in the metamathematics and in the textbook dkW 2000 p. 80ff

literature

• Gerhard Gentzen: Investigations into logical reasoning. Mathematical Journal 39 (1934). Reprinted in: Karel Berka , Lothar Kreiser: Logic Texts , Berlin (East) 1986. Part 1 and Part 2
• Stephen Cole Kleene : Introduction to Metamathematics , Amsterdam Groningen 1952
• Paul Lorenzen : Metamathematik , Mannheim 1962
• Gerhard Gentzen (ed. ME Szabo): The Collected Papers of Gerhard Gentzen , Amsterdam 1969
• Kuno Lorenz , P. Lorenzen: Dialogical Logic , Darmstadt 1978 - (Contains for the first time a proof based on dialogical game theory .)
• Paul Lorenzen: Textbook of the constructive philosophy of science , Zurich 1987, Stuttgart 2000, ISBN 3-476-01784-2
• Kurt Schütte: Theory of Proof , Berlin Göttingen Heidelberg 1960
• AS Troelstra , H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0521779111
• Gerrit Haas: Constructive Introduction to Formal Logic 1984 ISBN 3411016280
• George Boolos: Don't eliminate cut in: Journal of Philosophical Logic 13 (1984), pp. 373-378.
• Lutz Heindorf: Elementary Proof Theory , 1994 ISBN 3411171618
• Eckart Menzler-Trott : Gentzen's Problem. Mathematical Logic in National Socialist Germany. Birkhäuser Verlag, Basel 2001, ISBN 3764365749
• Peter Schroeder-Heister: Cut-elimination in logics with definitional reflection (PDF; 1.3 MB). Nonclassical Logics and Information Processing , pp. 146-171, 1990. In D. Pearce, H. Wansing (Editors): Nonclassical Logics and Information Processing. International Workshop, Berlin, November 9-10 1990, Proceedings. Springer Lecture Notes in Artificial Intelligence 619, Berlin / Heidelberg / New York 1992, ISBN 3-540-55745-8 .
• Jean-Yves Girard : Proofs and Types Cambridge University Press 1989; reprint web 2003 (PDF; 925 kB)
• Sakharov, Alex. Cut Elimination Theorem. From MathWorld - A Wolfram Web Resource, created by Eric W. Weisstein.
• Rüdiger Inhetveen: Logic. A dialogue-oriented introduction, Leipzig 2003 ISBN 3-937219-02-1
• William W. Tait , Gödels reformulation of Gentzen's first consistency proof for arithmetic (PDF; 236 kB). English article in: The Bulletin of Symbolic Logic 11 (2): pp. 225-238, 2005