Сколемовский метод в интуиционистских исчислениях

Изучается вопрос о допустимости устранения положительных кванторов с помощью функциональных символов в интуиционистском исчислении предикатов. С помощью синтаксических преобразований выводов в генценовских системах устанавливаются достаточные условия допустимости. Наиболее просто формулируемое условие: допустимо устранение положительного $\exists$-квантора, не находящегося в области действия $\supset$, $\neg$. Показано на примерах, что приведенный перечень допустимых правил в определенном смысле максимален. Отдельно рассмотрен вопрос о сохранении непротиворечивости при устранении положительных кванторов. Показано, что первая $\varepsilon$-теорема переносится на интуиционистское исчисление предикатов, а вторая – нет. Наконец, показано, что устранение положительных кванторов даже из предваренной формулы может перевести непротиворечивую интуиционистскую теорию с равенством в противоречивую. Существенным здесь оказывается требование экстенсиональности вводимого функционального символа: если его выполнение заранее обеспечено (как это имеет место при рассмотрении обычного метода исключения функциональных символов с помощью представляющих предикатов), то устранение квантора допустимо. Методы, разработанные при доказательстве основных результатов, позволяют указать специализацию формы вывода, с помощью которой легко доказывается устранимость структурных правил в генценовских исчислениях.
Библ. 7 назв.