1.3. Интуиция и аксиоматизация

Застывший характер математических моделей и теорий не всегда бросается в глаза - мешает платонистская привычка смотреть на объекты математики как на особый "не зависящий от нас мир", который "нами только изучается".

Мало кто будет оспаривать застывший характер теории, которая полностью аксиоматизирована. В аксиомах такой теории выражены все принципы рассуждения, которые в ней допускаются. Тем самым принципиальная основа теории зафиксирована и всякое ее изменение выражается в явных изменениях аксиом.

Каким образом, однако, можно считать застывшими теории, которые не аксиоматизированы? Так, все математики сходятся во мнении относительно того, какие рассуждения о свойствах натуральных чисел следует признать доказательными, а какие приводят только к гипотезам или ошибкам. И это - несмотря на то, что большинство математиков не знают ничего о каких-либо аксиомах арифметики! И даже в случаях, когда теория вроде бы построена на аксиомах (как, например, геометрия в "Началах" Евклида), в ее рассуждениях могут быть обнаружены моменты, не вызывающие разногласий относительно их справедливости, но в аксиомах тем не менее не отраженные. Например, различные свойства отношения "точка A лежит на прямой между точками B и C" используются у Евклида без всякого обоснования. Только в XIX в. М.Паш ввел "аксиомы порядка", характеризующие это отношение. Тем не менее и раньше все математики рассуждали о нем одинаково, не сознавая, как это у них получается.

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

Человеческий мозг является настолько сложной системой связей и процессов, что нет никакой надежды, что "слабый свет сознания" будет держать под контролем все детали этого электрохимического фейерверка. Это заставляет признать, что кроме мыслительных процессов, которые осознаются (полностью или частично), в мозгу постоянно происходит масса процессов бессознательного мышления. Причем, как показывает опыт, если бессознательный процесс приводит к результатам, имеющим большое значение для данной личности, то результат иногда распознается сознанием. Однако сам процесс, приведший к результату, при этом может остаться скрытым от сознания (отсюда и впечатление "откровения", см. Ж.Адамар [1945], А.Пуанкаре [1908]).

Если существуют бессознательные процессы мышления, то должны существовать и неосознанные "разумные принципы", регулирующие это мышление (ведь оно приводит не только к беспорядочным сновидениям, но и к разумному решению реальных проблем). Такие принципы могут управлять и теми процессами мышления, которые частично осознаются.

В случае математических теорий мы как раз имеем дело с определенным комплексом бессознательных принципов, которые наряду с аксиомами (или даже совсем без них) регулируют наши рассуждения. Такие бессознательные регулирующие факторы, вырабатываемые в ходе интенсивных умственных занятий в определенной области, и следует называть интуицией. Можно говорить поэтому, что помимо явно сформулированных аксиом и правил вывода теория может быть зафиксирована и в особой интуиции. Можно говорить об интуиции натурального ряда, которая (без каких-либо аксиом) однозначно регулирует наши рассуждения о натуральных числах, или о "евклидовой интуиции", которая делает геометрию вполне определенной, хотя в аксиомах Евклида содержатся далеко не все предпосылки геометрических рассуждений.

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

Со временем, когда исследования достигают определенного уровня сложности, постоянство (определенность) интуитивных моделей становится недостаточным. Тогда среди специалистов начинают возникать разногласия: какие способы рассуждений до- пустимы, а какие - нет. Но даже если постоянства и достаточно, оно может оказаться "не того рода". Может оказаться, например, что допустимые (по общему мнению) способы рассуждения приводят к нелепым выводам. В истории математики подобные ситуации бывали: крах дискретной геометрической интуиции в результате открытия несоизмеримых отрезков (конец VI в. до н.э.), подозрительность к отрицательным и комплексным числам (до конца XVIII в.), спор Л.Эйлера и Ж.д'Аламбера относительно понятия функции (XVIII в.), плохо обоснованное обращение с расходящимися рядами (XVIII-XIX вв.), трудности восприятия теории множеств Кантора, парадоксы в этой теории (XIX в.), скандал с аксиомой выбора (начало ХХ в.). Все это - следствие неизбежной неконтролируемости бессознательных процессов. По-видимому, "принципы", регулирующие эти процессы, отбираются и укрепляются посредством своеобразного "естественного отбора на полезность". Однако мы знаем, что естественный отбор страдает "близорукостью", что он не способен на безошибочную далеко идущую координацию. Поэтому появление парадоксов (как действительных, так и мнимых) неудивительно.

