Примитивно рекурсивная оценка сильной нормализации для исчисления предикатов

Теорема с сильной нормализацией утверждает, что любая последовательность редукций (стандартных шагов устранения сечения) обрывается на объекте в нормальной форме, т.е. на объекте, к которому дальнейшие редукции неприменимы. Наиболее наглядные доказательства сильной нормализации для различных систем, включая арифметику первого и второго порядка, используют, по существу, понятие наследственно нормализуемого объекта. Это понятие для объектов неограниченной сложности невыразимо в языке арифметики, так что упомянутые доказательства выходят за ее рамки. Доказательство Говарда для арифметики, использующее неоднозначное назначение ординалов, по-видимому, можно модифицировать таким образом, чтобы получить примитивно рекурсивное доказательство строгой нормализуемости для $(\forall,\supset)$-фрагмента интуиционистского исчисления предикатов, но автору настоящей статьи не удалось преодолеть комбинаторные трудности.
Наша цель – дать наглядное доказательство для исчисления предикатов, из которого извлекается примитивно рекурсивная оценка числа редукции, и доказательство в примитивно рекурсивной арифметике того факта, что эта оценка корректна.
Хорошо известно доказательство нормализуемости, то есть построение специальной редукционной последовательности, обрывающейся на нормальном терме. В этой последовательности сначала конвертируются подтермы наивысшего уровня $l$, причем сначала – самые внутренние из них. (Соответственно этому, в доказательстве применяется редукция по уровню). При этом количество конвертируемых термов максимального уровня, пригодных для редукции, уменьшается, а вновь возникающие конвертируемые термы имеют меньший уровень. Библ. – 2 назв.