Игошин Математическая логика и теория алгоритмов (1019110), страница 72

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 72)

С точки зрения логицизма антиномии — это симптомы, свидетельствующие об определенном неблагополучии не только в самой теории множеств, но и в существе применяемых в математике методов. Исходя из этого логицисты считают, что порочна не столько сама математика, сколько логика и ее использование для математических нужд, и предлагают предпринять глубокую реформу логики, которая заодно уже привела бы и к преодолению антиномий. Это направление характеризуется использованием средств нетрадиционных логик: неклассических (в частности, многозначных, интуиционистских и др.) логик, нестандартных средств логического вывода, дополнительных условий на доказательства, бесконечных правил вывода.

Системы, относящиеся к этому направлению, менее развиты. Знаменитые проблемы теории множеств. Методы аксиоматической теории множеств позволили отчетливо сформулировать и решить ряд трудных проблем, имевших свое происхождение в классических разделах математики. Важнейшей из таких проблем является проблема континуума. Именно ее поставил на первое место Д.Гильберт в своей знаменитой речи на П Международном математическом конгрессе, проходившем в Париже с 6 по 12 августа 1900 г., в которой им были сформулированы 23 актуальные математические проблемы. Еще Г. Кантор в 1878 г. сформулировал гипотезу, получившую название континуум-гипотезы: всякое бесконечное подмножество континуума й равномощно либо множеству натуральных чисел Ж, либо А, т.

е. не существует множества промежуточной мощности между счетной мощностью и мощностью континуума. Кантору не удалось ни доказать, ни опровергнуть эту гипотезу. Среди математиков росло убеждение в принципиальной неразрешимости проблемы континуума. Но только после того как вся проблемная среда, связан- 288 иая с континуум-гипотезой, была формализована, т.е. приобрела характер формальной аксиоматической теории, стало возможным математически точно поставить, а затем и решить вопрос о формальной неразрешимости континуум-гипотезы.

В 1939 г. К. Гедель показал, что если система Цермело — Френкеля ХР непротиворечива, то она остается непротиворечивой и после добавления к ней континуум-гипотезы. Это означает, что в системе ХР в предположении ее непротиворечивости невозможно доказать (вывести) отрицание континуум-гипотезы, т.е. отрицание континуум-гипотезы не зависит от остальных аксиом теории множеств, т.е. континуум-гипотеза не может быть опровергнута.

В 1963 г. американский математик П.Коан доказал аналогичное утверждение относительно континуум-гипотезы, т.е. континуум- гипотеза не может быть доказана, тем самым полностью закрыв проблему континуума. Таким образом, ни континуум-гипотеза, ни ее отрицание не зависят от остальных аксиом теории множеств. Это означает, что возможна теория множеств с континуум-гипотезой и возможна теория множеств с отрицанием континуум-гипотезы. Ситуация здесь оказалась сходной с той, которая возникла в начале Х1Х в.

с пятым постулатом Евклида, когда была открыта геометрия Лобачевского. Основным методом установления невыводимости формулы А в ХР является построение такой модели ХР, в которой выполняется отрицание А. Разработанный Козном, а затем усовершенствованный другими авторами метод вынуждения сильно расширил возможности построения моделей теории множеств и в настоящее время лежит в основе почти всех дальнейших результатов о невыводимости.

Совершенно аналогичной оказалась ситуация и с аксиомой выбора (ХР9). Гедель в 1939 г. доказал, что если система х,Р ~ (х.Р9) непротиворечива, то непротиворечива и система ХР, т.е. отрицание аксиомы выбора невыводимо из остальных аксиом системы 7Р. Невыводимость самой аксиомы выбора (х.Р9) из системы 2Р ~ (х.Р9) тоже установил Коан в 1962 г. С 1920 г. начинается история еще одной знаменитой математической проблемы ХХ в.

— проблемы М.Я. Суслина. Мы расскажем о ней ниже в пункте «О формальных теориях числовых систем», Установлено, что в системе 2Р ~ (х.Р9) не может быть ни доказано, ни опровергнуто (т.е. является неразрешимым) следующее утверждение: всякое подмножество множества действительных чисел измеримо по Лебегу. Выяснено взаимоотношение с системой ЕР многих важных проблем так называемой дескриптивной теории множеств, значительный вклад в которую внесли математики Московской математической школы, созданной академиком Н. Н.Лузиным (одним из ярких представителей которой является М.Я. Суслин). Получены многочисленные результаты об отсутствии ю ягоши« эффективно определенных обьектов в этой теории. Наконец, формализация теории множеств позволила обнаружить неизвестные ранее связи между проблемами «наивной» теории множеств.