Определяющая интуиция теории не всегда остается постоянной - особенно много изменений происходит на начальном этапе становления теории (когда интуиция, как и сама теория, еще не сложилась окончательно). На этом, самом деликатном, этапе между специалистами возникают особенно резкие разногласия (над новаторами издеваются и т.п.).

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

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

Аналогичное прояснение ситуации наступило с определением основных понятий математического анализа (предел последовательности, непрерывность и т.д.) в терминах "эпсилон-дельта". Однако оказалось, что некоторые из понятий, реконструированных в терминах "эпсилон-дельта", обладают неожиданными свойствами, которых у их интуитивного прообраза не было. Так, раньше полагали, что всякая непрерывная функция дифференцируема почти всюду, кроме отдельных исключительных точек "разлома". Однако если руководствоваться точным определением непрерывности, то оказывается, что можно построить непрерывные функции, не имеющие производной ни в одной точке (пример нигде не дифференцируемой функции К.Вейерштрасса). У А.Пуанкаре эти функции вызывали отвращение и он называл их язвой...

Появление у реконструированных понятий неожиданных свойств, во-первых, свидетельствует о том, что здесь происходит именно реконструкция (а не простое копирование интуитивных понятий), а во-вторых, это заставляет серьезно рассматривать вопрос об адекватности реконструкций.

Генетический метод "проясняет" одну интуицию средствами другой, т.е. действует относительно. Аксиоматический метод, напротив, действует "абсолютно" и состоит в следующем. Среди общепризнанных утверждений об объектах теории выделяются некоторые объявляемые аксиомами, т.е. "истинами", не требующими доказательства. После этого остальные утверждения теории уже требуется доказывать на основе аксиом. Доказательства могут содержать и интуитивные элементы, которые должны иметь более элементарный (более очевидный) характер по сравнению с тем, что выражено в аксиомах. Часто эти элементы сводятся к интуитивному использованию чисто логических средств рассуждения, арифметики целых чисел, математического анализа или теории множеств. Наиболее известные случаи, когда применялся аксиоматический метод: аксиомы Дж.Пеано для арифметики целых чисел, аксиомы Евклида, аксиомы Д.Гильберта для той же евклидовой геометрии, аксиомы Э.Цермело и А.Френкеля для теории множеств.

Аксиоматизация (так же как генетический метод) дает всего лишь реконструкцию интуитивных понятий. Проблема адекватности реконструкции здесь обычно сводится к вопросу: все ли существенные характеристики интуитивных понятий отражены в аксиомах или какая-то часть забыта? Более сложными являются случаи, когда аксиоматизация применяется не просто для реконструкции существующей интуитивной теории "один к одному", а для спасения последней, когда та запуталась в парадоксах. Система аксиом Цермело-Френкеля для теории множеств была создана именно в такой ситуации: в интуитивной теории множеств Г.Кантора были обнаружены парадоксы и аксиоматизация явилась единственным выходом из положения. Проблема адекватности реконструкции здесь особенно сложна: сохранено ли все положительное содержание интуитивной теории?

В чем может состоять критерий адекватности реконструкции? Рассмотрим в качестве примера определение понятия действительного числа через рациональные числа. Такие определения были предложены в 1870-х гг. одновременно несколькими математиками (Р.Дедекиндом, Г.Кантором и др.). В результате многие подразумеваемые ранее свойства действительных чисел превратились в теоремы. Но почему мы считаем эти реконструкции удовлетворительными? Достаточно ли точно и полно передают они исходное интуитивное понятие действительного числа? Как обосновать точность и полноту реконструкции, если исходное понятие существует только в интуиции и всякое его выделение оттуда становится новой реконструкцией, адекватность которой опять нуждается в обосновании? Другого пути нет: мы должны руководствоваться только тем, как интуитивное понятие проявляет себя в практике математических рассуждений. Если все свойства действительных чисел, которые ранее считались очевидными и которые хотя бы раз фиксировались на бумаге, доказаны как теоремы (на основе нового, реконструированного понятия), если все теоремы математического анализа, доказанные ранее с использованием интуитивного понятия, передоказаны на основе реконструированного понятия, то те стороны интуитивного понятия действительного числа, которые успели проявить себя в математической практике, в реконструкции отражены.

