RUS  ENG
Полная версия
ЖУРНАЛЫ // Записки научных семинаров ПОМИ // Архив

Зап. научн. сем. ЛОМИ, 1974, том 40, страницы 110–118 (Mi znsl2686)

О $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).

УДК: 51.01:164



Реферативные базы данных:


© МИАН, 2024