О допустимости правила маркова в интуиционистской теории множеств.

Abstract

Хорошо известно, что правило Маркова является допустимым в таких преди дативных теориях,как интуиционисткие арифметика и анализ [ 5 ]. Первые доказательства были достаточно сложными и использовали конструкции функционалов высоких типов или нормализацию выводов. В 1977 г. Х.Фридманом [3] (и, независимо, АДрагалиным в 1979 г. [1]) был предложен простой метод доказательства допустимости правила Маркова для предикативных теорий высокого порядка и даже для непредикативной теории множеств, но в последнем случае отсутствовали аксиома объемности, а также параметры по множествам. В настоящей работе доказывается допустимость сильного правила Маркова с параметрами по множествам (но без параметров по натуральным числам) для двусортной теории множеств, включающей все аксиомы стандартной теории множеств. К теории добавлен принцип существования двойного пополнения множеств, что делает эту теорию равнонепротиворечивой с классическим вариантом ZF [4]. Рассматриваемая теория обладает также свойствами дизъюнктивное™ и полной экзистенциальное™ [6;2].