Но, быть может, некоторые стороны интуитивного понятия еще не проявили себя, но могут проявить в будущем? Оспаривать такое предположение, казалось бы, очень трудно. В самом деле, допустим, что так оно и случится: явится через 100 лет математик X и докажет новую теорему математического анализа, используя свойство действительных чисел, которое ранее никто не использовал (т.е. оно себя в математической практике никак не проявляло). И тогда все сразу согласятся, что это неотъемлемое свойство действительных чисел? И что оно подразумевалось и 100 лет назад? Последнее во всяком случае уже нельзя будет проверить - никто из ныне живущих математиков до открытия X не доживет! Другими словами, предполагать, что в интуитивных математических понятиях скрыты какие-то аспекты, которые очень долго не проявляют себя на практике ("на бумаге"), - это все тот же математический платонизм, считающий мир математических объектов существующим независимо от рассуждений математиков.

В ряде случаев дополнительным аргументом в пользу совпадения интуитивных понятий и их реконструкций оказывается построение нескольких принципиально различных, но эквивалентных реконструкций. Так, при уточнении понятия действительного числа в 1870-х гг. Г.Кантор определял действительные числа как сходящиеся последовательности рациональных чисел, Р.Дедекинд - как "сечения" во множестве рациональных чисел. Можно строго доказать эквивалентность этих реконструкций.

Другим впечатляющим примером является уточнение (казалось бы, весьма неопределенного) интуитивного понятия вычислимости (или понятия алгоритма). Начиная с 1930-х гг. было предложено множество различающихся по форме уточнений понятия алгоритма: рекурсивные функции, машины Тьюринга, лямбда-исчисление А.Черча, канонические системы Э.Поста, нормальные алгорифмы А.А.Маркова и др. И во всех случаях была строго доказана эквивалентность этих уточнений.

Эквивалентность различных реконструкций одного интуитивного понятия свидетельствует, что объем реконструированных понятий не является случайным. Это очень важный аргумент в пользу замены интуитивного понятия реконструкцией.

Тенденция перехода от интуитивных понятий к более или менее явным их реконструкциям в истории математики проявляется достаточно четко. Интуитивные теории не могут развиваться без этих реконструкций: усложнение понятий и методов приводит к необходимости их явной реконструкции просто для обеспечения нормального развития теории. В большинстве случаев реконструкция выполняется генетическим методом, а когда дело касается фундаментальных математических понятий (например, понятия множества) - аксиоматическим методом (фундаментальные понятия потому и фундаментальны, что их нельзя "генетически" свести к другим понятиям).

Теорема К.Геделя о неполноте (см. раздел 5.3) породила множество рассуждений о том, что аксиоматический метод недостаточен для реконструкции "живого, содержательного" математического мышления. Аксиоматику сравнивали с прокрустовым ложем, которое не в состоянии вместить все богатство содержательной математики. Это рецидив платонизма. Разве могут в математике какие-либо доказательные рассуждения происходить иначе, как по схеме "посылки - заключение"? Если так и всякое математическое рассуждение сводится к цепи заключений, то можно спросить: эти заключения происходят по определенным правилам (т.е таким, которые не меняются от одного случая к другому и от одного математика к другому)? И если правила являются определенными, то, будучи функцией человеческого мозга, могут ли они быть такими, что их нельзя никак явно сформулировать? Если какие-либо "правила" нельзя явно сформулировать, то, следовательно, нельзя доказать их определенность! Ну, а полагать, что в математике кроме рассуждений (по определенным правилам) имеются "объекты", существующие независимо от этих рассуждений, означает впасть в обыкновенный платонизм работающего математика.

