| Abstract: | The strong normalization theorem asserts that any sequence of reductions (standard steps of cut elimination) stops at an object in normal form, i.e., at an object to which further reductions are inapplicable. The most intuitive proofs of strong normalization for various systems, including first- and second-order arithmetic, use, essentially, the concept of hereditary normalizability of an object. This concept, for objects of unbounded complexity, cannot be expressed in the language of arithmetic, so that the proofs mentioned leave its domain. Howard's proof for arithmetic, using nonunique assignment of ordinals, apparently, can be modified so as to get a primitive recursive proof of strict normalizability for the
-fragment of the intuitionistic predicate calculus, but the author of the present paper has not succeeded in overcoming the combinatorial difficulties. Our goal is to give an intuitive proof for the predicate calculus, from which one can extract a primitive recursive estimate of the number of reductions, and a proof in primitive recursive arithmetic of the fact that this estimate is proper. The proof of normalizability, that is, the construction of a special reduction sequence stopping at a normal term, is well known. In this sequence one first converts subterms of the highest levell, and first the innermost of them. (Corresponding to this, in the proof one can apply reduction with respect to level.) Here the number of convertible terms of maximal level, suitable for reduction, is lowered and the newly arising convertible terms have lower level.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 131–135, 1979. |
