О $E$-теоремах

Имеется [I] несколько методов построения по каждому доказательству $P$ суждения $\exists x A$ в гейтинговской (интуиционистской) арифметике [2] терма $t_p$, такого что $A[t_p]$ истинно (в том или ином смысле). Оказывается, что большинство из этих методов эквивалентны: соответствующие термы $t_p$ конвертируемы в одно и то же натуральное число. Это доказывается здесь для трех методов: (I) полного устранения сечения в бесконечных формулировках системы $HA$ [3], [4]; (II) рекурсивной реализуемости [2]; (III) частичного устранения сечения методом 2-го генценовского доказательства непротиворечивости [5], [6] или нормализации [7], [8]. Показано, что процесс устранения сечения по методу (I) ведет разве лишь к вычислению значений термов, связанных с данным доказательством по методам (II) и (III).