Таким образом, преждевременно говорить об ограниченности аксиоматизации - границы ее применимости, по-видимому, совпадают с границами применимости самой математики (см. раздел 6.1).

В процессе развития математических теорий аксиоматизация и интуиция взаимодействуют. Аксиоматизация "проясняет" интуицию, когда та "запуталась в себе". Но аксиоматизация влечет за собой и неприятные последствия: многие рассуждения, которые в интуитивной теории опытный специалист проводит очень быстро и представляет компактно, в аксиоматической теории оказываются очень громоздкими. Поэтому после замены интуитивной теории аксиоматической (особенно если эта замена неэквивалентна по причине недостатков интуитивной теории) специалисты развивают новую интуицию, которая восстанавливает способность теории к творческому развитию. Пример тому - история аксиоматизации теории множеств. Когда в интуитивной теории множеств Кантора в 1890-х гг. были обнаружены противоречия, от них удалось избавиться путем аксиоматизации. Естественно, что созданная аксиоматическая теория множеств Цермело-Френкеля отличалась от интуитивной теории Кантора не только формой, но и отдельными аспектами содержания. Для работы в новой теории специалисты развили модифицированную интуицию (в том числе особую интуицию множеств и классов). Ныне вполне нормальной считается работа в теории Цермело-Френкеля на интуитивном уровне. Именно на таком уровне доказываются серьезные новые теоремы этой теории.

Какую пользу дает аксиоматизация?

Во-первых, аксиоматизация позволяет "подправить" интуицию: устранить неточности, двусмысленности и парадоксы, которые иногда возникают из-за неполной контролируемости бессознательных процессов. Самый впечатляющий пример - историю аксиоматизации теории множеств, мы только что отметили.

Во-вторых, аксиоматизация позволяет подвергнуть подробному исследованию отношения между принципами теории (прежде всего установить их зависимость или независимость), а также между этими принципами и теоремами теории. Для доказательства конкретной теоремы иногда требуются не все аксиомы теории, а только их часть. Исследования такого рода могут привести к созданию более общих теорий, которые применимы в различных конкретных теориях. Характерными примерами являются теория групп и многочисленные ее алгебраические ответвления.

В-третьих, нередко после аксиоматизации удается установить недостаточность данной теории для решения отдельных проблем, естественно возникающих в ней. Именно так произошло с континуум-проблемой в теории множеств. В таких случаях можно ставить вопрос о необходимости совершенствования системы аксиом теории, о развитии альтернативных вариантов теории и т.д.

1.4. Формальные теории

Насколько далеко может зайти процесс аксиоматизации теории? Возможно ли полное изгнание интуиции из рассуждений теории, т.е. исчерпывающее сведение теории к системе аксиом и правил вывода?

В трудах Г.Фреге, Б.Рассела и Д.Гильберта, относящихся к концу XIX - началу ХХ вв., процесс аксиоматизации ряда серьезных математических теорий действительно удалось довести до конца. Они были представлены в виде исчерпывающей системы аксиом и правил вывода, без всякой примеси интуиции. Логическая техника, разработанная этими корифеями, позволяет полностью аксиоматизировать любую теорию, которая основана на застывшей системе принципов (т.е. любую математическую теорию).

Как же выглядят такие полностью аксиоматизированные теории? Чаще всего их называют формальными теориями, подчеркивая, что в них ни один шаг рассуждения нельзя сделать, не сославшись на "документ" - точно сформулированный список аксиом и правил вывода. Даже "самоочевидные" логические принципы вроде "если A влечет B и B влечет C, то A влечет C" должны выводиться из явно сформулированных аксиом и правил вывода.

