Содержание к диссертации
Введение
Глава 1. История развития теории множеств с интуиционистской логикой: метаматематика и философские аспекты 24
Глава 2. Описание базисных теорий множеств с интуиционистской логикой и дополнительных постулатов конструктивного, интуиционистского и теоретико-множественного характера .. 92
Глава 3. Свойства ординалов в интуиционистской теории множеств. Интуиционистское доказательство совместности тезиса Чёрча с теорией множеств 100
Глава 4. Соотношения дополнительных постулатов в базисных теориях множеств с интуиционистской логикой 109
Глава 5. Независимость схемы собирания от принципа двойного дополнения множеств и vice versa в теории множеств с интуиционистской логикой 116
Глава 6. О допустимости правила Маркова в теории множеств с интуиционистской логикой. Предикаты реализуемости для теории множеств с интуиционистской логикой 126
Глава 7. Аксиома выбора в теории множеств с интуиционистской логикой 144
Глава 8. Вариант теории множеств "New Foundations" Куайна с интуиционистской логикой 151
Глава 9. Функциональные алгебраические модели для НА и теории множеств с интуиционистской логикой 159
Заключение 172
Литература 177
- История развития теории множеств с интуиционистской логикой: метаматематика и философские аспекты
- Описание базисных теорий множеств с интуиционистской логикой и дополнительных постулатов конструктивного, интуиционистского и теоретико-множественного характера
- Свойства ординалов в интуиционистской теории множеств. Интуиционистское доказательство совместности тезиса Чёрча с теорией множеств
- Соотношения дополнительных постулатов в базисных теориях множеств с интуиционистской логикой
Введение к работе
Актуальность темы исследования Третий кризис в основаниях математики, порожденный созданием Г. Кантором в конце XIX века учения о множествах (теории множеств), вызвал бурный рост различного рода течений математической философской мысли, связанных в первую очередь с возможностью преодоления возникшего кризиса (ликвидацией различного рода парадоксов в теории множеств (и не только в теории множеств, но и в самой логике)), а во вторую очередь переосмыслением философских оснований всего математического здания, которое к тому времени имело, казалось бы, прочное основание. Известные предложения по преодолению создавшейся кризисной ситуации и сохранению всего математического знания, накопленного к тому времени, не имели полного, признаваемого всеми математиками того времени, успеха, однако эти попытки преодоления кризиса в основаниях математической науки дали могучий рост разных течений философской математической мысли, начиная от позиции формализованного подхода Д. Гильберта, Б. Рассела, Э. Цермело и заканчивая появлением такого интересного направления в основаниях математики, как интуиционизм Л. Брауэра.
Интуиционизм мыслился его создателем Л. Брауэром как полностью невозможное к формализации математическое знание, ибо в основу математической деятельности Л. Брауэр положил интуитивную ясность и точность математических определений и конструкций.
Однако интуиционистская математика, созданная Л. Брауэром, была недостаточно четким образованием (для сравнения приведем ситуацию, которая сложилась чуть позже в теории алгоритмов, когда стало ясным, что существуют неразрешимые проблемы и что я успешного решения такого рода задач необходимо было уточнить неформальное понятие алгоритма, что и было сделано различными эквивалентными способами). В 1930 г. один из последователей Л. Брауэра, А, Гейтинг, предложил формализацию трёх основных логических исчислений интуиционизма: интуиционистского исчисления высказываний IL, интуиционистского исчисления предикатов IPC и интуиционистской арифметики НА. Стало возможным изучать интуиционистскую математику с точки зрения теории доказательств (метаматематики) и её соотношение с классической математикой, т.е. математикой, применяющей полный закон исключённого третьего. Было доказано (с использованием негативной интерпретации К. Гёделя), что все три упомянутые исчисления получаются из их классических аналогов исключением полного закона снятия двойного отрицания (последнее не означает, что частные случаи этого закона не выводятся в том или ином виде в соответствующих интуиционистских исчислениях) и что классические исчисления и соответствующие их интуиционистские аналоги равнонепротиворечивы.
Дальнейшие исследования в области формализованной интуиционистской математики сосредоточились в первую очередь вокруг системы арифметики НА, которая рассматривалась как базисная система арифметики. Различные расширения НА, такие, как арифметика Пеано, традиционный конструктивизм А.А.Маркова-младшего, антитрадиционный конструктивизм, арифметика реализуемости и ряд других оказались непротиворечивыми относительно базисной системы арифметики НА. Каждая из этих формализованных теорий имела свою семантику, с которой НА оказалась согласована.
Во вторую очередь исследования коснулись математического анализа или теории действительного числа и здесь спектр рассматриваемых формализованных теорий оказался неизмеримо богаче арифметического. Обозрения работ в этой области можно найти в ряде монографий А, Г.
Драгалина, М. Бизона и периодических обзоров А. Трулстры, хотя полного изложения результатов исследований на данную тему не существует. Наконец, очередь дошла и до систем теории множеств.
Первые формализованные системы теории множеств, базирующиеся на интуиционистской логике, появляются в конце 60-х и начале 70-х годов XX века. Здесь одними из первых необходимо отметить работы Дж. Майхилла по интуиционистской теории типов и еще очень несовершенные, как бы наполовину бестиповые, теории множеств Л. Тарпа и Л. Позгея. Основной пик исследований формализованных систем теорий множеств приходится на 1973 - 1990 г.г. Здесь нельзя оставить без внимания работы Х.Фридмана, А. Щедрова, Дж. Майхилла, посвященные интуиционистскому варианту ZF, работы Г.Шварца по интуиционистской теории типов; замечательные работы В.Поуэлла (в которой строится расширение интерпретации Гёделя для арифметики НА до уровня некоторой бестиповой системы теории множеств Цермело-Френкеля) и Р.Грайсона (для интуиционистского варианта теории множеств со схемой собирания (collection) строится V - гейтингозначный универсум над полной алгеброй Гейтинга Н). Полный перечень работ занял бы не одну страницу и здесь приведены наиболее важные и интересные работы.
Актуальность исследований по формализованным исчислениям с подлежащей интуиционистской логикой состоит в том, что такие исследования дают возможность получить богатый и тонкий спектр моделей с целью уточнения различных оттенков трактования эффективности в математике, выявить влияние интуиционистской логики (как наиболее глубоко исследованной на данный момент среди неклассических логик) на различное понимание таких фундаментальных математических объектов, как натуральные числа, действительные числа, функциии различного рода, множества и т.д. Для теории множеств трудность и актуальность такого рода исследований состоит в построении различного спектра моделей для универсума мнеств, для понимания поведения и роли разного вида дополнительных, специфически как F интуиционистских так и конструктивных, а также и чисто теоретико множественных принципов, метаматематики их соотношений на уровне теории множеств (как правило, бестиповой).
Степень разработанности проблемы Как уже упоминалось в предыдущем разделе, первые работы в области теории множеств с подлежащей интуиционистской логикой, появляются в конце 60-х и начале 70-х годов прошлого столетия. Здесь необходимо отметить исследования Дж. Майхилла и Г.Ф. Шварца по теории типов с интуиционистской логикой (эти исследования в определенной степени опираются на исследования по формализованному математическому анализу А. Трулстры (арифметика всех конечных типов), Дж. Московакис, А.Г. Драгалина, М. Д. Кроля, А. М. Левина, В.Г. Кановея, Е. Бишопа, школы tfj исследователей-конструктивистов во главе с А.А. Марковым-младшим (Н.А.Шанин, Б.А. Кушнер, И.Д. Заславский, Г.С. Цейтин и ряд других), М. Бизона, Г. Крайзеля, И. Стаплса, С.К. Клини, Р. Весли, Б. Скарпеллини и др.). По теориям множеств полу бестиповым и полуинтуиционистским назовем уже упоминавшихся Л. Тарпа и Л. Позгея. По бестиповым теориям множеств с интуиционистской логикой типа Цермело-Френкеля (которые в основном и являются целью исследований автора диссертации) имеются исследования X. Фридмана (доказательство равнонепротиворечивости интуиционистского и классического вариантов теории множеств Цермело-Френкеля), А.Щедрова (интуиционистский вариант теории множеств, расширяющий систему формализованного анализа со схемой Крипке), В. Поуэлла (расширившего геделеву негативную интерпретацию на теорию множеств с принципом двойного дополнения множеств), Р. Грайсона (построившего для теории множеств со схемой собирания гейтингозначные модели) и ряда других авторов как в России, так и за рубежом. Все приведенные работы и ряд других, использованных в диссертации, цитируются в ней.
Цели и задачи исследования Основная цель работы заключается в том, чтобы предложить формализованный вариант бестиповой односортной теории множеств с подлежащей интуиционистской логикой, который мог бы играть роль базисной теории множеств такого типа и был бы признаваем исследователями других направлений (классиками, интуиционистами, конструктивистами и т.д.) как нейтральный по отношению к развиваемым ими вариантам теории множеств. Это позволило бы также оценить влияние интуиционистской логики на бестиповые теории множеств. С этой целью в диссертации решается ряд следующих задач:
• исследование вопроса о совместности и независимости предлагае- 4 J мого базисного варианта теории множеств с рядом конструктивных, интуиционистских и теоретико-множественных принципов, в том числе с некоторым вариантом стандартной аксиомы выбора;
исследование свойств класса ординалов в предлагаемом варианте теории множеств с интуиционистской логикой;
усиление ряда результатов (Р. Грайсона, X. Фридмана) для рассматриваемой системы теории множеств;
построение для исследуемого базисного варианта теории множеств двух классов моделей, построенных ранее для интуиционистской арифметики А.Г. Драгалиным.
,( Также стояла задача предложить интуиционистский вариант для теории множеств Куайна «New Foundations» и исследовать вопрос о возможности погружения (интерпретации) классической теории Куайна в ее интуиционистский вариант.
Перечисленные выше задачи оказались тесно связанными между собой с точки зрения построения необходимых моделей и их решение дало возможность положительно ответить на основной вопрос исследования. Теоретико-методологические основания исследования Исследование обсуждаемых в диссертации проблем основано на построении ряда моделей для теории множеств с интуиционистской логикой, которые имеют в целом и общем по своей структуре характер универсума, чьё построение осуществляется с помощью трансфинитной индукции по ординалам (напомним, что метатеорией является в большинстве случаев та же теория множеств с интуиционистской логикой и таким образом классические свойства ординалов не используются). Универсумы такого вида строились ранее в работах Х.Фридмана, Дж. Майхилла, Л. Тарпа и ряда других исследователей. Однако в диссертации предлагается единый метод построения таких моделей (и целых классов моделей), который однако формализованного обобщения не имеет. Модели этого вида (и первую очередь их разновидность реализуемостного типа) дали возможность получить ряд метаматематических результатов для бестипового варианта теории множеств с интуиционистской логикой типа Цермело-Френкеля, которые не удавалось до сих пор получить (в сферу приложимости моделей такого вида попал даже интуиционистский вариант теории множеств Куайна «Новые основания»). Отметим также, что в диссертации самым непосредственным образом используются результаты, полученные в области исследования теории множеств с интуиционистской логикой Х.Фридманом, Дж. Майхиллом, А. Щедровым, В. Поуэллом.
Научная новизна работы. Основные результаты, выносимые на защиту В диссертации строится ряд новых моделей для теории множеств с интуиционистской логикой, с помощью которых получены следующие новые результаты, выносимые на защиту:
Исследованы свойства класса ординалов в теории множеств с интуиционистской логикой.
Исследованы соотношения ряда дополнительных постулатов интуиционистского, конструктивного и теоретико-множественного характера в базисном варианте теории множеств с интуиционистской логикой.
Доказана независимость схемы собирания от принципа двойного дополнения множеств и обратно в теории множеств с подлежащей интуиционистской логикой.
Доказана допустимость правила Маркова с параметрами только по множествам в рассматриваемом варианте теории множеств; построены обобщенные модели типа предикатов реализуемости для теории множеств.,
Исследован ограниченный вариант аксиомы выбора в форме АС на вопрос ее совместности и независимости с теорией множеств с интуиционистской логикой.
Предложен интуиционистский вариант для классической теории множеств Куайна и доказана непротиворечивость классической NF относитель но этого варианта.
Построен класс функциональных алгебраических моделей для интуиционистской теории множеств с принципом двойного дополнения множеств и доказана теорема о корректности для этого класса моделей; доказано, что штрих-реализуемость Клини не является функциональной алгебраической моделью для арифметики НА.
8. Как итог всех полученных результатов, предложен вариант аксиоматической базисной системы теории множеств с интуиционистской логикой, как удовлетворяющий большинству естественных требований к такому варианту со стороны исследователей различных направлений в основаниях математики (предварительно изложена история развития формализованных интуиционистских теорий множеств за все время их существования и основные результаты в этой области за последние 30 лет).
Теоретическое и практическое значение диссертации Примененные в диссертации методы построения моделей для теории множеств с интуиционистской логикой могут найти практическое применение у специалистов по логике в области решения проблем построения моделей для формализованных исчислений высокого порядка. Полученные в работе результаты могут быть использованы при создании новых курсов по логике (по теории множеств с неклассической логикой), составить содержание ряда специальных курсов для студентов, специализирующихся по данной тематике.
Апробация работы Все основные результаты диссертации были доложены на ряде международных Конгрессов по логике, методологии и философии науки (YII (1983), (только опубликованы тезисы),УШ (1987), IX (1991), (только опубликованы тезисы), X (1995), XI (1999), XII (2003) (только опубликованы тезисы)), на ряде международных конференций Logic Colloquium (1998, 2001, 2002, 2003), на международной конференции 5h Kurt Godel Colloquium (1997), на ряде всесоюзных и всероссийских конференций по математической логике (1979,1982,1984,1986,1988,1991, 1993,1995 и др.), на ряде зарубежных конференций по математической логике (1988,1990,1993, 1996 и др.), на научно-исследовательском семинаре им. А.А. Маркова кафедры математической логики и теории алгоритмов механико-математического факультета МГУ под руководством академика СИ. Адяна и профессора В.А. Успенского (2002), на заседании семинара сектора логики ИФРАН под руководством докторов философских наук В.А. Смирнова, Е.Д. Смирновой и А.С. Карпенко (1990-2003), на семинаре кафедры логики философского факультета МГУ под руководством профессора Е.Д. Смирновой (2004), на заседании семинара кафедры алгебры УрГУ под руководством профессора Ю.М.Важенина (1997), на семинаре отдела алгебры Уральского отделения МИР АН (1997).
Структура диссертации Диссертация состоит из Введения, девяти Глав, Заключения и списка литературы.
К концу XIX и началу XX века учение Г. Кантора о множествах оформилось окончательно и математическая наука, казалось, могла бы наконец получить надёжный и прочный фундамент. Но именно в это время в созданном Г. Кантором учении обнаружились противоречия (парадокс Рассела, парадокс Кантора, парадокс Бурали-Форти и др.). Противоречия имели место не только математике, но и в логике. Ситуация была критической и получила название «третий кризис в основаниях математики». Были предложены различные выходы из создавшегося положения. , Один из таких выходов состоял в создании строго формализованной системы теории множеств и такая система была создана усилиями Э. Цермело и А. Френкеля (1908 и 1925 гг. соответственно) и получила название теории множеств Цермело-Френкеля или ZF.
Другой выход был предложен Л. Я. Брауэром в 1907-1908 гг. в [63] и получил название интуиционистской математики или интуиционизма. В основу математической деятельности Брауэр положил интуитивную ясность и точность математических определений и конструкций (были предложены и другие выходы из создавшегося положения, из которых необходимо отметить формализованный вариант теории множеств -теорию типов Б. Рассела, см. [113] и появившийся значительно позже также формализованный вариант теории множеств В. Куайна «New Foundations» («Новые основания»), см. [111], однако последний не получил широкую известность среди математиков и логиков; но все отмеченные системы теории множеств использовали в качестве подлежащей логики классическую логику предикатов). Стоит также отметить, что ни один из выходов из создавшейся ситуации выходом не оказался, ибо никакой из этих путей не удалось по тем или иным причинам пройти до конца, планируемого создателями.
Интуиционистская математика, созданная Л. Брауэром, была недостаточно чётким образованием и уже в 1930 г. один из последователей Л.Брауэра, А. Гейтинг, см. [84] и [7], дал формулировку трёх основных логических исчислений интуиционизма:
интуиционистского исчисления высказываний IL, интуиционистского исчисления предикатов IPC и интуиционистской арифметики НА. Было доказано (с использованием негативной интерпретации К. Гёделя, см. [77]), что все три упомянутые исчисления получаются из их классических аналогов опусканием полного закона снятия двойного отрицания (последнее не означает, что частные случаи этого закона не выводятся в том или ином виде в соответствующих интуиционистских исчислениях) и что классические исчисления и соответствующие их интуиционистские аналоги равнонепротиворечивы.
Дальнейшие исследования в области формализованной интуиционистской математики сосредоточились в первую очередь вокруг системы арифметики НА, которая рассматривалась как базисная система арифметики. Различные расширения НА, такие как арифметика Пеано, традиционный конструктивизм А.А.Маркова-младшего, антитрадиционный конструктивизм, арифметика реализуемости и ряд других (см. [9], а также [57]) оказались непротиворечивыми относительно базисной системы арифметики НА, но каждая из этих формализованных теорий имела свою семантику, согласованную с НА.
Во вторую очередь исследования коснулись математического анализа или теории действительного числа и здесь спектр рассматриваемых формализованных теорий оказался неизмеримо богаче арифметического. За обозрением работ в этой области мы отсылаем читателя к монографии А.Г.Драгалина [9]. Наконец, очередь дошла и до систем теории множеств.
Первые формализованные системы теории множеств, базирующиеся на интуиционистской логике, появляются в конце 60-х и начале 70-х годов XX века. Здесь одной из первых необходимо отметить работу Дж. Майхилла по интуиционистской теории типов [102], еще очень несовершенные, как бы наполовину бестиповые, теории множеств Тарпа [122] и Позгея [ПО]. Основной пик исследований формализованных систем теорий множеств приходится на 1973 - 1990 г.г. Здесь нельзя оставить без внимания работы Х.Фридмана [70] - [72], [76] (совместно с А. Щедровым), [73] (обзор нерешенных проблем); работы Дж. Майхилла [103] и [104], посвященные интуиционистскому варианту ZF и ) формализации конструктивного анализа Бишопа соответственно; работу Г.Шварца по интуиционистской теории типов [55]; замечательные работы В.Поуэлла [109] (в которой строится расширение интерпретации Гёделя для арифметики НА до уровня некоторой бестиповой системы теории множеств типа Цермело-Френкеля) и Р.Грайсона [79] (для интуиционистского варианта теории множеств со схемой собирания (collection) строится VH - гейтингозначный универсум над полной алгеброй Гейтинга Н). Полный перечень работ занял бы не одну страницу и здесь приведены наиболее важные и интересные работы.
Настоящая работа представляет исследования автора по бестиповым теориям множеств типа Цермело-Френкеля, в которых подлежащей логикой является логика IPC и, безусловно, является продолжением работы [31], в которой эти исследования были начаты. В работе исследуются бестиповые интуиционистские ( т.е. базирующиеся на логике IPC) варианты классической системы теории множеств ZF, которые могут содержать на первом уровне как арифметику Гейтинга НА (см. [9]), так и систему Клини и Весли, формализующую интуиционистский анализ FIM (см. [9] или [18]). Точные формулировки всех рассматриваемых в работе теорий множеств (конечно, как уже отмечалось, подлежащая логика является интуиционистской) приведены Главе 2. Дадим теперь описание полученных результатов по главам.
Глава 1 диссертации посвящена вопросам философского характера и выводы, полученные в этой главе, опираются на современное состояние исследований разных логиков как в области теории множеств (в первую очередь), так и в области арифметики и анализа, которые, вместе с теорией множеств, составляют основания математической науки. С философской точки зрения необходимо отметить работы философов-логиков Б.В. Бирюкова, В.А. Бочарова, A.M. Анисова, В.Л. Васюкова, Е.К.Войшвилло, Ю.В. Ивлева, В.И. Маркина, В.А. Смирнова, Е.Д. Смирновой. Как уже отмечалось, к концу XIX и началу XX веков открытие Г.Кантора оформилось в отдельную ветвь математики и теория множеств стала с успехом и широко применяться в различных разделах математики. Однако открытие противоречий привело к новому (третьему) кризису в основаниях математики, что повлекло бурное развитие математической мысли в разных направлениях, но ни одно из направлений ни привело к общепризнанному выходу из кризиса (последнее признается и авторами [30], см. стр. 416, которые являются крупнейшими специалистами в области оснований математики). В этой же Главе даётся краткий обзор развития формализованных систем интуиционизма от арифметики до теории множеств, причем последним уделяется главное внимание.
В Главе 3 рассматриваются свойства ординалов в теориях множеств с интуиционистской логикой и некоторые свойства упорядочений (порядков). Все эти свойства исследовались в [79] с помощью гейтингозначных моделей, а также устанавливались свойства ординалов, которые остаются верными при замене классической логики предикатов на интуиционистскую. Доказательства из [79] использовали внешним образом, т.е. метатеоретически, схему собирания, которая не является выводимой из схемы подстановки (см. [76]). В [32] доказано, что достаточно внешним образом воспользоваться только схемой подстановки, что, в силу вышесказанного, ослабляет доказательство из [79]. Также, в работе из [79] отсутствовали многие доказательства тех фактов, что ряд свойств ординалов влечет полный закон исключенного третьего и некоторые, наиболее интересные из этих доказательств, приводятся в работе.
Далее даётся доказательство совместности тезиса Черча с интуиционистской теорией множеств (для теории с двумя сортами переменных), причем внешним образом достаточно воспользоваться только теорией множеств с двумя же сортами переменных, со схемой аксиом подстановки и с аксиомой двойного дополнения множеств. Естественно, что схема аксиом собирания отсутствует. Таким образом, метаматематика доказательства использует интуиционистскую логику (в отличие, скажем, от [31] или [43], где внешним образом используется теория множеств ZF; это означает, что не используется в полном объёме классическое исчисление предикатов, т.е. методы доказательства носят чисто интуиционистский характер). Доказательство впервые было анонсировано в [32] и [87]. В [33] и [88] были приведены полные доказательства отмеченного факта. Эти доказательства (используя технику из [32]) переносятся и на односортную теорию множеств. Полученный результат являлся ответом на вопрос Х.Фридмана из [76] «.. .it is not known whether ZFIR is equiconsistent with ZFIR + «Every /ею is recursive»». ZFIR - это далее ZFIR.
В Главе 4 даётся сводка результатов о соотношении различных принципов конструктивного, интуиционистского и теоретико-множественного характера в теории множеств с интуиционистской логикой, к которой добавлены принцип двойного дополнения множеств DCS и схема аксиом собирания. Часть этих результатов была получена в [31]. В данной работе доказывается независимость сильного теоретико-множественного принципа униформизации от тезиса Чёрча с выбором,что решает вопрос о взаимной независимости этих фундаментальных принципов, однако теория множеств берется без аксиомы объёмности. Известно, что (см. [55]) в присутствии аксиомы объёмности принцип униформизации с единственностью выводим из тезиса Чёрча с единственностью (этот же результат остается верным и для теории множеств с интуиционистской логикой). Таким образом, в качестве нерешенной остается только задача доказательства невыводимости сильного принципа униформизации из тезиса Черча с единственностью (или без единственности) или из слабого же принципа униформизации. Решение последней задачи позволило бы полностью закрыть вопрос о соотношении отмеченных принципов в теории множеств с интуиционистской логикой и с аксиомой объёмности. Здесь только отметим, что техника, примененная в [55] для теории типов, к бестиповым теориям не применима. Еще ряд приводимых метасоотношений между разного рода принципами является, как правило, легким следствием либо результатов из [31], либо сформулированного выше результата, полученного в диссертации. Рассматриваемые при этом теории множеств могут содержать в языке один, два или три сорта переменных, причем в первом случае те же результаты могут быть получены и для односортной теории множеств, но технически это гораздо труднее.
В Главе 5 рассматривается теория множеств с интуиционистской логикой, с принципом двойного дополнения множеств и со схемой подстановки, которая, с нашей точки зрения, претендует на роль базисной аксиоматической системы теории множеств с интуиционистской логикой, играющей в теории множеств роль, аналогичную роли НА в арифметике. Доказывается, что такая система теории множеств обладает свойствами дизъюнктивности и полной экзистенциальное™. С этой целью модель Майхилла из [103] расширяется до отмеченной теории множеств. Так как система теории множеств со схемой собирания свойством полной экзистенциальности не обладает (см. [76]), то в виде следствия получаем, что схема собирания не является выводимой из принципа двойного дополнения множеств (см. [92] или [42]). Это ещё один результат о независимости, полученный работе.
В этой же Главе доказывается, что принцип двойного дополнения множеств DCS не зависит от схемы аксиом собирания (сравни со следствием из этой же Главы ) в интуиционистской теории множеств. С этой целью основная модель, использованная ранее в [31], модифицируется так, что все постулаты нашей теории множеств снова выполняются в новой модели, а принцип двойного дополнения множеств — нет. Основное изменение модели связано с некоторым ограничением на множества из универсума, а именно: множество теперь принадлежит универсуму, если выполнено еще одно, дополнительное, условие: пересечение множеств натуральных чисел из первых членов пар нашего множества по всем множествам из вторых членов пар нашего множества должно быть пусто и этим же свойством должно обладать любое множество, являющееся вторым членом некоторой пары нашего множества. Более подробные формулировки с разъяснениями будут даны в Главе 5 при построении универсума модели. Результат был анонсирован в [92] и затем опубликован в [44].
В Главе 6 исследуется вопрос о допустимости сильного правила Маркова с параметрами только по множествам в теории множеств с интуиционистской логикой, со схемой собирания и аксиомой двойного дополнения множеств (см. [34], [35], [89], [90]) (вопрос о допустимости правила Маркова актуален в силу того, что допустимость этого правила в теории множеств с интуиционистской логикой говорит о конструктивном характере этой теории). Доказано, что сильное правило Маркова с параметрами по множествам и с единственным параметром по натуральным числам допустимо в теории множеств со схемой собирания и с принципом двойного дополнения множеств. Для арифметики и для HAS (арифметики второго порядка) этот результат был получен в 1973г. Трулстрой (см. [124]), который применил очень сложную технику, используя функционалы высоких порядков или нормализацию выводов. Позднее А.Драгалин в [9], а также несколько ранее А.Драгалина и независимо Х.Фридман в [74], предложили очень изящный и простой метод доказательства допустимости слабого правила Маркова для интуиционистских теорий (от арифметики до теории типов). Однако этот метод не мог быть прямо применен к теории множеств с интуиционистской логикой типа ZF. Построив универсум специального вида и определив понятие реализуемости формулы с использованием техники Драгалина-Фридмана, в Главе 6 и доказана допустимость соответствующего правила Маркова для бестиповой теории множеств с интуиционистской логикой. Затем удалось получить этот же результат как следствие обобщенного модельного подхода типа предикатов реализуемости к теории множеств (см. Главу 6, ниже), что распространяет технику предикатов реализуемости А.Драгалина для арифметики НА на значительно более мощную бестиповую теорию множеств с интуиционистской логикой с добавленным к ней принципом двойного дополнения множеств. Также, в [89] этот же результат переносится на односортную теорию множеств (см. Аппендикс).
Обобщение на теорию множеств результата А.Драгалина, полученного для интуиционистской арифметики НА с целью упорядочения различных моделей, которые были построены для получения разных результатов метаматематического характера, уже было упомянуто (см. [9], [10]). Техника эта получила название предикатов реализуемости для арифметики. Работает эта техника следующим образом: предположим, что для арифметики построена модель типа предиката реализуемости (при этом описывается именно класс реализуемостей в стиле Клини). Тогда из данного предиката типа реализуемости можно построить другой предикат и доказать, что он также - типа реализуемости (это - основной момент работ Драгалина). После этого показано на ряде примеров, как из одних моделей реализуемостного типа можно получать другие, более сложные, модели того же типа и доказывать для арифметики НА не только многие уже полученные ранее результаты, но и получать новые. Примерами служат: допустимость правила Маркова (без параметров) в НА, доказательство того факта, что доказательство допустимости правила Маркова не может быть формализовано в НА, исследование ослабленной формы этого же правила, чьё доказательство уже формализуется в НА и ряд других результатов. Здесь нужно отметить, что все метаматематические результаты, полученные ранее с использованием полного закона исключенного третьего, могут быть получены с помощью техники предикатов реализуемости и что попытки, предпринимавшиеся ранее с целью придать операции Сморинского интуиционистский характер, к успеху не приводили.
Эта техника предикатов реализуемости поднимается в работе на уровень бестиповой теории множеств (см. [45]) и примером этой техники служит результат этой же Главы о доказательстве допустимости правила Маркова без параметров по натуральным числам в теории множеств с интуиционистской логикой.
В Главе 7 рассматриваются варианты аксиомы выбора, которые не усиливали бы подлежащую интуиционистскую логику до классической. Актуальность и необходимость использования аксиомы выбора в интуиционистской теории множеств связана в первую очередь с построением математического анализа в этой теории. Известно, что стандартная форма аксиомы выбора (в ZFI (интуиционистской теории множеств) не все известные формы аксиомы выбора эквивалентны) влечет полный закон исключенного третьего (здесь ситуация такая же, как с эквивалентными классически аксиомой регулярности и схемой трансфинитной индукции по множествам: первая влечет полный закон исключенного третьего, см. [103] ) или, например, [65], [78]. В [89] Поуэлл доказал, что лемма Цорна совместна с интуиционистской теорией множеств, а также без доказательства утверждал, что интуиционистски приемлемой является аксиома выбора в виде счетной стандартной формы, обозначаемой АСШ, у которой все множества являются дискретными (множество дискретно, если любые два его элемента либо равны, либо не равны (интуиционистски!)). В Главе 7 доказывается, что некоторая счетная форма аксиомы выбора по множествам натуральных чисел совместна и независима с базисным вариантом теории множеств с интуиционистской логикой, к которому добавлен принцип двойного дополнения множеств. Все результаты, полученные в этой Главе, опубликованы в работах автора [36], [37], [91], [38].
Глава 8 посвящена построению интуиционистского варианта для теории множеств Куайна «Новые основания» ("New Foundations", NF, см. [111]). Система Куайна является мало известной, достаточно нестандартной формализованной системой теории множеств, которая, с одной стороны, напоминает теорию типов Рассела [113], а с другой стороны является бестиповой теорией множеств, в которой есть только одна аксиома - объёмности и одна схема аксиом - свёртки, однако свёртка осуществляется не по всем формулам языка теории, а только по так называемым стратифицируемым формулам (формула языка первого порядка теории множеств называется стратифицируемой, если можно так приписать индексы всем переменным этой формулы, что в элементарных формулах вида хєу переменная у получит индекс, на единицу больший индекса переменной х и одинаковые переменные получат одинаковые индексы). Конечно, логика в теории множеств Куайна — классическая. Относительно теории NF Шпеккер в [118] и [119] доказал, что аксиома бесконечности выводима в этой теории (первоначально это была действительно аксиома), что в NF выводимо отрицание аксиомы выбора (результаты первой работы) и что система Куайна может быть получена из системы Рассела добавлением принципа типовой неопределенности. Для NF не удалось пока построить модель какого-либо вида и выяснить ее соотношение с теорией ZF (в смысле взаимной интерпретируемости).
Для системы Куайна в работе впервые строится ее интуиционистский аналог NFI, который получается следующим образом: подлежащая логика является интуиционистской, а к постулатам теории NF добавляется следующий, классически верный, принцип: если двойные дополнения множеств х и у равны между собой, то равны и сами эти множества (интересно, является ли этот принцип независимым от остальных двух постулатов теории NFI?) У автора диссертации имеется гипотеза, что удастся получить модель для интуиционистского варианта теории Куайна. Для теории Куайна NF строится погружение её в интуиционистский вариант NFI с помощью негативной интерпретации Гёделя и доказывается, что все переводы аксиом и правил вывода выводимы в интуиционистском варианте, что и доказывает равнонепротиворечивость теорий NF и NFI. В конце Главы 8 формулируется ряд нерешенных проблем для интуиционистского варианта системы Куайна и для ее ослабления, в котором в аксиоме объёмности все множества являются непустыми. Все результаты Главы 8 опубликованы в работах [39] - [41].
В Главе 9 на теорию множеств распространяется другой подход А.Драгалина к построению моделей (теперь уже не только типа реализуемости) для интуиционистской арифметики НА, использующий технику функциональных алгебраических моделей. Основной результат состоит в том, что в любой такой модели выполняется вся интуиционистская логика предикатов. После этого модели конкретизируются для НА и приводится ряд примеров, демонстрирующих технику моделей функционального типа (см. [9], [11], [12]). Однако при построении функциональной алгебраической модели, соответствующей штрих-реализуемости Клини, была допущена ошибка. Автору диссертации удалось доказать (см. [46], [47]), что такой модели не существует.
Для обобщения подхода Драгалина строится подходящий универсум и расширяется понятие функциональной модели так, что не только интуиционистская логика предикатов, но и все основные аксиомы теории множеств выполняются в любой такой модели. Основные результаты были анонсированы в [93] и опубликованы в [48].
В Заключении предлагается некоторый вариант базисной системы теории множеств с интуиционистской логикой и его приемлемость обосновывается рядом результатов, полученных в области теории № множеств с интуиционистской логикой к настоящему времени рядом исследователей, включая и автора.
История развития теории множеств с интуиционистской логикой: метаматематика и философские аспекты
В математической логике всё большее и большее внимание уделяется исследованию неклассических логик: многозначных логик, модальных логик, релевантных логик и многих других. Среди этих логик наиболее важной, конечно, является интуиционистская логика. Подход, связанный с интуиционистской критикой оснований классической математики (здесь и далее прилагательное «классический» указывает на связь с двузначной классической логикой предикатов) и выдвинутый Л.Брауэром [63] в начале прошлого столетия, имеет глубокое и интересное философское обоснование, см. [30]. Интуиционистская логика является к настоящему времени глубоко изученным разделом неклассических логик. С её помощью в рамках концепции Брауэра проводилась обширная и глубокая математическая разработка (которая и по сей день имеет место в голландской математической школе) основ многих разделов математической науки. Интуиционистская логика лежит в основе построения ряда различных концепций конструктивности и позволяет очень точно и тонко анализировать важный вопрос о существовании объектов в математике.
Практические попытки построения математических теорий на базе интуиционистской логики (сопровождающиеся поразительным разнообразием оттенков эффективности при таких построениях) были изложены в ряде монографий и работ Гейтинга [7], Гудстейна [8], Мартин-Лёфа [24], Кушнера [22], Драгалина [9], Шанина [54] и других авторов. Например, в монографии Кушнера [22] изложены многие результаты исследований школы конструктивной математики А.А.Маркова, проведённые в 50-х — 70-х годах прошлого века.
Вслед за арифметикой Гейтинга на базе интуиционистской логики были построены и исследованы формальные системы математического анализа, включающие теорию действительных чисел и базирующиеся на различных дополнительных, специфически интуиционистских или конструктивных, принципах (Клини и Весли [18], Кушнер [22], Бишоп [60], Драгалин [9], Майхилл [106], [105], Трулстра [126]). При этом изучение характеризовалось построением большого количества разнообразных моделей для изучаемых теорий. Наконец, в конце 60-х годов XX века появляются первые исследования, связанные с изучением интуиционистских (т.е. базирующихся на интуиционистской логике) теорий множеств (Тарп [122], Позгей [ПО], Майхилл [103], [104], [102], Фридман [70] - [73],[76], Поуэлл [109], Грайсон [79], Шварц [55], Хаханян [49], [50], [52], [80]).
Цель настоящей Главы - дать историю развития формальных аксиоматических систем теорий множеств, основанных на интуиционистской логике, описать основные, полученные к настоящему времени (2002 г.) результаты, приведя основные виды моделей для получения этих результатов (ряд результатов и моделей, полученных автором, приводится в ряде Глав настоящей работы), т.е. описать метаматематику таких теорий множеств, а также сформулировать некоторые философские выводы, связанные с более чем столетним развитием формализованных систем теории множеств, в первую очередь по отношению к теории множеств с подлежащей интуиционистской логикой, чья история берет начало в конце 60-х годов прощлого столетия и привести систему теории множеств с интуиционистской логикой, играющей базовую роль в стиле роли системы теории множеств Цермело Френкеля (см. [129] и [69]). Данная Глава в сжатом виде взята из книги [51], опубликованной автором в 2003 году.
Чтобы направление исследований по формализованным системам теории множеств были более понятны, сначала будет дано краткое описание направлений исследований по формализованным системам арифметики и анализа.
В своих работах 1927-1930 А. Гейтинг [7] впервые в интуиционизме изложил три формализованных исчисления: интуиционистскую логику высказываний IL, интуиционистское исчисление предикатов IPC и интуиционистскую теорию чисел (арифметику) НА. С одной стороны, такая формализация противоречила основному принципу интуиционистской математики, утверждающему интуитивную ясность математических доказательств, с другой стороны, возник ряд вопросов метаматематического характера, решить которые без точного очерчивания границ соответствующих теорий не представлялось возможным. Формализованные теории исчисления высказываний, предикатов и арифметики решали эти задачи успешно. Получались эти теории из соответствующих классических исчислений опусканием полного закона исключенного третьего (конечно, ряд частных случаев этого закона оставался выводимым). При этом выполнялись некоторые неформальные семантические соглашения, характерные как раз для понимания суждений с интуиционистской точки зрения (эти соглашения в определенной степени характерны и для понимания суждений с конструктивной и ряда других эффективных точек зрения). Более У подробно эти соглашения описаны в [9] и здесь мы отметим только два существенных момента: а) формула вида cpv( считается истинной (доказанной, подтвержденной) только в том случае, если истинен по крайней мере один из ее членов (с точным указанием, какой именно). Приведем хорошо известный пример ван Далена, цитируя его из [9]. Теорема. Существуют два иррациональных числа а и b такие, что а рационально. Вот два различных с точки зрения интуиционизма доказательства этого факта.
Описание базисных теорий множеств с интуиционистской логикой и дополнительных постулатов конструктивного, интуиционистского и теоретико-множественного характера
Что касается операции а) в применении к теории множеств, то объединение моделей Крипке в новую модель (и доказательство того факта, что полученная модель есть именно модель Крипке) носит также интуиционистский характер, но конкретных приложений пока не сделано ввиду громоздкости технических конструкций. Отмеченное приложение [35] не требует полной общности и носит достаточно частный характер.
Кратко осветим вопрос о доказательстве приведенных выше утверждений, в первую очередь утверждения 3) (утверждение 4) есть очевидное следствие 1) - 3)). Основная трудность - построение универсума, в котором предикат А оказался бы экстенсиональным (это более трудный путь, отличный от приведенного выше, который исключил бы требования v) и vi) при определении предиката S; вся техника аккуратно изложена в [89] и перенос ее на общий случай не представляет каких-либо трудностей, кроме технических). В большинстве случаев предикат А есть предикат Т, ограниченный на атомарные формулы.
В заключение приведем ряд результатов из [9], которые, можно «поднять» на уровень теории Z. Отметим также, что Z может быть как односортной, так и двусортной теорией множеств. Хорошо известно, что принцип Р не является выводимым в НА, однако совместен с НА + СТ, но не с НА + СТ + М. Аналогичные результаты можно получить и на уровне теории множеств Z (как двусортной, так и односортной). Докажем допустимость принципа Р без параметров по натуральным числам, но с параметрами по множествам в двусортном варианте теории Z. Утверждение: если в Z Ь- -i(p - Эу\/(у), то в Z для некоторого натурального п выводимо —іф —» \j/(n). В качестве Л возьмем метапредложение "Z I 1—іф" и пусть Т\/ = "Z I іф - \/", а в качестве предиката А берем предикат Т, ограниченный на атомарные формулы (здесь ф - фиксированное предложение языка теории Z). Полагаем теперь S=S(A,A,T). Нетрудно видеть, что Т - r-предикат (если выводимо —іф - у и если выводимо —іф— (\/ — г), то, конечно, выводимо -іф — Т). Теперь предположим, что выводима формула —іф - Зу\/(у). В силу выполнимости пункта 3) истинно S(—іф — 3y\j/(y)). Нетрудно также видеть, что выполняется S(—іф) (так как и вф = S± и Т(-іф) о "Z І іф-»-іф"; если 8ф, то Тф и выводимо -чр—кр, а это противоречие, следовательно SJ_). Но, следовательно, истинно S(3yij/(y)), то есть, S\/(n) для некоторого натурального п, а тогда Т\/(п), то есть "Z I іф — \/(п)" для некоторого п, что и требовалось доказать. Для доказательств остальных интересных приложений, связанных с использованием предикатов реализуемости для теории Z, см. [45].
Вторым классом моделей для теории множеств ZFIC + DCS является обобщение еще одной конструкции А.Драгалина для арифметики НА до уровня отмеченной теории множеств, известное как функциональные алгебраические модели (см. [9] или [11] и [12]). В [12] А.Драгалин предложил общий подход для построения моделей для нестандартных логик в стиле равномерных алгебр, в [11] этот подход был специфицирован для интуиционистской логики. Здесь будут изложены одно замечание к работе А.Драгалина [11], которое опубликовано в [46] и [47] и обобщение конструкции А.Драгалина для интуиционистской теории множеств ( см. [93] и [48]).
Очень кратко определение функциональной алгебраической модели (ФАМ) для логики предикатов и для произвольной теории можно дать следующим образом. Функциональноая псевдобулева алгебра (ФПБА) задается набором B,D,F , где В - псевдобулева алгебра (ПБА) -алгебра истинностных значений, D - непустое множество (объектная область), a F - семейство функций или форм ФПБА, определенных на элементах из D и со значениями в ПБА. Основные требования на F: это семейство содержит ноль и единицу ПБА, замкнуто относительно псевдобулевых операций л, v, D и замкнуто относительно операций взятия верхних и нижних граней. Последнее означает вот что. Если f из семейства форм (например, от одной переменной), то должны существовать формы g и h такие, что g=A{f(x):xeD}, h=v{f(x):xeD}, т.е. должны существовать отмеченные верхняя и нижняя грани. Понятно, что не требуется, чтобы ПБА была полной.
Пусть теперь язык задается набором Cnst, Рг - констант и предикатных символов (этого всегда можно достичь). Теперь ФАМ для такого языка определяется набором ФПБА, Cnst, Pr , где Cnst: Cnst - D и Pr: Pr -» F (детали см. [11] или [47] или Главу 9). Если задана ФАМ для языка, то можно определить значение в модели для всякой формулы этого языка. Главное отличие этой конструкции от приводимой в книге Расёвой и Сикорского «Математика метаматематики» в том, что истинностное значение приписывается не оцененным формулам языка, а просто любым, в том числе и незамкнутым, формулам языка. При этом значение J_ есть ноль ПБА, атомарной формуле ставится в соответствие функция, являющаяся значением функции Рг, а затем по индукции определяется значение любой формулы с использованием замкнутости ФПБА относительно логических операторов и кванторов. Предложение языка истинно в модели, если его оценка из ФПБА есть единица (т.е.тождественно истинная функция). ФАМ есть модель теории, если все нелогические аксиомы этой теории получают оценку единица. Основная теорема гласит, что все выводимые в интуиционистской логике предикатов формулы являются истинными в любой ФАМ.
Если теперь в качестве теории взять НА, модифицировав её привычный язык требуемым образом, в качестве D взять все натуральные числа и счётное множество объектов, называемых «каналы» («канал» интуитивно есть натуральное число, о котором ничего не известно), в качестве Cnst взять функцию, сопоставляющую каждой константе п языка натуральное число п, то вся модель ФАМ определится заданием ФПБА (и, конечно ПБА) и функцией Рг.
Свойства ординалов в интуиционистской теории множеств. Интуиционистское доказательство совместности тезиса Чёрча с теорией множеств
Одним из наиболее важных понятий теории множеств, наряду с понятием множества, являются понятия ординала и кардинала. Существует несколько эквивалентных определений понятия ординала в теории множеств с подлежащей классической логикой предикатов. Ряд этих определений требует использования закона исключённого третьего при доказательстве основных свойств ординалов. Поэтому не все классические определения ординала можно прямо перенести в интуиционистскую теорию множеств. В качестве примера работ, в которых даются определения понятия ординала и доказываются основные свойства ординалов, а также приводятся контрпримеры для ряда других (классически верных) свойств ординалов, можно привести [109], [79] и [121]. Последняя работа лежит несколько в стороне от наших исследований, но представляет интерес, т.к. в ней дается определение ординала, для которого все классические свойства (т.е. свойства, при доказательстве которых используется закон исключенного третьего) могут быть доказаны и в интуиционистской теории множеств, в частности, это свойства ординала-последователя. В первых двух работах берётся следующее определение ординала: ординал есть транзитивное множество транзитивных множеств. Такое определение даёт возможность доказать, что последователь ординала также есть ординал и что объединение любого множества ординалов есть ординал. Также, в первых двух из цитированных работ даются определения порядков разных видов: частичных, линейных, фундированных и полных (вполне упорядочений). В [109] доказано (частично), что приведенное определение ординала разрешает доказать трансфинитные индукцию и рекурсию по ординалам. Также, такое определение ординала используется для построения кумулятивной иерархии Ra и (важный момент) для определения ранга множества таким образом, что х є Rrk(X)+i- Конечно, при таком способе определения понятия ординала последний является вполне фундированным множеством (см. [79]), но не является вполне упорядоченным, т.к. принцип наименьшего элемента влечет закон (полный) исключенного третьего, т.е. превращает интуиционистскую теорию множеств в ее классический аналог (для доказательства см. [103] или [79] ). Также можно определить понятие кардинала и развить форсинг, т.е. обсудить континуум-проблему. Можно определить множество натуральных чисел и транзитивное замыкание множества (см. [109]). Работа [79] посвящена построению в интуиционистской теории множеств (ниже мы приведём точную формулировку двух основных теорий множеств в стандартном (односортном) языке первого порядка -это теории ZFIR и ZFIC; эти две теории имеют различную дедуктивную силу, т.к. схема аксиом «collection» не выводится из схемы аксиом подстановки, как доказано в [76], что явилось решением одной из наиболее трудных проблем, приведенных в [73]) гейтингозначного универсума множеств как основной модели для теорий ZFIR и ZFIC. Однако доказательство того факта, что приведенный универсум является моделью этих теорий, внешним образом требует использования каждый раз теории ZFIC. В [32] доказано, что при использовании моделей типа реализуемости достаточно внешним образом (конечно, в случае теории ZFIR) использовать ту же самую теорию, что усиливает результат Грайсона из [79] (используя гейтингозначный универсум, в [79] приводятся строгие контрпримеры для ряда свойств ординалов, которые не выполняются (не выводятся) в отмеченных теориях множеств при приведенном выше определении ординала). Дальнейший план Главы 3 такой: сначала будет сформулирован ряд свойств ординалов и отмечено, какие из них верны интуиционистски, а какие нет (более точно: какие из них влекут полный закон исключенного третьего); затем будут сформулированы теории ZFIR и ZFIC и приведена модель типа реализуемости, в которой эти теории выполняются. Т.к. ряд свойств ординалов (не являющихся интуиционистски верными) влечет закон исключенного третьего (последнее будет доказано для тех свойств, для которых это не сделано в [79]) и т.к. в приведенной модели выполняется тезис Чёрча, то соответствующие свойства ординалов являются невыводимыми в отмеченных выше теориях, однако метаматематика нашего доказательства слабее, чем в [79].
1. Следуя [79], приведем следующие определения. Ординал а есть последователь, если ЗР(а=р4); есть слабо предельный, если Vpea. Зуєа. Рєу и сильно предельный, если Vpea. Р єа. Тогда утверждения а) «каждый ординал есть ноль, последователь или слабо предельный» и б) «все слабо предельные ординалы являются сильно предельными» каждое в отдельности влекут полный закон исключенного третьего.
Приведем полные доказательства того , что утверждения 1-5 и а) (для б) это доказано в [79]) влекут полный закон исключенного третьего, т.е. доказательство Теоремы 3.1 (пункт Б)). В случае 1. полагаем: a=0, Р={х : х=0лф}=1 . Если верен первый член дизъюнкции, то 0 є{х : х=0лф}, т.е. —іф; т.к. не верно, что Рєа, то снова имеем ф v —іф, ч.т.д. В случае 2. полагаем а={0,1 ,{0,1 }}, р={0,1}.Если а р,то l =0 v 1 =1 и -1фVф; если Р а, то 1=1 V 1={0,1 } и снова ф v —і ф, ч.т.д. В случае 3. полагаем а=1, Р={х : х=0 v (х=1лф)}. Ясно, что ас=Р; если Ієр, то ф; если {х : х=0}=1={х : х=0 v (х=1лф)}, то -іф. В любом варианте имеем Ф v -іф, ч.т.д. В случае 4. полагаем а=0; а+=0 и{0}={х : х=0}=1; р={х : х=0 v (х=1лф)}. Ясно, что 0 є р. Если Ієр, то ф; если 1=р, то —іф, ч.т.д. В случае 5. полагаем а=Г, Р =1, у ={0,1}. Нетрудно видеть, что аср и Рєу. Но если аєу, то Г=0, а тогда -іф, или 1 =1, а тогда ф, т.е. в любом варианте ф v —іф. Наконец, в случае а) полагаем а=Г. Если а=0, то -іф; если а=Р+, Р=0 и ф; наконец, а не может быть предельным, т.к. содержит не более одного элемента (точное доказательство рутинно). Итак, и в случае а) имеем всегда ф v —іф. Следовательно, в силу произвольности формулы ф получаем, что каждое из утверждений 1-5, а) влечёт полный закон исключенного третьего. Отметим, что в наших доказательствах активно использовалась аксиома объёмности и интуиционистская логика предикатов.
Соотношения дополнительных постулатов в базисных теориях множеств с интуиционистской логикой
Описание языка теории ZFIC было дано ранее. Атомарные формулы имеют вид хєу, остальные формулы строятся из атомарных обычным образом. Постулаты теории включают интуиционистскую логику предикатов и собственные аксиомы: экстенсиональности, пары, суммы, схемы выделения и собирания, Е-индукции и бесконечности. Отметим, что отсутствует аксиома множества подмножеств.
Построим универсум множеств А. Для более ясного понимания необходимо знакомство с [43] или [49]. Пусть ю - предельный регулярный кардинал, например, первый бесконечный кардинал. Каждое множество в универсуме А будет набором пар п,х , где п - натуральное число и х - уже построенное множество (построение А проводится индукцией по ординальным числам). В универсуме множеств А есть отношение эквивалентности и новое множество не должно его разбивать (см. также [43] или [49]). Определим теперь новое условие на множества из нашего универсума . Пусть у = {(п,х)}. Обозначим через у1 = {п : Зх.(п,х) є у} и через у2 = {х : Эп.(п,х) є у}. Через « обозначим отношение эквивалентности на А и для данных х и у пусть хун = {п : (п,х) є у}. Новое условие таково: если мощность у больше фиксированного со, то для любого подмножества zcy такого, что z со и которое не разбивает отношение эквивалентности «, n{x2H : xez2} = 0, т.е. пересечение всех множеств натуральных чисел, с которыми х входит в z , будет пустым. В частности, это условие выполнено как для самого множества у , так и для любого его подмножества, не разбивающего отношения эквивалентности на Л. В остальном построение А совпадает с построением универсума множеств в [43] или [49] (необходимое замечание состоит в том, что в цитируемых работах рассматривались двусортные теории множеств, здесь же рассмотрена модель для односортной теории множеств, однако ясно, как в этом случае модифицируется модель). Более формальное описание универсума множеств таково: Ао=0; для предельного ординала a: Да = u{Ap: р а}; Аа+і = {х : хс(АаХа)) л Bh.xext h}; xext h z 3hih2VyzeAa.((n,y)Gx л y«z(h!h2) == ! h(n,hi,h2) л (h(n,hbh2),z Gx); здесь y«z(h!h2) 3 Vnxh[«n,x)ey л xext h = !hi(n,h) л (hi(n,h),x)ez) и (наоборот с заменой у на z и hi на h2)]. Конечно, теперь ещё при определении пункта xext h нужно добавить новое условие на х, описанное выше. Определение же понятия реализуемости формулы при оценке (тут только одна оценка) в точности повторяет [43] или [49], но с учетом, что у нас только один сорт переменных - по множествам. Например: R(e,g,Vx (x)) - VxeA.R(e,gnx,( (an)), где g - оценка для переменных, также см. [43] или [49].
Основная Теорема 5.2.1. гласит: если в теории ZFIC - Р (без аксиомы степени) выводима замкнутая формула ф, то эффективно указывается число е такое, что VgR(e,g, ). Приведем доказательство основной теоремы. Возьмем а из А такое, что а ю. Тогда П{хан : хєа2}=0. Пусть для некоторых e,g R(e,g,DCS). Если R(k,g,—і—іуєа), где у є А, тогда любое п реализует —і-іуєа. И так для всякого у такого, что 3eR(e,g,-i-iyea). Тогда единое е(к) реализует уєх для некоторого хєА, но так быть не может, так как хєА = п{уануєх2}=0; конечно, х со, т.к. а со, . Итак, аксиома DCS нереализуема и невыполнима в предложенной модели. Остановимся на вопросе выполнимости в модели остальных аксиом. Часть аксиом (экстенсиональность, пара, бесконечность, индукция по множествам) реализуется в точности как в [49]. Остальные аксиомы, в которых требуется указать сущее множество, требуют, чтобы это множество принадлежало А, т.е. чтобы выполнялось дополнительное условие, описанное выше. Продемонстрируем это на схеме выделения 3xVy(yex г уєа л ф(у)). Пусть а - фиксированное множество из А. Полагаем х = { е,у : еІ5у єа л R(e2,g,c (y))}, где g - некоторая фиксированная оценка. Если х со, то {(еі,у) : (е,у)єх} со, (т.к. это подмножество аєА) и, конечно, n{yx„ уєх2}= 0, и тогда аналогичное условие будет выполнено для всех подмножеств х, которые не разбивают отношения эквивалентности, т.е. х будет принадлежать А. В остальном доказательство реализуемости схемы выделения проходит как в [49]. Совершенно аналогичным образом проходит доказательство выполнимости (реализуемости) аксиомы суммы Va3xVyz[yezAZGa-»yex]. Для данного аєА полагаем х = { п,у ЗгєД. ( Пі,у ez л n2,z єа}. Если х со, то либо z со для некоторого z, либо a co. В первом случае пересечение в х будет пусто по вторым компонентам (так как z из А), во втором случае пересечение в х будет пусто по первым компонентам, так как а из А. В любом случае х будет из универсума, так как выполнено условие на х, описанное выше (конечно, это же условие будет выполнено для любого подмножества X, которое не разбивает отношение «. Это доказывает реализуемость аксиомы суммы. Выполнимость (реализуемость) остальных аксиом, например схемы аксиом собирания ("collection") проводится аналогично приведёным доказательствам с учетом доказательств реализуемости для этих постулатов, описанных в [49]. Основная Теорема 5.2.1. доказана.
