| Тимур Василенко ( @ 2007-07-31 19:58:00 |
| Entry tags: | Наблюдения краем глаза |
Противоречие и существование
Девиз Таинственный похож
На опрокинутое 8:
Она - отраднейшая ложь
Из всех, что мы в сознаньи носим.
И. Анненский
В математической логике есть теорема Гёделя о полноте, гласящая, что любая непротиворечивая теория первого порядка имеет модель. То есть если в теории нет противоречия, то описываемый этой теорией объект существует. Более детальный анализ показывает, что если теория имеет конечный или счетный язык, то существует счетная модель этой теории (это уже теорема Левенгейма-Сколема). Возьмем канторовскую теорию множеств в аксиоматике Цермело-Френкеля (ZF). Она утверждает существование несчетных множеств, более того - существование бесконечной последовательности все более мощных ординалов. Одновременно с этим теория множеств в аксиоматике ZF удовлетворяет условиям теоремы Левенгейма-Сколема и, тем самым, имеет счетную модель, в которой все эти бесконечные ординалы счетны. Получили противоречие, которое носит название парадокса Сколема.
Рассмотрим это подробнее. Два множества называются равномощными, если существует взаимно-однозначное соответствие между их элементами; если же такого соответствия нет и первое множество взаимно-однозначно отображается на подмножество второго, то говорят, что мощность второго множества больше. Согласно теореме Кантора мощность множества всех подмножеств непустого множества больше мощности этого множества (P(A)>A), а специальная аксиома ZF (аксиома степени) гарантирует, что вместе с любым множеством существует и множество всех его подмножеств. Как же такая теория может иметь счетную модель?
Классическое (и, насколько мне известно, единственное) разрешение парадокса Сколема состоит в том, что в этой счетной модели взаимно-однозначное соответствие, конечно, есть, но оно не выразимо в языке этой теории, т.е. в рамках теории его как бы и нет. Более того, при любой попытке формализации теории это взаимно-однозначное соответствие так и останется невыразимым (собственно, мы даже не знаем, что это невозможно, мы на это надеемся - иначе теория множеств окажется противоречивой).
Формально парадокс решен, но неформально возникает подозрение, что в этой счетной модели что-то не так. Логично было бы ожидать, что формальные рассуждения не могут ограничивать неформальные, поскольку являются их частью. Если бы мы начали с формальной теории, получили бы некий странный результат, а потом неформально, т.е. более богатыми средствами, его интерпретировали - все было бы понятно. Мы же начали с неформальной канторовской теории множеств, формализовали ее аксиоматикой ZF, получили некий странный результат (парадокс Сколема) и смогли его интерпретировать только в рамках формальной, более узкой теории. На верхнем же, неформальном уровне, парадокс Сколема остался - в конце концов, построение счетной модели в теореме Левенгейма-Сколема осуществляется достаточно неформальными рассуждениями. Придется немного проанализировать доказательство теоремы Гёделя о полноте и подетальнее разобраться во взаимосвязи непротиворечивости и существования.
Что значит, что теория непротиворечива? Это значит, что сколько бы мы ни проводили логических выводов, понимаемых как цепочка формул, выписываемых по определенным правилам, мы никогда не выведем ложь, т.е. утверждение вида A&¬A. У нас есть непротиворечивость как некое свойство записей, текстов - и больше, в общем, ничего нет. То есть из этого синтаксического материала нам придется строить лингвистическую модель нашей формальной теории: рассмотрим множество термов (выражений вида 1+1, (1+1+1)*(1+1+1+1-1-1+0) и т.п., использующих константы и функции, но не использующих переменные, кванторы и предикаты) и введем на нем отношение эквивалентности такого вида: T1~T2, если в этой теории доказуема формула T1=T2; факторизуем множество всех термов по этому отношению эквивалентности (т.е. разобьем его на непересекающиеся подмножества из эквивалентных элементов) - получаемые классы эквивалентности и служат носителем модели (подробнее можно прочесть в любом учебнике матлогики). Осталось только определить мощность полученной модели. Алфавит теории счетен, длина любой формулы конечна, так что множество всех формул счетно. Классы эквивалентности - это непересекающиеся подмножества формул, т.е. их количество не более чем счетно. Т.о. мы получили счетную лингвистическую модель непротиворечивой теории. При этом счетность модели устанавливается средствами неформальной канторовой теории множеств, так что парадокс Сколема на неформальном уровне остается.
Оставим в стороне теорию множеств и сконцентрируемся на теореме Гёделя о полноте: непротиворечивая теория имеет модель, т.е. описываемые ею объекты в каком-то роде существуют. Насколько вообще правомочна такая лингвистическая модель для непротиворечивой теории? Неужели существование тождественно непротиворечивости (хотя бы в математике)? Неужели способность говорить о чем-то, не запутываясь при этом, доказывает, что это что-то существует? Проанализируем само понятие противоречия, чтобы как-то осмыслить непротиворечивость и существование. Прежде всего, противоречие - единственное абсолютно конструктивное понятие в математике, в любом ее изводе - что в классической, что в интуиционистской. Противоречие всегда строится явно, предъявляется. Возьмем понятие доказательства от противного: мы предполагаем некую гипотезу, противоположную тому, что хотим доказать. Потом самим ходом доказательства мы строим противоречие - выводим одновременно A и ¬A. Хотя доказательство теоремы косвенное (от противного), но само противоречие сконструировано, построено и предъявлено. В принципе, косвенным образом использовать противоречие это предположить, что оно имеет место - тупик с точки зрения логики, поскольку из такого предположения следует все, что угодно. Непродуктивно. Итак, противоречие используется именно конструктивным образом, зато его отрицание - точнее, утверждение о том, что его нет (непротиворечивость) - очень даже используется неконструктивным образом. Условно говоря, непротиворечивость либо доказывается - обычно построением модели одной теории в другой, получается такая относительная непротиворечивость, очень полезная вещь: благодаря ей из натуральных чисел, которые от бога (Кронекер), последовательно строятся целые, рациональные, действительные, комплексные числа, а также модели нестандартного анализа с актуальными бесконечно-малыми величинами; другое использование понятия непротиворечивости - она предполагается для некоторой теории и дальше делаются выводы на основании этого предположения. Один из таких выводов - что любая непротиворечивая теория имеет модель - мы как раз и рассматриваем.
Есть еще одна противоречащая интуиции теорема - теорема компактности: пусть дана теория первого порядка с (возможно) бесконечным числом аксиом; известно, что любая ее подтеория с конечным числом аксиом имеет модель; тогда и исходная теория имеет модель. Доказательство достаточно просто: предположим, что исходная теория противоречива, тогда существует конечный вывод противоречия, который может использовать только конечное количество аксиом; но подтеория, включающая только эти аксиомы, по условию имеет модель, т.е. непротиворечива; тем самым мы получаем непротиворечивость исходной теории, которая (по теореме Гёделя) имеет модель. Интересно отметить, что в этом доказательстве понятие противоречия используется дважды: один раз косвенно, предполагая его отсутствие (наличие) и второй раз уже конструктивно, строя его в самом доказательстве от противного.
Теорему компактности можно доказать и без использования теоремы Гёделя о полноте, с помощью ультрапроизведений и теоремы Лося. Я не буду вдаваться в подробности, отмечу только, что и здесь используются в виде носителя модели классы эквивалентности неких конструктивно построенных объектов. А теперь посмотрим на некоторые следствия из этой теоремы.
Рассмотрим аксиоматику абелевых групп, дополненную бесконечным числом аксиом Cn, утверждающих существование n различных элементов группы. К примеру, это можно записать так:
Существуют x1…xn (x1≠x2) & … & (x1≠xn) & (x2≠x3) & … & (xn-1≠xn)
Рассмотрим ее конечноаксиоматизируемые подтеории; можем считать, что в набор аксиом входят все аксиомы абелевой группы и сколько-то аксиом Ck. Моделью такой подтеории является циклическая группа <Zn,+> вычетов по модулю n с операцией сложения (остатки от деления на n) при достаточно большом n. Каждая такая модель является конечной, причем эти модели не вложены друг в друга (достаточно брать простые n). Получается, что из нашего знания бесконечного числа моделей (вернее - умения их построить), ни одна из которых не является моделью анализируемой теории (вся совокупность аксиом Cn говорит о бесконечной группе), вдруг следует существование модели для этой теории. Формально все верно, но здравому смыслу несколько противоречит.
Дальше - больше. Теми же рассуждениями мы можем доказать, что теория конечных абелевых групп неаксиоматизируема. Докажем от противного: пусть есть набор аксиом P1…Pm, утверждающий конечность группы. Добавим их к рассмотренной выше теории. Теперь можем считать, что каждая ее конечноаксиоматизируемая подтеория содержит не только все аксиомы абелевой группы, но и новые аксиомы «конечности». Все рассмотренные модели подтеорий являются конечными, так что удовлетворяют и новым аксиомам. Но тогда по теореме компактности получается, что заведомо противоречивая теория имеет модель (аксиомы P1…Pm не совместимы с бесконечным набором аксиом Cn)! Полученное противоречие показывает, что свойство «быть конечным» не может быть выражено в аксиомах.
А теперь вспомним алгебру. Из нее известно, что любая конечная абелева группа разлагается в прямое произведение циклических групп <Zn,+>. Т.е. мы все-таки имеем конструкцию стандартной модели, т.е. теорию конечных абелевых групп, которую, в то же время, не можем аксиоматизировать. Если это не противоречие, то парадокс во всяком случае. От чего-то стоит отказаться: либо от неформально понимаемой конечности, которая и дает возможность установить общую структуру произвольной конечной абелевой группы, либо от теоремы Гёделя (Левенгейма-Сколема, теоремы компактности…), которые слишком вольно трактуют существование - откуда я знаю, что доказав существование методами формальной логики, я не опровергну его, исходя из неформально постигаемых понятий конечного и бесконечного? Опровергли же мы формально доказанное несуществование.
Прежде, чем перейти к рассмотрению существования, проанализируем понятие конечного. Мы видели, что аксиоматически свойство конечности выразить нельзя, но почему-то можно выразить свойство бесконечности (мы с успехом это сделали). Нетрудно понять, почему так: бесконечность мы смогли выразить через бесконечное число аксиом, т.е. на самом деле мы его не выразили, мы его указали явно. Что значит «явно»? Разве мы выписали все эти аксиомы? Нет, мы указали способ их построения и, по сути, апеллировали к имеющейся у каждого человека интуиции конечного, или, если угодно, к интуиции натурального числа. Натурального, сиречь природного - само название говорит больше, чем любые объяснения. Интуиция бесконечного хорошо выражается словами «и так далее» - т.е. речь идет о собрании однородных элементов (это может быть как потенциальная бесконечность с возможностью продолжать некий процесс, либо актуальная бесконечность, где все элементы ее в каком-то смысле сходны, неразличимы). Получается, что математические объекты в некотором роде антропоморфны - они зависят от способов нашего мышления. В теореме компактности явно используется свойство конечности логического вывода. Да, так мы умеем мыслить. Но почему невозможно допустить, что бог, несоизмеримо превосходящий человека, умеет одновременно учитывать бесконечное количество условий? Вдруг то, чего мы не можем помыслить, одновременная взаимосвязь бесконечного числа утверждений, не возможна в природе, хотя любое конечное их сочетание вполне реализуемо? Это ограничение нашего разума, антропоморфизм. Получается, что вроде бы наиболее абстрактная область - формальные теории - оказывается очень зависящей от человека.
В дальнейших рассуждениях, говоря о боге, я имею в виду математического бога, который способен на бесконечность, может проделать до конца некоторый бесконечный процесс, выявить все логические следствия. Но он не знает то, чего невозможно вычислить, так что китайский тест на привидения он не пройдет. Также он не имеет никаких нравственных обязательств перед человеком, без чего не обошлись философские построения Декарта и Беркли. Этого бога можно считать процессом или свойством - мне удобнее мыслить в терминах конструирования, а это предполагает деятеля, того, кто конструирует. Не знаю, как там у бога (или Бога), но для человека это одно из определяющих понятий.
Теперь можем рассмотреть то существование, которое доказывается в теоремах Гёделя и Левенгейма-Сколема, конструкцию лингвистической модели. В этой конструкции одним из важнейших элементов является именно конечность - формул, доказательств, иначе мы бы не смогли построить отношения эквивалентности, и уж тем более модель не оказалась бы счетной. Кстати, формально эта теорема допускает использование несчетных алфавитов (тогда мощность модели будет равна мощности алфавита), но это обобщение явно находится за пределами здравого смысла - наше мышление и счетную-то бесконечность включает как конструкцию, т.е. бесконечный алфавит понимается в конечной кодировке (обычно кванторы, знаки операций, индивидные константы и бесконечное количество переменных x1,x2…xn… - сама эта запись и является необходимой кодировкой с условием, что индексы записаны в десятичной системе). Как же мы можем осмыслить алфавит, который мы не в силах удержать в памяти целиком, да еще и не можем обозримо закодировать его отдельный символ? Что бы там ни было с алфавитом, конечность конструкций из него явно указывает на их антропоморфность. Поэтому можем поиграть этой антропоморфностью и посмотреть, как изменится само понятие их существования.
Формальные доказательства можно представить в виде своеобразной игры: первый игрок (назовем его «Утверждающий») выписывает некое утверждение (гипотезу) или шаг логического вывода, т.е. формулу, получаемую из ранее им выписанных по какому-либо правилу вывода. На каждый шаг первого игрока второй игрок («Опровергающий») выписывает конечное число формул, образующихся из ранее написанных любым из игроков по какому-либо правилу вывода. Цель Утверждающего: выписать в конце концов требуемую формулу, теорему. Цель Опровергающего: вывести противоречие, заведомо ложное высказывание. Будем считать, что последний ход всегда у Опровергающего, и если он достиг своей цели, то он победил. Позиции игроков асимметричны - Опровергающий может пользоваться плодами трудами обоих игроков, но не имеет права на гипотезы.
В такой постановке игра тривиальна - Опровергающему достаточно иметь только один последний ход, чтобы опровергнуть доказанную теорему, если это вообще возможно. Попробуем немного модифицировать игру: пусть не только Утверждающий, но и Опровергающий выписывает только по одной формуле за ход. Теперь игра стала «на время», кто быстрее успеет: Утверждающий доказать, или Опровергающий найти противоречие? Понятно, что такая модификация увеличила шансы Утверждающего на победу. Но доказал ли он что-нибудь, имеет ли его теорема какой-либо математический смысл?
Для этого подумаем: а уверены ли мы, что арифметика в аксиоматике Пеано непротиворечива? Вопрос не математический, а философский. Вроде как уверены (см. цитированное выше высказывание Кронекера), но вполне может оказаться, что она противоречива, но всего вещества вселенной не хватит для записи вывода противоречия. Т.е. практически она непротиворечива, если противоречие и есть, мы никогда с ним не столкнемся. Пусть противоречие есть, тогда есть минимальный по длине вывод этого противоречия (длину вывода считаем в количестве формул, а не символов). Но тогда любой формальный вывод, имеющий меньшую длину, не может приводить к противоречию и полученный результат верен. К примеру, в теории чисел многое зависит от гипотезы Римана о нулях дзета-функции. Предположим, что мы каким-то способом смогли доказать следующее утверждение: «Формальный вывод доказательства или опровержения гипотезы Римана содержит не менее 1020 шагов (формул)». (интересно отметить, что такие утверждения мы можем делать даже относительно недоказуемых формул - для отсутствующего доказательства годится любая нижняя оценка) Для практического использования этого утверждения нам остается только оценить длину формальной записи доказательства, занимающего N страниц статьи. Думаю, что оценка 100*N2 вполне разумна. Итак, если неформальное доказательство какого-либо факта, использующего гипотезу Римана, занимает не более 109 страниц, то оно верно и этот факт доказан самым строгим образом (если строго доказаны использованные оценки). Миллиард страниц - это не так много: в данном случае надо брать не объем конкретной статьи, а объем всех математических текстов, поскольку эта конкретная статья неявно использует доказанные в них факты (возможно использует). Теперь мы можем добавить аксиому: «Гипотеза Римана верна» (или противоположную аксиому, но не обе сразу), чтобы практически работать в непротиворечивой математике.
Математика, конечно, очень преобразится при использовании такого рода доказательств. Главная загвоздка в том, что мы не умеем оценивать снизу сложность задач, исключения можно перечислить по пальцам: нижняя оценка Бардзиня для распознавания симметрии слова N log(N), оценки сложности распознавания слов и разрешения логических теорий Мейера-Рабина-Сейфераса - вот, практически, и все. Причем если оценка Бардзиня выполняется для «почти всех» слов, то во втором случае доказывается существование слов, на которых алгоритм будет работать не менее чем exp(exp(…(exp(N)…)) шагов. Для общей постановки задачи - определить минимальное время работы при конкретных начальных данных - никаких способов решения не известно, хотя данная задача имеет огромное практическое значение - в криптографии, к примеру. Общее состояние дел с нижними оценками практической сложности чего бы то ни было хорошо описывает цитата из книжки Г. Линдгрена «Занимательные задачи на разрезание»:
В отдельных (увы, очень редких) случаях можно строго доказать, что используемое число разрезов минимально. В некоторых случаях (тоже немногочисленных) у нас есть уверенность в этом, хотя строгое доказательство и отсутствует. Во всех же остальных случаях вполне возможно, что вам удастся найти лучшее или даже качественно новое решение.
Но оставим в стороне практическую осуществимость построения таких нижних оценок сложности доказательства, посмотрим, что вытекает из самого факта их наличия. Прежде всего, появляется некоторая временность существования - при неограниченном продолжении, которое за пределами человеческих сил, но вполне вообразимо, мы можем придти к противоречию и все то, что казалось существующим, таковым быть перестанет. К примеру, в доказательствах мы исходили из верности гипотезы Римана, а она оказалась не верна. Все факты, доказанные за меньшее время, остались верными, но при дальнейшем использовании могут оказаться несовместимыми друг с другом. С точки зрения бессмертных богов это, конечно, не существование - но ведь с их точки зрения и игры в шахматы не существует. Известно, что любая конечная игра имеет выигрышный (или беспроигрышный) алгоритм - что же останется от игры в шахматной партии двух богов? Для любой игры необходима неопределенность, а она тут отсутствует.
Самое интересное, что теорема Гёделя о полноте доказана как раз с позиции бога - в ее доказательстве мы используем разбиение всех формул на классы эквивалентности, что предполагает транзитивность: A=B, B=C, тогда A=C. То есть прямое использование такого принципа предполагает, что длина доказательства последнего равенства равна сумме длин доказательств первого и второго равенств. Пока мы на точке зрения бога, т.е. не ограничены по длине используемых доказательств, то все нормально. Если же мы говорим, что можем использовать только «короткие» доказательства, то последнее равенство может оказаться недоказуемым и нам просто не из чего будет стоить лингвистическую модель непротиворечивой теории. Изменилась непротиворечивасть, изменилось и существование.
Вернемся снова к нашей игре. Это ведь конкурентная игра. Почему цели Утверждающего и Опровергающего должны быть противоположны? Переводя на язык математики: почему из противоречия следует все, что угодно? Неужели нельзя поставить себе иные, неконкурентные цели? Как на пикнике играют в бадминтон - цель подольше удержать воланчик в воздухе, кооперативная цель. Сопротивление тут выносится вовне - ветер или просто неуклюжесть. В математике, декларирующей работу с абстрактными объектами, этому «вне» неоткуда взяться, поэтому противоречие в ней подобно сверхтекучей жидкости - в самую маленькую дырочку пролезет и все отравит. В физике все иначе - есть внешняя среда, сама Природа, Реальность - которая и дает достаточно сопротивления для кооперации в игре. Физики делают странные вещи - хотя бы фейнмановское суммирование по всем траекториям частицы. Насколько я знаю, до сих пор не найдено непротиворечивого математического формализма. Но те противоречия, что есть в формализмах - откуда у нас есть уверенность, что они возможны в Реальности? Мы построили математического монстра - почему мы уверены, что возможен ему соответствующий реальный объект? Физики не уверены и потому вполне спокойно относятся к некоторым противоречиям (отнюдь не ко всем!). Есть у них некое чувство физического смысла, и некоторые конструкции им не обладают. С логической точки зрения действия физика можно описать правилом: «Строить только такие доказательства, при которых не возникает противоречия». Некий путь ведет к противоречию - так запретим такой способ доказательства! Эти доказательства уже не формализуешь - вместо конечного набора правил вывода, в которые можно подставлять любые допустимые выражения, мы имеем еще кучу ограничений - так нельзя, и так нельзя (не имеет физического смысла), а почти таким же способом - можно. На языке логики это уже не математика, а метаматематика - в физике они оказываются перемешанными. Физические рассуждения обладают достаточно большой вязкостью (если воспользоваться метафорой текучести), т.е. нам не требуется заделывать дыры полностью, достаточно, чтобы именно эта жидкость через них не лилась. В начале этой статьи я говорил о боге, который может учитывать бесконечное количество условий - в физике это бесконечное количество ограничений. Я не уверен, что это может быть выражено какой-либо математизированной физической теорией, так что они обречены сменять друг друга.
Должна ли, в самом деле, непротиворечивость быть гарантирована на веки вечные или же мы можем не предпринимать без надобности никакой ревизии формализма до тех пор, пока в нем фактически не появится противоречие? Математику такое отречение дается с трудом. Физик работает с физическими законами, которые подтверждаются тем, что находятся в соответствии со всеми известными физическими явлениями. Для него само собой разумеется, что он должен быть готов к тому, что однажды, в силу каких-то новооткрытых фактов, эти законы будут отброшены.
Г. Вейль «О символизме математики»
Итак, в результате мы имеем целый спектр разных существований: существование с точки зрения математического бога (то существование, которое использует математика), существование с наложением бесконечного числа разнородных условий (так по теореме Линденбаума можно расширить любую формальную теорию до полной и как-то так должна существовать Реальность), а также целый спектр временных существований по типу физических теорий. Есть и не охваченные предыдущими рассуждениями социологические реальности: можно ли утверждать, что в 50-х годах у США существовало намерение сбросить атомную бомбу на СССР? Похоже, что единственное, что можно сказать о таком существовании, выражается законом У.А. Томаса: «Если люди определяют ситуации как реальные, они реальны по своим последствиям».
Общий вывод тривиален: нет какого-то единого (математического) существования, и все виды существования в какой-то мере антропоморфны. Если же мы верим в Бога (уже не математического, который создал мир познаваемым для человека - это уже не математическое утверждение), то стоит принять утверждение Кронекера, что целые числа созданы Богом, и на этом строить остальную математику. Кажется, в основном математики так и делают.
В заключение хотелось бы проиллюстрировать два описанных выше способа рассуждения на нематематическом материале.
Итак, короткие верные выводы при длинном доказательстве противоречия. В принципе, этому соответствует движение к недостижимой цели - вопрос лишь в том, успеет ли появиться что-то полезное до того, как противоречивость окажет свое разрушающее влияние. А вот и достаточно большая цитата из философского текста, примечательная именно обоснованием проводимых рассуждений:
Не будем спорить сейчас, возможно ли чистое искусство. Очень вероятно, что и нет; но ход мысли, который приведет нас к подобному отрицанию, будет весьма длинным и сложным. [...] Даже если чистое искусство и невозможно, нет сомнения в том, что возможна естественная тенденция к его очищению. Тенденция эта приведет к прогрессивному вытеснению элементов «человеческого, слишком человеческого», которые преобладали в романтической и натуралистической художественной продукции. И в ходе этого процесса наступает такой момент, когда «человеческое» содержание произведения станет настолько скудным, что сделается почти незаметным. Тогда перед нами будет предмет, который может быть воспринят только теми, кто обладает особым даром художественной восприимчивости. Это будет искусство для художников, а не для масс.
Хосе Ортега-и-Гассет «Дегуманизация искусства»
Второй пример - использование способа рассуждений, при котором стараются избегать путей, ведущих к противоречию. Любую компьютерную программу можно рассмотреть как некоторую формальную теорию, а действия пользователя - как написание формул и совершение логических преобразований (я не готов описывать это как формализм, примем как иллюстрацию). Логично определить противоречие как ситуацию, когда программа отказывается работать или дает очевидно неверный результат. Ошибка в программе, она должна быть устранена. Но ошибки нельзя устранять слишком часто: во-первых, это дорого, а во-вторых, исправление одной ошибки может повлечь появление других, так что это еще и опасное дело, требующее времени и аккуратности. Но работать-то надо, поэтому часть ошибок можно устранить на уровне инструкций пользователям: не делайте того-то, а вот это делайте только таким, а не вроде как эквивалентным способом (последний приведет к сбою). Т.е. пользователь сам старается достигнуть цели, не получив по пути противоречия. При более общем взгляде в этой позиции можно опознать саму установку техники как способа действия в мире, направленного на получение запланированного результата, а не на получение нового знания о мире. Ходить по тропам или прокладывать их - различие техники и науки.