Более точно понятие формальности можно определить в терминах теории алгоритмов: теорию T можно считать формальной, если построен алгоритм (механически применяемая процедура вычисления) для проверки правильности рассуждений с точки зрения принципов теории T. Это значит, что если некто предлалагает математический текст, являющийся, по его мнению, доказательством некоторой теоремы в теории T, то механически применяя алгоритм, мы можем проверить, действительно ли предложенный текст соответствует стандартам правильности, принятым в T. Таким образом, стандарт правильности рассуждений для теории T определен настолько точно, что проверку его соблюдения можно передать вычислительной машине (следует помнить, что речь идет о проверке правильности готовых доказательств, а не об их поиске!). Если проверку правильности доказательств в какой-либо теории нельзя передать вычислительной машине и она доступна в полной мере только человеку, значит, еще не все принципы теории аксиоматизированы (то, что мы не умеем передать машине, остается в нашей интуиции и "оттуда" регулирует наши рассуждения).

В качестве несерьезного примера формальной теории можно рассматривать игру в шахматы - назовем это теорией Ш. Утверждениями в Ш будем считать позиции (всевозможные расположения фигур на доске вместе с указанием "ход белых" или "ход черных"). Тогда аксиомой теории Ш естественно считать начальную позицию, а правилами вывода - правила игры, которые определяют, какие ходы допустимы в каждой позиции. Правила позволяют получать из одних утверждений другие. В частности, отправляясь от нашей единственной аксиомы, мы можем получать теоремы Ш. Общая характеристика теорем Ш состоит, очевидно, в том, что это - всевозможные позиции, которые могут получиться, если передвигать фигуры, соблюдая правила.

Упражнение 1.1. Найдите пример недоказуемого утверждения теории Ш.

В чем выражается формальность теории Ш? Если некто предлагает нам "математический текст" и утверждает, что это - доказательство теоремы A в теории Ш, то ясно, что речь идет о непроверенной записи шахматной партии, законченной (или отложенной) в позиции A. Проверка не является, однако, проблемой: правила игры сформулированы настолько точно, что можно составить программу для вычислительной машины, которая будет осуществлять такие проверки. (Еще раз напомним, что речь идет о проверке правильности записи шахматной партии, а не о проверке того, можно ли заданную позицию получить, играя по правилам, - эта задача намного сложнее!)

Упражнение 1.2. Оцените объем текста этой программы на одном из языков высокого уровня.

Несколько серьезнее другой пример формальной теории (мы заимствуем его у П.Лоренцена). Утверждениями в теории L являются всевозможные цепочки, составленные из букв a, b например a, aa, aba, abaab. Единственной аксиомой L является цепочка a, наконец, в L имеется два правила вывода:

X X

--------, ---------.

Xb aXa

Такая запись означает, что в теории L из цепочки X непосредственно выводятся Xb и aXa. Примером теоремы L является цепочка aababb:

a |- ab |- aaba |- aabab |- aababb.

Этот факт обычно записывается так: L |- aababb (читается: в теории L доказуемо утверждение aababb).

Упражнение 1.3. а) Напишите все теоремы L, содержащие не более 7 букв.

б) Опишите алгоритм, отличающий теоремы L от других ее утверждений.

Очень важное общее свойство формальных теорий дает следующее

Упражнение 1.4. Покажите, что множество всех теорем формальной теории является эффективно перечислимым (по другой терминологии - рекурсивно перечислимым).

Таким образом, теоретически для каждой формальной теории существует вычислительная машина, которая печатает на бумаге подряд все ее теоремы (и ничего кроме теорем). К сожалению, в общем случае такая машина мало подходит для решения проблемы, которая обычно интересует математиков: доказуемо ли в данной теории данное утверждение? Если, сидя возле машины, мы дождались момента, когда интересующее нас утверждение напечатано, то проблема решена (утверждение оказалось доказуемым). Но пока этот момент не наступил, мы не можем знать, будет ли утверждение напечатано через некоторое время или не будет напечатано вообще.

Теорию T принято называть разрешимой (или эффективно разрешимой), если существует алгоритм, распознающий теоремы T среди всех ее рассуждений. В упражнении 1.3 Вы доказали, что теория L является разрешимой.

