1 Introduction
It turned out in 1984 that Gerhard Gentzen (1909–1945) had left behind two slim folders of shorthand notes. These can be divided into three groups: Notes on the proof theory of intuitionistic number theory, acronym BTIZ, notes on the consistency of analysis, acronym WA, and the rest. The third group is transcribed and translated into English in the book Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic and Foundations of Mathematics (von Plato Reference von Plato2017). The second series contains a manuscript with the cryptic title WKRd; it stands for something like Widerspruchsfreiheit, Kalküle und Reduktionen, Durchsicht (consistency, calculi and reductions, overview) (see the Appendix). The manuscript consists of eight beautifully written pages on two folded sheets. They are a summary of a lost long series WKR that contained work on sequent calculi and various reduction methods for derivations in these calculi.
Gentzen’s series of shorthand notes that begin with the letter W contain materials about consistency proofs or “Widerspruchsfreiheitsbeweise” that translates, literally, as “proofs of freedom from contradiction.” Thus, WA stands for Widerspruchsfreiheit Analysis and WTZ for Widerspruchsfreiheit transfinite Zahlen, the latter unfortunately completely lost. The page numbers indicate that WA ran up to at least 337 pages, of which some two hundred have been preserved. Gentzen left the two folders of notes in a family summer place on the Baltic island of Rügen, near his home town Stralsund, during a visit in August 1944. His mother Melanie Gentzen, and after her, his sister Waltraut Student kept them and made them available to Prof. Christian Thiel 40 years later, as detailed in von Plato (Reference von Plato2017).
What is left of the series WA has been written in two stretches: A first one is, following the style of dates found in Gentzen’s manuscripts, from 11.VIII.38 to 8.XII.38, with the pages 77–80 (11.VIII.), 111–116 (29.IX.), 121–128 (1.–11.X.), 135–146 (–8.XI.), 169–172 (22.XI.–3.XII.), and 177–180 (8.XII.); altogether 38 pages.
A second series of notes with the signum WA follows between May and September 1943. The pages that have remained are 183–184 (11.V.43), 187–197, 198.01, 198.02, 198.5–198.11 (9.VI.–1.VIII.), 209–222 (3.VIII.–15.IX.), and 225–254 (–27.IX.43); altogether 56 pages.
The preserved shorthand pages in the series WA amount to some 150 printed pages, the whole of it for pages 1–339 to some 500 pages.
Next to the two preserved folders of Gentzen’s shorthand manuscripts, there exists a 13-page cryptic summary of “the most modern parts” of WA, for the pages 255–339, thus in direct continuation of the preserved pages. This manuscript was recovered much earlier than 1984, namely in 1948, and transcribed at that time from the shorthand. It is preserved in a typewritten form as a carbon copy, very hard to read at places, with the original shorthand having been lost in the meanwhile. This manuscript bears the date II.45 and is called WAdd. It is the last known writing in Gentzen’s hand.
The main aim of all the W-series was to bring further Gentzen’s central problem after he had found the proof of consistency of Peano arithmetic in 1935, namely a proof of the consistency of analysis. The first proof of consistency for Peano arithmetic was by bar induction, used but not made explicit, in Gentzen (Reference Gentzen1935).Footnote
1
In Gentzen (Reference Gentzen1936), Gentzen developed a special arithmetic notation for the constructive ordinals up to
$\varepsilon _0$
. The point of the notation was to emphasize the “nominalistic” character of such ordinals, as not being dependent on set theory.Footnote
2
Gentzen’s published proof of 1936 used as a logical system natural deduction, written in sequent calculus style, with a notation as in
$\Gamma \rightarrow A$
. Here,
$\Gamma $
stands for a list of open assumptions in a natural deduction derivation of formula A. The use of such sequents within natural deduction is explained by a second special feature of Gentzen’s article, namely, by derivations in the system being plain lists of sequents. The state of the art would have been to give the formal derivations in the two-dimensional tree form of Gentzen’s doctoral thesis. These derivation trees are found for the first time in the 1933 doctoral thesis Untersuchungen über das logische Schliessen, in which assumptions appear as top formulas of the trees. The effect is that the deductive dependencies in a proof get an exact representation: Any formula in a derivation tree depends on exactly those open assumptions that are found in the subtree determined by that formula.
The mentioned features of the 1936 article should be concessions towards Gentzen’s projected readers, namely, any mathematician who follows the premier mathematics journal of the German-speaking world, the Mathematische Annalen. The paper begins with a general overview of foundational problems, one Bernays in correspondence suggested to be deleted, but Gentzen persisted. His article was meant to be readable even by those who know little about logic and therefore would not have heard of sequent calculus nor seen two-dimensional derivation trees but could be led into understanding the basics of natural deduction if they are suitably presented.
2 Background: the proof of 1938
Gentzen’s proof of consistency by bar induction reached the stage of proofs in late 1935. Bernays had the article with him in Princeton where he stayed for the academic year 1935–36. Even Gödel, actually on board the same transatlantic ocean liner as Bernays in late September 1935, studied the manuscript carefully, in particular the “reduction procedure” Gentzen defined. Gödel read Gentzen as giving a notion of arithmetic truth as failure of an idealized refutation procedure. It is the idea behind the no-counterexample interpretation that in turn led Gödel to his functional interpretation.
Gentzen’s correspondence with Bernays shows that the proof of consistency was discussed and subjected to criticism among Bernays, Gödel, and von Neumann, with the result that Gentzen changed the proof into one that uses transfinite induction.Footnote 3 He rewrote large sections of the manuscript, with an overall effect that was anything but optimal. Bernays had kept the proofs of the original version that had its first publication, in an English translation, in Gentzen’s Collected Papers of 1969, then in the German original in 1974.
Gentzen turned to his consistency proof 2 years later, in Gentzen (Reference Gentzen1938), this time with no compromises in the presentation: He used the standard notation for ordinals and a proper sequent calculus as the logical formalism. He had to make a modification in the treatment of the classical sequent calculus LK of his doctoral thesis (Gentzen Reference Gentzen1934–35), for a rather subtle reason that at the same time points at the crucial role of a properly formulated calculus. Namely, in 1934–35, Gentzen used in the crucial cut elimination theorem what is known as the “mix” rule, a formulation of the rule of cut in which several cut formulas can get removed in one step, this “for ease of presentation” as he wrote. As we shall see, this proof method would not suit the aims of Gentzen’s proof of the consistency of arithmetic within the calculus LK.
Gentzen in his manuscripts referred to the 1938 proof as “Neu” (new). The reception of this proof was good, among the few who cared to learn the formalism. One who praised it was Laszlo Kalmár, but he also wrote a version of the proof in terms of axiomatic logic, for those “who don’t care to take the trouble of learning a new formalism,” as he put it (Kalmar Reference Kalmár1938).
The calculus LK has sequents of the form
$\Gamma \rightarrow \Delta $
, with lists of formulas on both sides of the sequent arrow. Gentzen gives in 1938 the reading that
$\Delta $
lists the cases that follow from the list of assumptions in
$\Gamma $
(as in Neu, p. 21). As a limiting case, lists on both sides of a sequent can be absent, with the empty sequent
$ \rightarrow$
as a result that expresses contradiction.
As LK is a classical calculus, Gentzen leaves out implication from the formalism of Neu, but he retains the rest of the connectives and quantifiers,
$\&, \lor , \neg , \forall , \exists $
. The reason is that
$\&$
and
$\lor $
, and
$\forall $
and
$\exists $
, obey a remarkable duality in LK, one that makes the notation easy to read. Even
$\neg $
is self-dual; all of this is carefully displayed in the layout of the rules in the printed article, with their mirror image like arrangement Gentzen had designed for the publication. He divides the rules into logical, structural, and mathematical ones. The first group of rules is:
Logical rules of the classical sequent calculus LK
The rules have shared contexts
$\Gamma , \Delta $
in both of the two-premiss rules
$\&R$
and
$\lor L$
. It is a property by which it possible to read the rules in a root-first manner, from the endsequent of a derivation upwards: Whenever the principal formula in a sequent is chosen, its main connective corresponds to one of the left or right rules, and the premisses with the active formulas (immediate subformulas of the principal formula) become uniquely determined. There is only one slight blemish with Gentzen’s rules for LK in this respect, namely that the premiss is not uniquely determined in the left conjunction and right disjunction rules; either one of the conjuncts or disjuncts can be chosen to be the active formula in the premiss.
An innocent-looking modification proposed by Ketonen (Reference Ketonen1944), for the explicit purpose of having a system that supports root-first proof search, will correct the above defect. Ketonen has a single left conjunction and right disjunction rule:
Ketonen’s invertible sequent rules
Gentzen in 1938 had put implication aside, for a greater symmetry, but Ketonen’s Reference Ketonen1944 calculus has even the left implication rule properly formulated, as an invertible rule.
The calculus of Ketonen is the same as the modern invertible G3 sequent calculus, from which it differs only in the quantificational part, with respect to the left universal and right existential rules: To make the calculus to fully support root-first proof search also with the quantifier rules, the principal formulas
$\forall xA(x)$
and
$\exists xA(x)$
in the conclusions of
$\forall L$
and
$\exists R$
have to be repeated in the premisses, the intuitive motivation being that if an instance
$A(t)$
fails to lead to success in root-first proof search, new instances can be later tried.
The structural rules in LK are thinning, contraction, and exchange, and lastly Cut:
Structural rules of the calculus LK
Note that rule Cut has independent contexts in the two premisses, added up in the conclusion. The reason for this will turn up soon.
Derivations in LK begin with initial sequents that have the form
$ A\rightarrow A$
. As noted by Ketonen (Reference Ketonen1944), one can continue root-first proof search from
$A \rightarrow A$
until all formulas in initial sequents are atomic. Research in proof theory has led, through Ketonen (Reference Ketonen1944), Kleene (Reference Kleene1952), and Dragalin (Reference Dragalin1988), to the remarkable G3 sequent calculi in which root-first proof search by just the logical rules, all of the structural ones left apart, gives a complete system. – The point with these observations is to show how close in 1938 Gentzen came to later developments in structural proof theory.
Gentzen’s proof of consistency in Neu has a system of Peano arithmetic that is added to the above logical calculus. He formulates induction as a mathematical rule of inference added to the calculus LK. The rest of the arithmetical axioms are given as mathematical groundsequents:
Mathematical rule added to LK
The eigenvariable a must not occur free in
$\Gamma $
and t is an arbitrary term. The rest of the arithmetical axioms are handled by mathematical groundsequents such as
$a= b \rightarrow b = a$
and
$a=b,b=c \rightarrow a= c$
. These are added next to the initial sequents, to form together the topsequents of a derivation. Gentzen gives little attention to the treatment of arithmetical axioms beyond the rule of induction, thinking that the consistency of parts of derivations that use just the mathematical groundsequents combined by cuts is obvious, that is, in the end, appealing to an intuitive semantical argument.Footnote
4
Gentzen in Neu next assumes there to be at hand a derivation of the empty sequent. An inspection of the logical, structural, and mathematical rules shows that Cut is the only rule that can have the empty sequent as a conclusion:
The endpiece of a derivation of
$ \rightarrow $
is determined by climbing up from the root in the sequent calculus derivation tree until the lower sequent of an instance of a logical rule or a topsequent in the derivation is found. Thus, the endpiece contains only structural rules.
A crucial lemma, with a lousy proof by the way, states that there is at least one cut in the endpiece in which, when that cut is permuted up to where the endpiece begins, the cut formula is principal in the left and right premiss of cut.Footnote
5
Then that cut can be replaced by cuts that reduce the complexity of the derivation, where such complexity has a rather involved definition in Neu. Here, instead, is a simple example that gives the basic idea of how cut elimination works. We have a derivation with the cut formula
$A\& B$
that is principal in both of the premisses of cut:
The part of derivation is replaced by:
It is clear in what sense the derivation is simplified: The new cut is on a shorter formula.Footnote 6
Why the old mix rule of 1934–35 does not work with the cut elimination procedure in Neu was, after considerable asking around, pointed out in 2005 by Michael Rathjen: The order of application of two successive instances of mix need not commute, whereas two instances of cut always commute – the latter a property that is crucial in Neu. It is for this reason that independent contexts are needed in rule Cut.
As just intimated, there is a further complication in the reduction of the complexity of derivations in Gentzen’s Reference Kalmár1938 cut elimination procedure. Namely, a cut on the original formula is retained in a first instance, with the height of the cut diminished, where height is defined as the sum of the maximal number of steps from the two premisses to topsequents. Gentzen defines a notion of altitude line (Höhenlinie) as the inference line of an instance of Cut such that all cuts below the one in question are on shorter cut formulas. The length of a cut formula is called its grade. Gentzen defines a tedious process that introduces new cuts. Here is Gentzen’s example:
The transformed derivation is, disregarding rules of exchange in the original (Neu, p. 35):
Gentzen indicates only in the text but not in the figure that altitude lines with a lowered altitude
$< \varrho $
appear higher up in the transformed derivation, above the sequents
$\Gamma _3 \rightarrow \Theta _3,F(n)$
and
$F(n),\Gamma _3 \rightarrow \Theta _3$
.Footnote
7
On the whole, the idea is that altitude lines are being pushed up in the endpiece. The last cut, with the empty endsequent as a conclusion, has altitude 0, and the transformations force this to be the case for the whole endpiece, by which there is no derivation of the empty sequent.
One may wonder why Gentzen seems to make things worse by introducing cut formulas through thinning. Here is what he writes (Neu, p. 34):
The inference figures represent an introduction and an elimination of
$\forall $
in
$\forall xF(x)$
. Following the original basic idea, both should be put aside and
$\forall xF(x)$
should be substituted by
$F(n)$
– its grade is one less; in place of the cut with the cut formula
$\forall xF(x)$
there would occur a cut with the cut formula
$F(n)$
. There appears, however, the difficulty already mentioned, namely that the formula
$\forall xF(x)$
can have been used and even introduced in several places.
If the cut formula occurred “in several places,” there must have been contractions before the cut that reduced their number to one. The case in which a premiss of cut is derived by contraction is precisely the difficulty that Gentzen met in 1933, one that made him use the mix rule there. How this phenomenon arises in the context of Neu is illustrated by the following example:
A standard permutation of Cut would be to take, say, its left premiss and a cut with the premiss of LC, followed by a second cut with the same left premiss and the conclusion of the first cut:
The trouble with this simple-minded idea is that the lower cut thus produced is not reduced in any way as compared to the original cut. It has three instances of logical rules as compared to the two before the transformation. The derivation is instead transformed as follows (Negri and von Plato Reference Negri, von Plato, Probst and Schuster2016, p. 283):
Gentzen notes that the essential point of the above transformation is that above the two new cuts on the old cut formula, the inferences have been simplified because one step of logical inference has been removed above each of the new cuts.
The elaboration of Gentzen’s procedure suggests a reconstruction of what likely was his original proof of cut elimination when he invented sequent calculus in 1933, as detailed out in Negri and von Plato (Reference Negri, von Plato, Probst and Schuster2016). He changed that proof, as he writes in the published thesis, for “ease of presentation.”
3 Three kinds of sequent calculi
In Gentzen’s summary of calculi and reductions for consistency proofs, dated August 1944, the main calculus used is called the U-calculus, where U stands for Umkehrung, inversion. Other calculi are the intuitionistic sequent calculus LI Footnote 8 of the doctoral thesis, and the calculus LIG in which half of the logical rules are replaced by logical groundsequents.
WKRd as well as the series WA and BTIZ contain many forms of the cut rule. A summary of the calculi and types of cut will be useful for the reading of WKRd. Gentzen divided sequent calculi into three forms:
1. The calculi LI and LK of the doctoral thesis of 1933 that have left and right rules for the connectives and quantifiers.
2. The groundsequent calculi LIG and LKG that have rules for one side and logical groundsequents for the other. The groundsquents for LIG are
$\hskip 15pt GS1: A\,\&\,B \rightarrow A\ \hskip 25pt GS2: A\,\&\,B \rightarrow B$
$\hskip 15pt GS3: A\rightarrow A\lor B\ \hskip 25pt GS4: B\rightarrow A\lor B$
$\hskip 15pt GS5: \forall xA(x) \rightarrow A(t)\ \hskip 5pt GS6: A(t) \rightarrow \exists xA(x)$
$\hskip 15pt GS7: \neg A,A \rightarrow \ \ \hskip 30pt GS8: A\supset B, B \rightarrow B. $
The rules of LI and LK are derivable by cuts on groundsequents, for example:
Gentzen began with the groundsequent calculi in the spring of 1933, then came soon to the calculi that have just rules. The groundsequent calculus LIG is clearly explained in Gentzen’s doctoral thesis with the above list of groundsequents
$GS1$
to
$GS8$
presented in connection with the translation of derivations from sequent calculus to axiomatic logic (pp. 424–425). These calculi are discussed in detail in Bernays’ Reference Bernays1965 article Betrachtungen zum Sequenzen-Kalkul. There is no full cut elimination for groundsequent calculi, but cuts in which both premisses are groundsequents remain. In these cases, the cut formula is always a subformula of the conclusion of cut. A detailed treatment is found in section 12 of von Plato (Reference von Plato2012).
3. The calculi LIU and LKU with invertible rules, briefly, U-calculi. Calculi with inverted rules are found right at the beginning of Gentzen’s setting up of sequent calculus, in the spring of 1933 (see von Plato Reference von Plato2017, p. 176 for this). Invertibility of a logical rule in LIG and LKG typically follows by cut. Here is an example of rule
$R\supset $
:
This example is characteristic: The inverse of a right rule is derived by the corresponding left rule, with premisses initial sequents and a cut on the principal formula after the rule, and similarly for the inverses of left rules. The calculi LI and LK are not optimal in respect of invertibility, in contrast to Ketonen’s calculus, but they suffice for Gentzen’s aims.
In WKRd, only universal quantification and implication are treated by the above method, in a single-succedent intuitionistic formulation with the U-rules:
Here, ABU and FBU stand for something like All-Beseitung-Umkehrung and Folge-Beseitigung-Umkehrung, respectively.
As with the groundsequent calculi, the rules of LI and LK follow by cuts in the U-calculi, for example, the conclusion of Gentzen’s rule
$L\supset $
of LI follows from its premisses
$\Gamma \rightarrow A$
and
$B,\Delta \rightarrow C$
as in:
In LI and LK, there is for each connective and quantifier a side on which an invertible rule is found. Gentzen had not realized that a variant of LK is possible in which all propositional rules are invertible, as in Ketonen’s thesis (1944). Had it been otherwise, signs of this most remarkable discovery could be seen in Gentzen’s notes, the present WKRd in particular. On the other hand, Gentzen knew that if implication is left out, a sequent calculus for classical propositional logic can be given with just the above six propositional groundsequents, the rule of cut, and the added groundsequents (as detailed out in von Plato Reference von Plato2012, section 11):
$A,B \rightarrow A\,\&\,B \hskip 15pt A\lor B \rightarrow A,B\hskip 15pt \rightarrow A,\neg A.$
Interpretation of LIG and LIU in LI: Gentzen’s groundsequents are derivable in LI by single rule instances in which the premisses are initial sequents:
Interpretation of LIG in
LI+Cut
: Derivations in LIG are special cases of LI-derivations with cuts in which the premisses of rules
$L\&, R\lor , L\supset , L\neg , L\forall ,$
and
$R\exists $
are initial sequents.
In cut elimination in LIG, it eventually happens that cut hits a groundsequent, as in:
If
$A\,\&\,B$
is not principal in the left premiss, cut is permuted up. The only new case now is that both premisses in cut are groundsequents, as in
It is clear enough that the subformula property is maintained in cuts that have groundsequents in both premisses.
The remaining case of cut elimination is that
$A\,\&\,B$
is principal in the left premiss, with the derivation:
A loop is produced. The same pattern repeats itself with the other connectives and quantifiers.
When the procedure of derivation of groundsequents is applied to the rest of the rules of LI, the result is
The groundsequent that corresponds to rule
$R\&$
has independent contexts, and the same for rule
$L\lor $
that has even a multiple succedent. For
$R\supset $
, a degenerate case is produced, and for
$R\neg $
, a groundsequent that gives classical logic. With
$\supset $
left out, the above-mentioned classical propositional calculus with just groundsequents and cuts is obtained, the completeness proof of which is an easy exercise (as in von Plato Reference von Plato2012, sec. 11).
There are no groundsquents that would correspond to rules
$R\forall $
and
$L\exists $
, for the derivations are blocked by the eigenvariable conditions.
Interpretation of LIU in
LI+Cut
: As can be seen from the example with rule
$R\supset $
, invertibility follows by a cut with a groundsequent as the other premiss. Thus, the above interpretation of derivations of LIG in LI extends even to derivations in LIU.
There remains the question why the calculi LIG and LIU were considered at all, if they are such easy variants of LI. The answer can be read from page 2 of WKRd: “The multiplications should belong to the permutations, not to the reductions of connectives and quantifiers.” A main problem in cut elimination was met in the case in which the right premiss of cut is derived by a contraction, as in:
Two successive cuts of D in the premiss of rule Ctr do not necessarily reduce the derivation.
In Gentzen’s thesis, the problem with contraction is circumvented by the “mix rule” by which any number of copies of the cut formula can be deleted in one step. Other solutions are possible: It is very likely that Gentzen’s original cut elimination proof used a method by which the original cut formula is first maintained, with cut permuted up in at least one premiss, followed by cuts on its immediate subformulas, as detailed out in Negri and von Plato (Reference Negri, von Plato, Probst and Schuster2016). This solution does not follow Gentzen’s dictum of keeping the multiplicity of formulas apart from the logical rules. Here is a typical case of contraction followed by cut:
The premiss of contraction arises from the presence of the principal formula of rule
$L\&$
in its premiss. The proof transformation, as in Negri and von Plato (Reference Negri, von Plato, Probst and Schuster2016), is into:
Ctr
$^*$
indicates possible repeated contractions. The upper cut has a lesser sum of heights of derivation of the premisses, as the instance of
$L\&$
has vanished, and the lower one is on a shorter cut formula. With groundsequents, it happens that the cut formula is never principal in both premisses of cut, and the above situation does not arise.
4 Types of cuts
Gentzen found the rule of cut from the papers of Paul Hertz on “sentence systems” of the 1920s, the topic of his first paper of 1932. Hertz had a rule he called “syllogism” in which there was, displayed as a stack, a number k of sequents of the form
$a_{i_1},\dots ,a_{i_n} \rightarrow b_i$
as left premisses, and a right premiss of the form
$b_1,\dots ,b_k,c_1,\dots ,c_m \rightarrow d$
. In a syllogism, all of the
$b_i$
were cut in one step, to obtain the conclusion:
$$ \begin{align*}a_{1_1},\dots,a_{1_n},\dots,a_{k_1},\dots,a_{k_n},c_1,\dots,c_m \rightarrow d.\end{align*} $$
Gentzen in his paper used the special case of
$k=1$
and the two-dimensional form of inference rule:
The rule of Hertz can be reproduced by k successive cuts.
The rule of cut appears in Gentzen’s notes of the spring of 1933 in the same form as in the 1932 article. As mentioned, the published thesis gave a proof of cut elimination through the use of a form of cut Gentzen called Mischung, literally mixing, in which any number of cut formulas can be deleted from the right premiss:
In the series WA, three types of cut are distinguished (p. 128):
1. Critical cut:
$\displaystyle {\frac {\rightarrow D \hskip 10pt D\rightarrow E}{\rightarrow E}}$
2. Multiplicative cut:
$\displaystyle {\frac {C\rightarrow D \hskip 10pt D\rightarrow E}{C\rightarrow E}}$
3. Additive cut:
$\displaystyle {\frac {B, (C)\rightarrow D \hskip 10pt B, D\rightarrow E}{B, (C)\rightarrow E}}$
The notation
$(C)$
in the additive type of cut indicates a possible occurrence of formula C. This cut includes a contraction on formula B.
In WKRd, contexts in the different types of cut are written out:
Cut:
$\displaystyle {\frac {\textstyle \Gamma \rightarrow D \quad D\, \Delta \rightarrow C}{\textstyle \Gamma \, \Delta \rightarrow C}}$
Critical cut:
$\displaystyle {\frac {\textstyle \rightarrow D \quad D\, \Delta \rightarrow C}{\textstyle \Delta \rightarrow C}}$
(
$\Delta $
empty: genuinely critical cut)
Chain cut:
$\displaystyle {\frac {\textstyle \Gamma \rightarrow D \quad D\, \Delta \rightarrow C}{\textstyle \Gamma \, \Delta \rightarrow C}}$
(
$\Gamma $
not empty)
Contractive cut:
$\displaystyle {\frac {\textstyle \Gamma \, \Theta \rightarrow D \quad D\, \Delta \, \Theta \rightarrow C}{\textstyle \Gamma \, \Delta \, \Theta \rightarrow C}}$
The last one is further called a “general cut” (allgemeiner Schnitt), as it contains the rest as special cases, with the contexts in the two premisses divided into a shared contractive part
$\Theta $
and additive parts
$\Gamma ,\Delta $
. Later in WKRd, Gentzen uses a “bra-ket” notation for a cut in which the antecedent is contracted:
Of the structural rules, exchange is dispensed with through the principle that “all schemes are meant so that the antecedent formulas can be understood as having been written down in an arbitrary order.” The formal notation is
$[\,\Gamma ,\Delta \,] \rightarrow C$
.
Gentzen’s Reference Kalmár1938 proof of the consistency of arithmetic introduces the mentioned Höhenlinie, altitude line, an inference line of a cut such that, from that cut to the endsequent of a derivation, all cuts are on shorter formulas. In WKRd as well as in WA and BTIZ, a related proof transformation is found, called Höhenschichtung,” altitude layering: Cuts in a derivation are permuted so that for any given cut, there are no cuts on longer formulas below that cut. In this connection, Gentzen introduces a type of cut that is like Hertz’ syllogism but without the stacking of left premisses, called Sammelschnitt, collective cut:
The aim with a collective cut is to get rid of the arbitrariness in the order of successive cuts with two premisses.
It seems that none of Gentzen’s attempts at getting, by some variant of cut, the multiplication of formulas in derivations under control, led to any definitive result. Forms of cut other than the standard one can lead to situations in which the cuts cannot be permuted with respect to each other. This is especially the case for Gentzen’s mix rule that contains an implicit contraction.
5 Gentzen’s summary of WA
The mentioned summary WAdd of WA covers the last 80-odd pages of the series WA, from page 255 to 339. It begins with some general remarks on Gentzen’s consistency program that are for the most part understandable, reproduced below. The rest is, as mentioned, quite cryptic but likely to make sense once the whole of the extant WA series gets transcribed and studied.
The summary WAdd begins with a note by which the shorthand pages were transcribed by “H. Kneser and H. Urban,” the former Gentzen’s mathematics professor Hellmuth Kneser at Greifswald where he began his mathematics studies in 1928.Footnote 9
WAdd 1
II.45 From WA the most modern part. Contents.
Basic ideas of the procedure: (1) Hilbert’s thought of the givenness of formal objects through exposition in concrete intuition (proof figures). (2) The enumerability of proof figures and of all objects of proof theory, by which the non-enumerable, of which the proofs deal, is seen to be only apparent in a certain sense. (Skolem’s theorem in this in a somewhat different sense.) (3) The reducibility of the logically compound, my idea of departure. Positive logic. (4) Yet to be worked through clearly: The assignment of great numbers to the 0-grade equations, i.e.: the number of elementary inferences among all reducible logical compositions all the way through. The accidental character of the whole assignment of values [Wertung, the value of the ordinal of a derivation under a given assignment of ordinals] must find its expression, especially the necessity of ever steeper functions. Here, in fact, the functional connections are rendered presentable in an equation, through logical compositions as a means of putting-together. Further, for the presentation of these things, one has to work clearly through the necessity of distancing oneself in a very precise sense, because of (4), from the simplicity (1) envisaged by Hilbert, as is dictated by the “great numbers.”
The difficulties of the procedure are three-fold: (1) The real ones, that the [?] there is; of - - further non-constructive. Hereto essentially (2) the extraordinary steepness (height) of the inferential increase, (3) the extraordinary breadth and multiplicity of combinations of inferences and the extension at the same time in two dimensions. – There is in the higher forms of inference anyway the possibility to surpass the previously given ones. What is this? It is not only the introduction of new and more complex
WAdd 2
concepts. These make naturally possible new theorems and proofs about the new concepts. The new concepts, though, stand in reality in the closest connection to the old ones, generalizations [Sammelbegriffe] of them, say. Therefore, they make it possible to prove the next-to-higher about the old objects [Gegenstandsmaterial]. What is the next-to-higher? The diagonal procedure shows it. ! E.g. in the formation of ever steeper functions, new objects [Material] are given over and over again. What there is to prove here is a particular question. (Computability of functions, or VI [complete induction] valid, or similar.)
6 Concluding remarks
A close look at Gentzen’s work brings to the surface a variety of sequent calculi. Next to the calculi LK and LI of his doctoral thesis that have been canonized in later literature, the thesis already clearly contains the groundsequent calculi LIG and LKG, the only thing missing being names for them. Moreover, the section on decidability of intuitionistic propositional logic in fact contains a calculus in which all multiplications of formulas produced in the conclusions of rule instances are contracted at once when writing the conclusions. All this is made explicit in Negri and von Plato (Reference Negri, von Plato, Probst and Schuster2016). The 1944 overview, with its multitude of calculi and reductions, clearly shows Gentzen’s flexibility with such choices of formal details – incidentally quite a contrast to many a later author on proof theory.
Many of the concepts used by Gentzen in his 1944 overview of calculi and reductions in proofs of consistency can be found in his cut elimination procedure of the 1938 proof of the consistency of arithmetic, but the calculi in WKRd, beyond the familiar LK, and many of the methods, are new to us. Concerning the concepts, I have collected in the end of my English rendering of Gentzen’s WKRd a glossary of the English terms used in the translation, with the German originals set next to these terms.
In his published work, Gentzen had fine-tuned the formal details of his calculi, to achieve the results he wanted, and later research has found nothing to correct there. My hope, having gone through Gentzen’s preserved shorthand manuscript, is that his overview of different sequent calculi and cut elimination procedures for them will spark new ideas and results in proof-theoretical research.
Ideas there are, indeed, in Gentzen’s shorthand manuscripts; a striking example is given by the very first preserved page of WA, numbered 77: Gentzen gives there a natural deduction system for arithmetic, and he assigns ordinal functions to formulas in derivations in the system. In implication introduction, a variable term of the functional hierarchy is assigned to the assumption A and a formula B with some term assignment is derived that depends on the term of the assumption. The step of implication introduction carries with itself the lambda abstract of the term for B, with abstraction over the variable for A. Implication elimination, then, consists of the corresponding functional application. Gentzen’s idea with this work was that steps of normalization in a derivation should lower the ordinal function assignment, under a suitably defined measure for such. The terms are written in blue pencil to the left of the formulas, and Gentzen is very clear in his reading, namely that the formulas are read as types. This reading is even more evident when Gentzen poses the requirement that the variable that is assigned to a formula that is being assumed in a derivation be of the appropriate functional form. If, say, an implication is assumed, the term assigned has to be of the right functional type; a typed lambda calculus to accompany derivations in natural deduction, drawn out of the blue it seems, and with the same idea as one finds hidden under Howard’s Reference Gentzen and Szabo1969 pioneering article The formulae-as-types notion of construction, originally carried through in sequent calculus, but by a suggestion of Martin-Löf’s, applying as well, and even better, to natural deduction (Howard Reference Howard1969, p. 484).
Appendix
Consistency: calculi, and reductions, overview, VIII.44
G. GentzenFootnote 10
Consistency, calculi, and reductions, overview.
WKRd 1
$\fbox{Taken VIII.44.}$
Limitation to: single-succedent sequents, positive logic, the connectives
$\forall $
and
$\supset $
(together or separately).
The calculus.
(1) Structural and groundsequents and inferences:
T
Footnote
11
$\mathfrak D \rightarrow \mathfrak D$
Thinning
$\frac {\textstyle \Gamma \rightarrow \mathfrak C}{\textstyle \mathfrak D \,\Gamma \rightarrow \mathfrak C}$
Contraction, exchange as known.
Cut
$\frac {\textstyle \Gamma \rightarrow \mathfrak D \quad \mathfrak D\, \Delta \rightarrow \mathfrak C}{\textstyle \Gamma \, \Delta \rightarrow \mathfrak C}$
Special types of cuts:
$\frac {\textstyle \rightarrow \mathfrak D \quad \mathfrak D\, \Delta \rightarrow \mathfrak C}{\textstyle \Delta \rightarrow \mathfrak C}$
“critical cut” (
$\Delta $
empty: properly critical cut)
$\frac {\textstyle \Gamma \rightarrow \mathfrak D \quad \mathfrak D\, \Delta \rightarrow \mathfrak C}{\textstyle \Gamma \, \Delta \rightarrow \mathfrak C}$
$\Gamma $
not empty: chain cut.
(These formulations remain valid when
$\supset $
is equated with
$\rightarrow $
)
Formulation without contraction, with a contractive cut:
$\frac {\textstyle \Gamma \, \Theta \rightarrow \mathfrak D \quad \mathfrak D\, \Delta \, \Theta \rightarrow \mathfrak C}{\textstyle \Gamma \, \Delta \, \Theta \rightarrow \mathfrak C}$
(Exchanges can be represented through these, at least in LIG without any further changes.)
Formulation without exchange: All schemes, also the ones that follow, intended so that the antecedent formulas can be thought written in an arbitrary order. The contractive cut thus intended is called a “general cut.” (Calculus without exchange and contraction.)
(2) Connective-groundsequents and inferences.Footnote 12
$AI\colon \hskip 5pt \frac {\textstyle \Gamma \rightarrow \mathfrak F \, \mathfrak a} {\textstyle \Gamma \rightarrow \forall {\scriptstyle \mathfrak X}\mathfrak F \, {\scriptstyle \mathfrak X}}$
(for object or property variables)Footnote
13
$FI\colon \hskip 5pt \frac {\textstyle \Gamma \, \mathfrak A \rightarrow \mathfrak B} {\textstyle \Gamma \rightarrow \mathfrak A\supset \mathfrak B}$
AE and FE, different formulations:
(a) Groundsequent AEG
$\forall {\scriptstyle \mathfrak X} \mathfrak F {\scriptstyle \mathfrak X} \rightarrow F\mathfrak t$
, FEG
$\mathfrak A \supset \mathfrak B, \mathfrak A \rightarrow \mathfrak B$
“calculus LIG”
(b) LI-formulation as in the thesis. Calculus LI.
(c) U-formulation: AEU:
$\frac {\textstyle \Gamma \rightarrow \forall {\scriptstyle \mathfrak X}\mathfrak F \, {\scriptstyle \mathfrak X}} {\textstyle \Gamma \rightarrow \mathfrak F \, \mathfrak t}$
FEU
$\frac {\textstyle \Gamma \rightarrow \mathfrak A \supset \mathfrak B} {\textstyle \Gamma \,\mathfrak A \rightarrow \mathfrak B}$
(calculus LIU)
(d) NLI-formulation as in the consistency paper.Footnote 14
AE for object variables is OAE, for predicate variables PAE. (
$\mathfrak t$
is then a big predicate)
(3) Mathematical groundsequents and inferences.
Mathematical groundsequents: Without
$\forall $
and without P variables, is correct under each substitution.
(Other formulations:
$\rightarrow \mathfrak A {\scriptstyle \mathfrak X}$
is not convenient, because it would go over to the open in reductions.Footnote
15
A formulation without each connective would, naturally, not suffice with single-succedent sequents.)
REND is NNB
Footnote
16
for propositions without
$\forall \, \exists $
, they are contained, formulated with
$\supset $
. (Note well: If
$\supset _{_\xi }$
is the only connective, I should allow these here, i.e.,Footnote
17
$\underline {\forall }$
.)
VI. VIG:
Footnote
18
$\forall {\scriptstyle \mathfrak X} (\mathfrak F\,{\scriptstyle \mathfrak X} \supset \mathfrak F\, {\scriptstyle \mathfrak X} ') \rightarrow \mathfrak F\,1\supset \mathfrak F\,\mathfrak t$
$\mathfrak t$
an arbitrary term
Nat-formulation:Footnote
19
The same with the antecedent formula Nat
$\mathfrak t $
added.
Derivation GG [object-groundsequent]
$\mathfrak s= \mathfrak t, \mathfrak F(\mathfrak s) \rightarrow \mathfrak F(\mathfrak t)$
To 1) the Heyting-inference:
First possibility: to allow here an empty succedent and thinning.
Second possibility:
$1=\stackrel {\textstyle H}{\textstyle 2} \rightarrow \mathfrak D$
as a groundsequent-scheme, e.g.,
$\frac {\textstyle \Gamma \rightarrow 1=2}{\textstyle \Gamma \rightarrow \mathfrak D}$
The concept of an endpiece. Backwards from the endsequent up to the first inference line of AI oder FI. (Or VI inference). This formulation holds for LIU, NLI, LIG. (For LI otherwise, as there.)
We have for LIG and LI: The endpiece contains, of the inferences, the structural inferences.Footnote 20
2
The U-calculus.
Inferences of the connectives: AI FI AEU FEU,
Structural: T and H. Thinning:
$\frac {\textstyle \rightarrow \mathfrak C}{\textstyle \mathfrak D \rightarrow \mathfrak C}$
Contraction:
$\frac {\textstyle \mathfrak D \, \mathfrak D \rightarrow \mathfrak C}{\textstyle \mathfrak D \rightarrow \mathfrak C}$
Exchange:
$\frac {\textstyle \Gamma \,\mathfrak D \, \mathfrak E \rightarrow \mathfrak C}{\textstyle \Gamma \,\mathfrak E \,\mathfrak D \rightarrow \mathfrak C}$
Chain cut:
$\frac {\textstyle \Gamma \rightarrow \mathfrak D \quad \mathfrak D \rightarrow \mathfrak C}{\textstyle \Gamma \rightarrow \mathfrak C}$
$\Gamma $
not empty.
Critical cut:
$\frac {\textstyle \rightarrow \mathfrak D \quad \mathfrak D\, \Delta \rightarrow \mathfrak C}{\textstyle \Delta \rightarrow \mathfrak C}$
(
$\Delta $
could be avoided, but there is then a lack of freedom of movement with the permutations.)
Mathematical groundsequents as above.
(Contraction-cut instead of contraction would not go just like that, for we have, as an example, that a contractible sequent can arise from a groundsequent by FEU)
The endpiece contains as inferences structural ones, as well as AEU, FEU. (It must not be assumed that critical cuts be restricted to just those on the endpiece.)
The reductions.
§1. The permutative reductions.
1.1. The forms of transformation of an endpiece (e.g., of the derivation as a whole) Calculus LIG in general.
The permutative reductions are modifications of the sequential composition of the natural image of a derivation,Footnote 21 so not any “reductions” proper. That means: preservation of value under a precise valuation. Their main aim seems to be to single out a connective-peak.Footnote 22 The multiplications should concern the permutations, not the connective-reductions. This was deferred to a specific ordering of the endpiece. The properties of this ordering come as simple additional conditions for the singling out of peaks
For the second, the following requirements, for example, are sufficient:
First possibility: Natural tree form, that is to say in the L-calculus: No thinning, T, contraction in the endpiece; this will not suffice for the
$\supset $
reduction in LIG, the following is rather to be required in addition: A cut on
$\mathfrak A\supset \mathfrak B $
must immediately follow FEG.
Second possibility: No thinnings nor T, as well as altitude layering, i.e., there must stand above a cut no cut with a lower grade (always in the endpiece). For the calculus LIG.
The first possibility is essentially satisfied by: “
$\rightarrow \mathfrak D$
normal form” of the endpiece, i.e., the critical cuts in this.
The forms of order of the endpiece.
First kind:
$\rightarrow \mathfrak D$
normal form. Can be produced from the natural image, forming only critical cuts from top down. (Put together from the [?] indirect parts of two.)
Second kind: “altitude ordering.” Starting from the natural image, one connects by cuts, overall by the strongest binding grade, three [?].
With both kinds, arbitrariness in the order of the cuts can be lifted by the use collective cuts:
First kind: Critical collective cut:
Second kind: Collective cut with cut formulas of the same grade throughout. Note well: If with the altitude ordering one wants to keep contractions, one gives as a collective cut, as fits the purpose, a system of cuts, contractions, and exchanges, with all the cuts of the same grade.
(Another kind of form of order is the cut-free natural ancestral tree form. Great disadvantage: reduction into indirect parts necessary.)Footnote 23
(In the U-calculus, one departs similarly from the strict separation of the open land and reduces into the indirect one.)
Third kind of form of order, combinable: altitude permutation is quasi
$\rightarrow \mathfrak D$
-normalization in each single layer. Say, sometimes critical collective cuts by formulas of a lower grade, that is, quasi critical.
3
Main advantage of the “
$\rightarrow \mathfrak D$
permutations.” Each structural inference is completely reduced once; for example, apparently simplified through a single cut. For a small [?] Advantage of the altitude layering permutations: The multiplications are coupled withFootnote
24
a permutation procedure through an entire altitude layer, advantageous functional conditions.
Altitude layering does not seem to be possible for Analysis, because the grades go in circles.
1.2. The
$\rightarrow \mathfrak D$
-shifts. For LIG and LI
A formulation with critical collective cuts.
Order land from the endsequent through all of the critical collective cuts that connect to each other. Collective cuts are allowed here.
The place of permutation. Where an uppermost sequent of the order land, namely the main (= proper) upper sequent similar to a
$\cap $
collective cut, is the lower sequent of a structural inference.Footnote
25
Claim: There is always, except for the endpiece as a whole, = order land.Footnote 26 Proof easy.
The permutations.
Thinning:
Contraction:
Exchange clearly analogous
$R1c$
Cut:
Here in general [?] two collective cuts after the reduction.
$\Delta $
empty nothing special.
$\Gamma $
and
$\Delta $
empty not possible.
$\Gamma $
empty remarkable:
$R1d^*$
taking over a critical cut into the collective cut.
T and H reductions:
a contradictory derivation arises
$RH1$
Formulation for a calculus without exchange and contraction: (It is not to be recommended to make away with thinning in advance, by permuting it down.)
Reduction schemes: (The concept
$\cap $
collective cut and place of permutation unchanged [?])
Thinning
$R1a$
.
General cut:
$\Gamma $
not empty.
Here parts can get multiplied at left, where [?] in
$\langle \Gamma \,\Delta \rangle $
, formulas have been contracted that occur separately in
$\Gamma $
und
$\Delta $
.
Correspondingly for
$\Gamma $
empty:
$R1d^*$
(exactly as above).
In addition T- and H-reductions as before.
4
Formulation with critical single cuts.
Order land: Up to the inference line without an inference that is not a
$\cap $
-cut. (
$\cap $
-cut has to be allowed also elsewhere.)
Place of shift: An uppermost sequent of the order land is a right upper sequent of the
$\cap $
-cut and lower sequent of a structural inference (not
$\cap $
-cut). There is always one.
The permutations. So that I can permute above exchange,
$\cap $
-cut is to be formulated:
(I should permute
$\cap $
-cuts one above the other.)
Reduction steps: a) Thinning
$\qquad\qquad\qquad\qquad\qquad\qquad\qquad R2a1$
$\quad\quad\qquad\qquad\quad\qquad R2a2$
Contraction is analogous, with a duplication of the derivation of
$\rightarrow \mathfrak D$
in the first case.
Exhange trivial, analogous: Either the exchange disappears or it is permuted down.
Cut. This is by assumption not critical. Two different cases according to whether
$\mathfrak D$
belongs to
$\Gamma $
or to
$\Delta $
.
First case (left):
(To notice especially: when
$\Gamma $
empty, then also the new cut has become a
$\cap $
-cut.)
Second case (right) analogous. (Here
$\Gamma $
cannot be empty.)
Additional permutations of
$\cap $
-cuts over
$\cap $
-cuts: Requirements something like: Cuts of a higher grade not below ones of a lower grade (some similarity to altitude layering).Footnote
27
To achieve through additional [?]: permutation
[ ]: Arbitrary succession of the formulas in question.
Another possibility: Arbitrary such permutations are allowed, without conditions on grade. Then the above permutations can be simplified, with the first case, however, needed.Footnote 28
T and H reductions as above.
Formulation for the calculus without exchange and contraction:
Thinning: as above
$R2a1 \ R2a2$
.
1. General cut, worst case:
$\mathfrak D$
comes from both sides. After the reduction, two
$\cap $
-cuts above. The lower also
$\cap $
, when
$\Gamma $
empty.
Formulation for the same calculus, with arbitrary permutations of
$\cap $
-cuts over
$\cap $
-cuts (i.e., dependence of the valuation on the succession of critical single cuts in a sequent).
Reduction schemes:
$R2[e?]$
as well as:
$R2a1$
as well for [?] general cut. [?] leaves
$\cap $
-cuts to accumulate and permutes them one over the other in such a way that there are, first, all single cuts of the contracted part (
$\Theta $
) permuted above an arbitrary cut, then all single cuts of the part that comes from the left (
$\Gamma $
). What comes only from the right (
$\Delta $
), remains as it is. (“
$\Theta \,\Gamma $
-procedure.”)
WKRd 5
1.3. Permutative reductions of the second kind: The altitude layering permutations. Calculus LIG.
There is to be given in advance a concept of grade for formulas that need not be the usual one, in view of the special position of
$\supset $
(BTIZ),Footnote
29
a concept that needs to satisfy just: The grade of the principal formula in a logical inference must be greater than those of the active formulas.
(Not possible for Analysis, because a circle can enter with PAE Footnote 30 with this concept.)
Collective cuts are not appropriate; one gets all of their advantages also with single cuts suitably collected together. This gives a procedure with a total permutation. As opposed to this there is the one with single permutations.
Order land in the endpiece: Up to a cut with a grade lower than the one next below. Place of permutation: such a place. Trivially at hand.
The permutations.
(1) Formulation with total permutations. (Advantageous to have on the basis of the valuation: total altitude …)
A cut is permuted that forms a place for a permutation, downwards beyond a large system of inferences, until the next “altitude limit.”
Schemes as in Neu, like this:
$\qquad\qquad R3$
into
(A rather unclear process. Seen naturally,Footnote
31
everything that was connected to
$\mathfrak D$
up to arriving at
$\mathfrak E$
is left out. Leaving out of parts and addition of thinnings.)
One needs further also: Getting away with thinning as in Neu (an unclear process) as well as T and H-reductions:
Further, thinnings to be removed.
What seems like a more advantageous formulation of total permutation would be a simple collecting together of single cuts after 2.) (below), in the calculus without exchange and contraction. Here, cuts would have to be collected together that belong lower down in [?] a complete shoveling through of a cut with a lower grade, by an altitude layering downwards.
(2) Formulation with single permutations. (Clear process, but more difficult to capture each in isolation in terms of valuation.)
Place of permutation as above. Difficulty: A cut cannot be permuted down below a contraction. Remedy: Use of contractive cuts. The same holds for exchange, so that it, too, must go into the concept of cut.
Then: Structural inferences: Without exchanges and contractions, instead “general cut”:
Order of succession indifferent
A more convenient formulation:
Meaning: The formulas in
$\Gamma \,\Delta $
contracted throughout.
6
It is simplest to reduce the thinnings at once. Permuted down.
It means that the concept of order land is modified: There is, directly above the cut at the right or left, thinning or a cut of lower grade.
This is to say 4 steps of reduction:
A cut is permuted, each time, upwards, over a thinning or cut of a lower grade, to the left or right.
Thinning left.
Thinning right analogous.
$R4a1$
and
$R4a2$
Cut left: (grade
$\mathfrak B <$
grade
$\mathfrak D$
)
Cut right. Worst case:
$\mathfrak D$
comes from both upper sequents of the upper cut.
$\triangleright $
as the other reduction of cut …
$\triangleleft $
Footnote
32
As well as two easier cases. Analogous, then.
Elimination of the structural groundsequents in the endpiece.
$RT2, RT3$
, and for H essentially analogous to above.
Essential remark concerning ordering, for creating an ordering for all kinds of permutative reductions (even though less appropriate for
$\rightarrow \mathfrak D$
):
One can, within the calculus with thinning and general cut, apparently completely eliminate the thinnings as well as the T and H-groundsequents from the endpiece, by the schemes
$R4a1, 4a2, 4b, T2, T3, H4.1, H4.2.$
After these, one has only cuts.
1.4. The combined permutations. Advantage: altitude layering permutations, in which, however, arbitrary cuts are not permuted, but only the quasi-critical ones.
Calculus LIG without exchange and contraction, with “general cut.” Thinning and structural goundsequents eliminated in advance, by what was just said.
The endpiece, then, the cut that is still general. A single cut, not a collective one.
Place of permutation, three possibilities: The upper cut has a grade that is equal or greater, but it is not quasi-critical. Then it can stand only above at right. Moreover, it can possess only the same grade.
Or: The upper cut has a lower grade, right or left, then.
A quasi-critical cut is always permuted upwards over a cut.
Schemes: As
$R4d1, 4d2, 4d3. 4c$
. As well as
$R2f1, 2f2$
.
7
§2. The reductions for the connectives. For LIG.
2.1. Proof of existence of a peak. The conditions are: An endpiece that contains only structurality.
As well as no thinnings nor T or H.
As well as: The endpiece contains no signs for connectives. The endpiece contains no equations nor CI. As well as: The uppermost sequents of the endpiece that are sequents with connectives contain principal formulas. As well as (not necessary for an LI-like notion of a peak, by the following proof): FEG is to be immediately followed by a cut on
$\mathfrak A\supset \mathfrak B$
, AEG with one on
$\forall {\scriptstyle \mathfrak X} \mathfrak F {\scriptstyle \mathfrak X}$
.Footnote
33
Proof of existence of a peak as in Neu, then (topological).
2.2. How a peak with a connective looks like: The logical groundsequent of a peak stands directly or almost directly above the peak cut.
With
$\forall $
: AEG
(
$\Gamma $
empty with
$\rightarrow \mathfrak D$
-permutations.)
$\supset $
-peak, several cases.
For altitude layering permutations:
The FI somewhere above FEG
For
$\rightarrow \mathfrak D$
with single cuts: similarly,
$\Gamma $
empty.
For
$\rightarrow \mathfrak D$
permutations with collective cuts: either
Or: without
$\Gamma :$
Further as before.
In the formulation without additional ordering by grade between the
$\cap $
-cuts, the following is also possible: First a single cut on
$\mathfrak A$
in FEG, finally also by mathematical groundsequents. In place of FI a mathematical groundsequent, similarly in place of FEG possible (concerning
$\mathfrak A \supset \mathfrak B\rightarrow $
).
2.3 Reduction of a logical peak.Trivial by the above schemes.
8
§3. The local reductions for the U-calculus. Calculus, see above.
The order land in the endpiece: Consists of a single thread: By U-inferences (with
$\Gamma $
empty) as well as by critical cuts, proceeding to the right here.
Place of reduction: One comes to a groundsequent or an inference line with no other inferences.
If there is a U-inference under this, with
$\Gamma $
augmented, there is at hand a trivially reducible logical peak.
There remains one in which the place of reduction is the right upper sequent of a
$\cap $
-cut.
If it is the lower sequent of an inference, permutation is to above it.
Over logical inferences:
$AE\ FE$
$ABU\ FBU$
Footnote
34
Permutation into the indirect land! (Though not further in it.)
Above exchange, with
$\Gamma $
not empty: similarly.
Above thinning:
Over contraction clear, duplication above
$\rightarrow \mathfrak D $
.
Above chain cut:
into
$\Gamma $
possibly empty.
Above exchange with
$\Gamma $
empty. (The essential case in the valuation.)
There cannot follow any FEU or AEU with an empty
$\Gamma $
above
$\mathfrak D \rightarrow \mathfrak C$
, so just one further
$\cap $
-cut. (The endsequent must have no antecedent formula). This is taken over into the permutation: It is
Reductions for groundsequents: T Reduction =
$RT1$
.
$RH1$
. For the mathematical ones.
