Введение к работе
Актуальность теш. Тема настоящей работы относится к применению теоретико-модельных методов в теории интуиционистских доказательств на материале некоторых теорем классической алгебры. Исследуется традиционная проблема перехода от выводимости некоторого суждения S в классической теории к выводимости самого суждения S или нового сувдения S'(близкого по смыслу к S) в соответствующей интуиционистской теории. В качестве таких теорий рассматриваются классическая и соответственно интуиционистская теории множеств.
Около 1930 г. А.Н.Колмогоров и К.Гедель решили эту проблему для исчисления предикатов. Предложенный ими негативный перевод Si—S' формул S обычного исчисления предикатов в формулы S' того же исчисления состоит в том, что в определенных местах формулы S нужно добавить связки -п. Тогда, если ь- 5, то 1ь— S', где к- обозначает вывод в классическом исчислении предикатов, a It— обозначает-вывод в соответствующем интуиционистском исчислении предикатов. Затем аналогичные исследования проводились для теории типов (Д.Майхилл, 1974г.) и теории множеств Цермело-Френкеля (Х.Фридмая,1973г.; В.Пауэлл,1975г.)
Значение этих результатов общеизвестно. "Но их особенностью является то, что формула 5' существенно отличается от исходной формулы S. Кроме того, одно из принципиальных достоинств интуиционистской теории состоит в свойстве экзистенциа-льности: если It—3xQS(xQ), то можно предъявить терм tQ, индивидуально описывающий соответствующее xQ (так, что її—S(tQ)). Теперь і— и її— обозначают соответственно классическую и интуиционистскую выводимости в теории множеств или теории типов. Оно "теряется", когда речь идет об интуиционистской доказуемости формулы типа -n3xQS{xQ); в этом случае, вообще говоря, нет возможности предъявить соответствующий терм для XQ.
Поэтому появились исследования, в рамках которых пытаются не изменять или почти не изменять вид формулы S при переходе от классической выводимости к- s к соответствующей интуиционистской выводимости її— S', и, во всяком случае, не добавлять в формулу S двойные отрицания. Для арифметики такой под-
ход реализуется в работе Х.Фридмана ([4]). Для теории множеств Цермело-Френкеля он был реализован сначала только для АЕ-арифметических формул Х.Фридааном (U1), а затем в методе, предложенном В.А.Любецким ([5,61) и Г.Такеути-С.Титани ([11,121) .
Цель работы. Получен перевод S*-*S.' формул языка 1-колец, для которого выводимость исходной формулы S в классической теории множеств влечет выводимость ее перевода S' в интуиционистской теории множеств. Этот перевод не связан с добавлением двойных отрицаний или релятивизацией исходной формулы S к специальному универсуму. К 5' применима теорема об эффективности дизъюнкции и квантора существования. Получен также класс формул в языке l-колец,.для которого классическая и интуиционистская выводимости в теории множеств совпадают.
Получены интуиционистские в смысле интуиционистской выводимости (глава 1) или в смысле общезначимости (главы 2,3) варианты ряда хорошо известных в классической алгебре теорем: о свойствах полей разложения, Гильберта и Ритта о нулях систем многочленов, Вейерштрасса о корнях многочлена , о положительном решении 17-ой проблемы Гильберта.
Методика исследований. Все результаты диссертации получены с помощью единого метода, развивающего работы В.А.Любец-кого ([5-9]), Г.Такеути и Г.Титани ([10-121). Суть этого метода состоит в семантическом оценивании формул элементами специально подбираемых булевых и гейтинговых алгебр.
Научная новизна. Все результаты диссертации являются новыми и снабжены подробными доказательствами.
Теоретическая и практическая ценность. Работа носит теоретический характер. Ее результаты могут быть использованы в исследованиях по теории доказательств, по интуиционистской теории множеств, при построении моделей интуиционистской теории множеств.
Апробация работы. Результаты диссертации излагались автором на 3-ем Всесоюзном семинаре по нестандартному анализу (Саратов-1990), на вторых Математических чтениях памяти М.Я. Суслина (Саратов-1991), на 11-ой Международной конференции по логике, методологии и философии науки (Обнинск-1995), на 3-ей
Суслинской конференции (Саратов-1994). А также подробно излагались автором на научных семинарах Петербургского отделения Математического института РАН (руководитель член-корр. РАН, проф. Ю.В.Матиясевич, 1997), Института проблем передачи информации РАН (руководитель проф. Р.Л.Добрушин, 1995), кафедры математической логики МГУ (руководители проф. Н.К.Верещагин, 1994, проф. В.А.Любецкий, 1996).
Публикации. Результации диссертации опубликованы в работах автора [13 - 21].
Структура и объем работы. Диссертация состоит из введения, трех глав, прилокения и списка литературы. Общий объем диссертации 150 страниц, список литературы содержит 56 наименований.