Языки серьезных формальных теорий содержат символ отрицания "~". В таких теориях решение проблемы, выраженной в некотором утверждении A, означает либо доказательство A, либо его опровержение (т.е. доказательство ~A). Если для решения проблемы попытаться воспользоваться перечисляющей машиной из упражнения 1.4, то мы, сидя возле машины, должны дожидаться печати утверждения A или ~A. Если будут напечатаны оба утверждения, это будет означать, что теория T противоречива (в ней можно доказать некоторое утверждение вместе с его отрицанием). Однако всего здесь четыре возможности: а) будет напечатано A, но не ~A, б) будет напечатано ~A, но не A, в) будет напечатано и A, и ~A (тогда теория T противоречива), г) не будет напечатано ни A, ни ~A. В случае г) мы можем сидеть у перечисляющей машины сколь угодно долго, однако ни напечатания A, ни ~A не дождемся. В этом случае теорию T принято называть неполной (а полной называется теория, в которой любое утверждение, которое можно сформулировать средствами языка теории, можно либо доказать, либо опровергнуть).

Упражнение 1.5. Докажите, что всякая полная формальная теория разрешима.

1.5. Логика

Логикой принято называть набор средств рассуждения, применяемых во многих теориях. Соответственно и каждая серьезная формальная теория должна иметь среди своих аксиом логические аксиомы, а среди своих правил вывода - логические правила.

Внешней оболочкой каждой теории является ее язык, на котором записываются утверждения теории (аксиомы, теоремы, гипотезы и т.д.). Первичными неделимыми единицами языка серьезных формальных теорий считаются:

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

б) константы (например, "0" в арифметике* интуитивно мы приписываем каждой константе "неофициальное" конкретное значение из области значений переменных),

в) функциональные символы (например, "+" в арифметике* "неофициально" это функция x+y),

г) предикатные символы (язык любой серьезной теории содержит как минимум символ "=", интуитивно понимаемый как равенство "объектов" теории),

д) логические связки и кванторы (отрицание "~", дизъюнкция "V", конъюнкция "&", импликация "->", квантор существования "E", квантор всеобщности "A"),

е) скобки и запятые.

Из переменных, констант и функциональных символов (а также скобок и запятых) по особым для каждого языка правилам составляются термы. Например, в арифметике возможен терм (x+y)+1, где x,y - переменные, 1 - константа, + - функциональный символ. Интуитивно, терм - либо составное обозначение для "объекта" из области значений переменных (например, (1+1)+1 - обозначение числа 3), либо обозначение функции.

Далее, из термов и предикатных символов составляются атомарные формулы. Например, (t₁ =t₂ ), где t₁, t₂ - любые термы теории. Атомарная формула P(t₁,..., t_n ), где t_i - термы, Р - предикатный символ, представляет собой утверждение, что "объекты", обозначенные термами t₁, ... ,t_n , находятся в отношении, обозначенном через Р.

Из атомарных формул, логических связок и кванторов по обычным правилам составляются формулы теории, например

(Ax)((x=0)V~(x=0)).

Это пример замкнутой формулы, все переменные которой связаны кванторами. Замкнутая формула - "определенное утверждение об объектах теории", тогда как "истинность" формулы, имеющей свободные переменные, может зависеть от того, какие конкретные значения эти переменные принимают. Например, формула (x=0)V(x=1) оказывается "истинной" при x=1 и "ложной" при x=2.

Покажем теперь, как можно сформулировать список логических аксиом и правил вывода, достаточный для воспроизведения общепринятых логических средств рассуждения. Большинство аксиом будут представлены схемами аксиом (каждая схема включает в себя бесконечное, но легко распознаваемое семейство аксиом). Эквивалентность не считается самостоятельной логической связкой, A<->B определяется как (A->B)&(B->A).

Сначала список аксиом:

L1) A->(B->A),

L2) (A->(B->C))->((A->B)->(A->C)),

L3) A->(B->A&B),

L4) A&B->A,

L5) A&B->B,

L6) A->AVB,

L7) B->AVB,

L8) (A->C)->((B->C)->(AVB->C)),

L9) (A->B)->((A->~B)->~A),

L10) ~A->(A->B) (из противоречия следует все),

L11) AV~A (закон исключенного третьего),

L12) (Ax)D(x)->D(t),

