|
Труды ордена Ленина Математического института имени В. А. Стеклова, 1972, том 121, страницы 67–99
(Mi tm3112)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Сколемовский метод в интуиционистских исчислениях
Г. Е. Минц
Аннотация:
Изучается вопрос о допустимости устранения положительных кванторов с помощью
функциональных символов в интуиционистском исчислении предикатов. С помощью синтаксических
преобразований выводов в генценовских системах устанавливаются достаточные
условия допустимости. Наиболее просто формулируемое условие: допустимо устранение положительного
$\exists$-квантора, не находящегося в области действия $\supset$, $\neg$. Показано на примерах,
что приведенный перечень допустимых правил в определенном смысле максимален.
Отдельно рассмотрен вопрос о сохранении непротиворечивости при устранении положительных
кванторов. Показано, что первая $\varepsilon$-теорема переносится на интуиционистское исчисление
предикатов, а вторая – нет. Наконец, показано, что устранение положительных кванторов
даже из предваренной формулы может перевести непротиворечивую интуиционистскую теорию
с равенством в противоречивую. Существенным здесь оказывается требование экстенсиональности
вводимого функционального символа: если его выполнение заранее обеспечено
(как это имеет место при рассмотрении обычного метода исключения функциональных символов
с помощью представляющих предикатов), то устранение квантора допустимо. Методы,
разработанные при доказательстве основных результатов, позволяют указать специализацию формы вывода, с помощью которой легко доказывается устранимость структурных правил
в генценовских исчислениях.
Библ. 7 назв.
Образец цитирования:
Г. Е. Минц, “Сколемовский метод в интуиционистских исчислениях”, Логические и логико-математические исчисления. 2, Тр. МИАН СССР, 121, 1972, 67–99; Proc. Steklov Inst. Math., 121 (1972), 73–109
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tm3112 https://www.mathnet.ru/rus/tm/v121/p67
|
Статистика просмотров: |
Страница аннотации: | 227 | PDF полного текста: | 130 |
|