A~primitive recursive bound of strong normalization for predicate calculus

G. E. Mints

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 131-136

Résumé

Strong normalization theorem asserts convergence of any reduction (cutelimination) sequence. Most popular strong normalisation proofs use hereditary normalizability which cannot be expressed by an arithmetic formula, thus the resulting proof for the intuitionistic predicate calculus is not formalizable in arithmetic. There is a hope to adapt Howard's proof [1] using nonunique ordinal assignments to obtain primitive recursive proof of strong normalizability for $(\supset,\forall$)-fragment of predicate calculus but the author of this paper was unable to overcome combinatorial difficulties. We obtain a primitive recursive bound for strong,normalization of $\lambda$-terms of finite types by reducing arbitrary reduction sequence to standard one (where innermost terms of maximal level are contracted first) and prove that the gain in the number of $s$ steps is not too big. Let $\nu(t)$ be the maximal length of reduction sequences for term $t$. First by recursion on $\omega^3$ we define function $\Psi$ estimating $\nu(t)$ in terms of $\nu(t')$ for $t\vdash t'$. Recursion on $\omega$ is known to be reducible to several ($\leq6$) primitive recursions. This allows us to define $\nu(t)$ in terms of $\nu(t')$, where $t\vdash t'$, by conversion of an innermost-subterm of the maximal level. In this way $\nu$ is defined from $\Psi$ by recursions. One cannot use less than 4 recursions for $\nu$ in veiw of Statman's lower bound (cf. also Orevkov's paper in this volume, cf. [3]) for normalization. It is to be seen what is exact bound for strong normalization.