L13) D(t)->(Ex)D(x).

Здесь A,B,C - произвольные формулы, D - формула и t - терм такие, что кванторы D не связывают переменных, входящих в t.

Это были схемы аксиом исчисления предикатов. Далее следуют аксиомы, описывающие свойства равенства:

L14) x=x,

L15) x=y -> y=x,

L16) x=y -> ((y=z)->(x=z)),

L17) x=t -> (D(x,x)->D(x,t)).

Здесь D - формула, содержащая x и переменные терма t только свободно. Обозначение D(x,x) предполагает, что все вхождения переменной x в формулу D разбиты на две группы. Если все вхождения второй группы заменить на t, получится формула D(x,t).

Кроме аксиом нужны еще три правила вывода:

A, A->B C->D(x) D(t)->C

--------------, ---------------, ---------------

B C->(Ax)D(x) (Ex)D(x)->C

Первое правило принято называть MODUS PONENS, в нем A,B - произвольные формулы теории. В остальных двух правилах формула C не должна содержать x и переменные терма t.

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

Полный набор перечисленных выше аксиом задает так называемую классическую логику. Она используется в подавляющем большинстве математических теорий. Исключив схему аксиом L11: AV~A (закон исключенного третьего), получаем так называемую конструктивную (или интуиционистскую) логику. В теориях, использующих конструктивную логику, невозможны доказательства существования объектов методом "от противного". Такие неконструктивные доказательства существования основаны на схеме ~~A->A, которая равносильна L11 (с целью доказать утверждение A мы принимаем ~A в качестве гипотезы, выводим противоречие, т.е. доказываем ~~A, и делаем вывод об истинности A). Подробнее о конструктивной математике см. А.Г.Драгалин [1979], Б.А.Кушнер [1973].

Интересную роль играет схема L10: ~A->(A->B). Согласно ей если в теории обнаружено противоречие (выведены одновременно некоторая формула A и ее отрицание ~A), то тем самым становится выводимой любая формула B. Таким образом, для доказательства непротиворечивости какой-либо теории достаточно установить невыводимость в этой теории хотя бы одной формулы (например, 0=1)).

Следствием логических аксиом является также формула (Ex)x=x (проверьте). Таким образом, принятие одних только логических аксиом уже гарантирует "существование" по крайней мере одного "объекта" теории.

Важным логическим принципом является теорема дедукции: если в теории T, приняв в качестве гипотезы формулу A, можно доказать формулу B (сокращенная запись T,A |- B), причем в этом доказательстве к свободным переменным из A не применяются второе и третье правила вывода, то T |- A->B, т.е. уже без всяких гипотез в теории Т доказуема импликация A->B.

Упражнение 1.6. Покажите, используя теорему дедукции, что аксиомы L15, L16 следуют из остальных аксиом.

1.6. Программа Гильберта

К началу XX в. честь математики была поставлена под серьезное сомнение: в теории множеств были обнаружены парадоксы - самые настоящие противоречия. К этому времени теория множеств уже успела показать себя как естественная основа и плодотворнейшее орудие математики. Для спасения "основы и орудия" немецкий математик Давид Гильберт предложил в 1904 г. свою программу перестройки оснований математики, которая состояла из двух частей:

а) Представить существующую математику (включая очищенный от парадоксов вариант теории множеств) в виде формальной теории.

б) Доказать непротиворечивость полученной теории (т.е. доказать, что в этой теории никакое утверждение не может быть доказано вместе со своим отрицанием).

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

Дело в том, что, не решив до конца а), т.е. оставаясь отчасти в области интуитивной математики, нельзя говорить об абсолютном доказательстве непротиворечивости математики. В интуитивной теории можно надеяться обнаружить противоречие, т.е. можно надеяться доказать, соблюдая общепринятые (интуитивные) правила рассуждения, некоторое утверждение вместе с его отрицанием. Но никак нельзя даже пытаться доказывать непротиворечивость интуитивной теории, поскольку утверждение о непротиворечивости относится к множеству всех теорем, доказуемых в теории, т.е. к совокупности, четкого определения которой мы как раз не имеем.

