Concluding Remarks and Further Applications

Looking at the single detour conversion schemes in the proof of Theorem 1, we notice that simplification convertibility with disjunction in case 2.2 leaves two possible results of conversion. For the rest of detour conversions, the local transformations produce unique converted derivations, and that property is sufficient for the overall result: Bar induction is a principle by which such local control of a suitably chosen property is turned into global structure, one could put it.

There is at each stage of strong normalization a finite number of non-normalities from which to choose the conversion to be made. Therefore strong normalization is a consequence of the variety of bar induction known as the fan theorem. The consistency of arithmetic was originally proved by bar induction by Gentzen and soon replaced by a proof through transfinite induction (see von Plato 2015 [8], and Siders and von Plato (2015) [4] for an explicit formulation of Gentzen's bar induction). As with Gentzen's proof, also the present proof could be carried through by the use of transfinite ordinals. What the least ordinal needed is, is at present not known, but because the fan theorem suffices for the result, Gentzen's ε0 gives a strict upper bound.

The proofs of normalization and strong normalization through Hilfssätze should work without problems for classical natural deduction with the rule of indirect proof and the same definition of normality as above, as in von Plato and Siders (2012) [9].

The proofs can obviously be worked through also for standard natural deduction, along the lines of my paper (von Plato 2011 [6]).

Two more applications of explicit composition can be noted here:

1. The interpretation of arbitrary cuts in natural deduction: A comparison of natural deduction in sequent calculus style with sequent calculus proper shows that a non-normal instance of an E -rule corresponds exactly to the case of a cut in which the right premiss of cut has been derived by a corresponding left rule. In the translation from sequent derivations with cuts to natural deduction, such cuts turn into nonnormalities. The rest of the cuts are translated as explicit delayed compositions. What corresponds to cut elimination is seen from the admissibility of composition in natural deduction: An uppermost instance of Comp is permuted up until it either reaches an assumption and vanishes or hits a normal instance of an E -rule and gets turned into a non-normality. After the delayed compositions have been eliminated, there remain the proper non-normalitites and these can be eliminated in any order whatsoever. When in the normal derivation the major premisses are left unwritten, a sequent derivation is obtained. The overall procedure gives strong cut elimination in precisely the same sense in which there is strong normalization in natural deduction. Details are found in Sect. 13.4 of von Plato (2013) [7].

2. Normalization and strong normalization of λ-terms: Any proof of normal-

ization and strong normalization can be turned into a corresponding proof for typed λ-terms. The term structure is particularly transparent with general elimination rules, for the selector terms have now, with implication elimination as an example, the following structure (von Plato 2001 [5, p. 566]):

[x :. B]


c : A B a : A d : C

gap(c, a, (x )d) : C

A selector term is normal if its first argument is a variable, in particular, for the above “generalized application” as it is called in von Plato 2001 [5], the nested “tower” of applications, met with the standard application function, does not occur for normal terms. Permutative conversions reduce a suitably defined notion of depth of selector terms, and detour conversions reduce to substitutions. A Hilfssatz is used to prove that strong normalizability of λ-terms is maintained under such substitution.


1. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176– 210, 405–431 (1934–35)

2. Gentzen, G.: Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie. First published in Archiv für mathematische Logik 16(1974), 97–118 (1935)

3. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm (1965)

4. Siders, A., von Plato, J.: Bar induction in the proof of termination of Gentzen's reduction procedure. In: Kahle, R., Rathjen, M. (eds.) Gentzen's Centenary: The Quest of Consistency, pp. 127–130. Springer, New York (2015)

5. von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Log. 40, 541–567 (2001)

6. von Plato, J.: A sequent calculus isomorphic to Gentzen's natural deduction. Rev. Symb. Log.

4, 43–53 (2011)

7. von Plato, J.: Elements of Logical Reasoning. Cambridge University Press, Cambridge (2013)

8. von Plato, J.: From Hauptsatz to Hilfssatz. In: Kahle, R., Rathjen, M. (eds.) Gentzen's Centenary: The Quest of Consistency, pp. 89–126. Springer, New York (2015)

9. von Plato, J., Siders, A.: Normal derivability in classical natural deduction. Rev. Symb. Log. 5, 205–211 (2012)

< Prev   CONTENTS   Next >