Еше раз подчеркнем, что все зти проблемы удалось четко поставить и успешно разрешить только после формализации содержательной («наивной») канторовской теории множеств. О формальной арифметике. Язык и аксиомы. Это — логико-математическое исчисление (или прикладное исчисление первого порядка), формализующее элементарную теорию чисел. Наиболее популярная формализация основана на подходе Пеано, предложенном им в 1889 г.

и рассмотренном нами в в 26 (пример 26.3). Язык этого исчисления кроме логических связок и равенства содержит нелогическую константу О, двухместные функциональные символы +,, одноместный функциональный символ '. Термы строятся из константы 0 и переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида 0"-'. Атомарные формулы — зто равенство термов; остальные формулы строятся из атомарных с помощью логических связок. В качестве аксиом выбираются логические аксиомы, зто аксиомы формализованного исчисления предикатов (см. Э 25) и следующие нелогические (арифметические) формулы: х = у -«(х = е -«у = е), -1(х = 0); х=у — «х'=у', х'=у' — »х=у; х+О=х, х+у'=(х+у)' х 0 = О, х .

у' = (х ' у) + х'* ЖО) . Г~х)(Г(х) -~ Г('))) -+ Г«ХНЕ(х)), где Г(х) — произвольная формула теории с одной свободной предметной переменной х. Последняя формула есть схема аксиом, называемая схемой аксиом индукции. Средства формальной арифметики оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. Более того, формальная арифметика оказывается эквивалентной аксиоматической теории множеств Ег Цермело — Френкеля без аксиомы бесконечности (УГ7): в каждой из этих систем может быть построена модель другой.

Программа Гильберта формализации математики и теорема Геделя о неполноте. Формальная арифметика играет исключительно важную роль в основаниях математики. Это связано с тем, что именно арифметика лежит в основаниях классической математики, проблема непротиворечивости которой сводится к проблеме непротиворечивости арифметики. Эта содержательная сторона нашла свое наивысшее выражение и на формальном уровне. Одним из путей выхода из кризиса в основаниях математики в начале ХХ в., обусловленного обнаружением парадоксов (ан- 290 тиномий) в теории множеств, должен был стать гильбертовский путь формализации математики и логики. Каждая конкретная математическая теория должна быть переведена на язык подхоляшей формальной системы таким образом, чтобы каждое осмысленное (ложное или истинное) предложение содержательной теории выражалось бы некоторой формулой формальной системы. Тогда естественно было надеяться, что этот метод формализации позволит строить все положительное содержание математических теорий на такой точной и, казалось бы, надежной основе, как понятие выводимой формулы (теоремы формальной системы).

Кроме того, такие принципиальные вопросы, как проблема противоречивости математических теорий, решались бы в форме доказательства соответствующих утверждений о формализующих эти теории формальных системах. Поскольку описанные нами формальные системы сами оказываются точными, или, как говорили в школе Гильберта, финитными, математическими объектами, можно было ожидать, что удастся получить финитные доказательства утверждений о непротиворечивости, т.

е. доказательства, которые в определенном смысле были бы эффективными, не зависящими от тех мощных средств, вроде абстракции актуальной бесконечности, которые в классических математических теориях как раз и являются причиной трудностей в их обосновании. Но результаты, полученные Геделем в начале 1930-х гг., привели к краху основных надежд, связывавшихся с этой программой Гильберта. Гедель доказал следующие две теоРемы, получившие общее название етеорема о неполноте формальной арифметикиьч 1) всякая естественная непротиворечивая формализация Я арифметики или любой другой математической теории, содержащей арифметику (например, теории множеств), неполна и непополнима.

Неполнота означает, что в Ю имеется содержательно истинная, но неразрешимая формула, т.е. такая формула А, что ни А, ни ее отрицание А не выводимы в Х Непополнимость |означает, что каким бы конечным множеством дополнительных аксиом (например, неразрешимыми в 5 формулами) ни расширить систему 5, в новой формальной системе неизбежно появятся свои неразрешимые формулы; 2) если формализованная арифметика в действительности не- противоречива, то хотя утверждение о ее непротиворечивости выразимо на ее собственном языке, но доказательство этого утверждения средствами, формализуемыми в ней самой, невозможно.

Эта теорема, как и первая, распространяется на всякую непротиворечивую формальную систему, содержащую формальную арифметику. Доказательство первой теоремы проводится разработанным "еделем методом арифметизации синтаксиса языка формальной 291 теории, который стал олним из основных методов теории доказательств (метаматематики). Этим методом строится формально неразрешимая формула. Фиксируется нумерация основных формальных объектов (формул, конечных последовательностей формул и т.д.) натуральными числами, такая, что основные свойства этих объектов (быть аксиомой, быть выводом по правилам системы и т.д.) оказываются распознаваемыми по их номерам с помощью весьма простых алгоритмов.

Характеристики

Список файлов книги