Однако, если вместо интуитивной теории взять формальную, положение изменяется. Множество теорем формальной теории является уже точно определенным объектом. Несмотря на это оно все же бесконечно. Каким же образом Д.Гильберт рассчитывал получить доказательство утверждения о непротиворечивости, относящегося ко всему этому бесконечному множеству?

Вернемся к нашим примерам формальных теорий. В теории Ш множество всех теорем оказывается, правда, конечным (хотя конечность эта с практической точки зрения ближе к бесконечности). Легко доказать следующее утверждение, относящееся ко всем теоремам Ш: ни в одной теореме белые не имеют 10 ферзей. В самом деле, достаточно заметить, что в аксиоме Ш белые имеют 1 ферзь и 8 пешек и что по правилам игры белым ферзем может стать только белая пешка. Остальное решает арифметика: 1+8<10. Таким образом, мы подметили в системе аксиом и правил вывода теории Ш особенности, которые делают справедливым наше общее утверждение о теоремах Ш.

Аналогичные возможности имеем в случае теории L. Можно доказать, например, следующее утверждение, относящееся ко всем теоремам L: если X - теорема, то aaX - тоже теорема. В самом деле, если X=a (X - аксиома), то L |- aaa по второму правилу вывода. Это базис индукции. Шаг индукции: если для теоремы X выводимость aaX уже установлена, то для теорем aXa и Xb имеем aaX |- aaaXa, aaX |- aaXb. Таким образом, индукцией по структуре вывода справедливость нашего утверждения установлена.

Итак, если множество всех теорем теории точно определено, можно доказывать утверждения, относящиеся ко всем теоремам одновременно. Д.Гильберт полагал, что утверждение о непротиворечивости теории не будет исключением. Грубо говоря, он надеялся подметить особенности системы аксиом всей математики, которые делают вывод противоречия невозможным.

Заметим, однако, что утверждение, относящееся к бесконечному множеству объектов, не может быть доказано простой эмпирической проверкой (перебором объектов). Всякое его доказательство неизбежно должно быть теоретическим. Например, при доказательстве утверждения L |- X --> L |- aaX мы воспользовались математической индукцией. Так в какой же теории следует доказывать непротиворечивость формальной теории, охватывающей всю существующую математику? Ясно, что средства рассуждения, используемые для обоснования непротиворечивости некоторой теории Т, должны быть более надежными по сравнению со средствами, допускаемыми в самой теории Т. В самом деле, можно ли доверять доказательству непротиворечивости, если в нем используются сомнительные средства, сами нуждающиеся в обосновании? Но если теория Т охватывает всю математику, то никаких средств рассуждения, выходящих за рамки Т, математик знать не может. Поэтому необходимые для доказательства непротиворечивости средства рассуждения мы вынуждены черпать из самой (универсальной) теории Т - из той ее части, которая представляется нам наиболее надежной.

В математике четко выделяется два уровня "надежности" рассуждений:

1) арифметические ("дискретные") рассуждения используют только понятие целого числа и аналогичные дискретные объекты,

2) теоретико-множественные рассуждения используют канторовское понятие о произвольном множестве.

Первый уровень считается надежным (его мало кто подвергает сомнению), второй - опасным (его только недавно "очистили" от явных противоречий). Д.Гильберт рассчитывал, разумеется, на доказательство непротиворечивости всей математики средствами первого уровня.

Сразу, как только Д.Гильберт объявил о своем проекте (1904 г.), французский математик А.Пуанкаре высказал сомнения в его реальности. По мнению А.Пуанкаре, Д.Гильберт, доказывая непротиворечивость математики с помощью математической индукции (самое важное средство первого уровня), допускает в своих рассуждениях порочный круг. Непротиворечивость математики означает и непротиворечивость математической индукции,... доказанную с ее же помощью! Мало кто тогда (включая самого Д.Гильберта) мог осознать серьезность этого намека... Но через 25 лет К.Гедель доказал, что А.Пуанкаре был прав: абсолютное доказательство непротиворечивости математики невозможно (см. раздел 5.4).