Гедель 3
1
2
3
4
5
6
7
VIII. Машина доказательств
ФСС элементарной арифметики (ФСЭА), как мы уже знаем, производит строки, интерпретируемые как утверждения арифметики. Она содержит аксиомы, начальные верные строки, и выводит новые строки - теоремы. Мы не будем рассматривать конкретные аксиомы 8 и правила вывода новых строк из уже выведенных; нам достаточно помнить, что они заданы. В алфавит ФСЭА входят символы для кодирования чисел и переменных, операции + и ×, сравнение =, скобки, кванторы существования E и всеобщности A (мне придется обозначить их латинскими буквами из-за типографских ограничений), и логическое отрицание ~. Числа кодируются в такой же «единичной» системе, какую мы уже рассматривали, количеством «звездочек». Так же кодируются и переменные, только начинаются они со специального символа переменной x: вместо x, y, z, a, b система выдает x•, x••, x••• и т. д. В примерах ниже мы, однако, будем записывать числа в десятичной записи, а переменные буквами.
Примеры утверждений, которые выводит ФСЭА:
Ex:x×2=6
Здесь говорится, что число 6 четно (найдется такое число x, что 2×x=6)
~Ex:Ey:(x+1)×(y+1)=13
13 простое число: не существует таких x и y, что (x+1)×(y+1)=13. Прибавление единицы требуется, чтобы каждый сомножитель был больше 2 9.
Ax:Ea:~Eb:Ec:(x+a)=(b+1)×(c+1)
Здесь утверждается, что существует бесконечно много простых чисел. Следует читать это так: для любого x найдется a такое, что не существует таких b и c, чтобы равенство (x+a)=(b+1)×(c+1) выполнялось. Иными словами, для каждого x найдется такое a, что (x+a) будет простым числом. Поскольку a>0, то и x+a>x: какое число x ни возьми, найдется простое число, еще большее.
В образовании смысла строк мы следуем правилам, которые мы же сами установили для их интерпретации. Например, «~» мы читаем «неверно, что», A как «для всех», E как «для одного или более», «:» как «верно следующее:», и так далее. Тогда утверждения, выводимые ФСЭА, становятся теоремами. Являются ли они «истинными»? Здесь нужно задуматься о понятии истинности.
Мы изначально полагаем аксиомы истинными, верными утверждениями. Их запись в виде строк ФСЭА интерпретируется именно так, как мы того хотим, с тем смыслом, которые мы в них закладывали, когда придумывали эти строки 10. Являются ли истинными в этом смысле и теоремы? Ровно настолько, насколько мы можем доверять формальному механизму вывода, аппарату формальных систем.
На поверхности кажется, что этот механизм работает надежно. Можно увидеть, как выводятся приведенные выше утверждения, которые мы понимаем как верные в арифметике. Но ведь теорем, которые производит ФСЭА, бесконечно много. Поэтому мы должны поставить вопрос «доверия» к нашей механике вывода. В ФСС сложения чисел доказательство было довольно простым, однако, ФСЭА намного сложнее, и ее «правильность» отнюдь не очевидна.
Вопросы касательно ФСЭА, которыми мы зададимся, следующие. Во-первых, нас интересует, все ли возможные теоремы арифметики выведет наша машина? Например, будет ли среди ее строк доказательство Великой теоремы Ферма? Предположения Гольдбаха? Свойство, которое нас интересует, мы назовем полнотой системы: система полна, если она выводит, в интерпретации смысла, все истинные утверждения в некоей области.
Второй, еще более важный вопрос, который нас волнует: не произойдет ли так, что два утверждения, полученных ФСЭА, будут противоречить одно другому? Например, одним путем мы получим утверждение, что предположение Гольдбаха истинно, а другим - что оно ложно. Такое нарушение будет фатальным для всей системы арифметики: из противоречия можно вывести все, что угодно! Это легко показывается в формальной логике. Из такого противоречия следует, что 0=1, что 2×2=5, что простых чисел не существует, что их существует конечное количество, что количество простых чисел бесконечно - все, что пожелаете. Противоречия в выведенных теоремах ни в коем случае быть не должно. Свойство системы не выдавать противоречивых (в интерпретации смысла) утверждений назовем непротиворечивостью.
Является ли элементарная арифметика полной и непротиворечивой теорией? Над этим вопросом работали великие математики начала XX в. Попытка вывести самообоснованность теории множеств тогда потерпела неудачу 11. В ответ на это Давид Гильберт сформулировал в начале 20-х гг. программу по поиску способа вывода всех математических утверждений из аксиом путем механической вычислительной процедуры. Формулировка требований, заданных Гильбертом к аксиомам и процедурам математики, такова: требуется найти (а) процедуру, которая бы выводила все без исключения истинные математические утверждения, и только истинные, из заданного однажды набора аксиом; (б) самый набор этих аксиом и (в) алгоритм доказательства любого наперед заданного утверждения, чтобы определить за конечное время, возможно ли вывести это утверждение из аксиом (в таком случае, оно истинно) или нет (и тогда оно ложно).
Таким образом, Гильберт сформулировал задачу поиска, в наших терминах, полной и непротиворечивой формальной системы арифметики, и дополнил ее требованием конструктивной вычислимости 12принадлежности лексически верной строки множеству синтаксически верных строк.
Над реализацией этой программы математики работали еще 10 лет, до тех пор, пока Курт Гедель не обнаружил фундаментальное свойство формальных систем, которое предопределило неудачу программы Гильберта и невозможность аксиоматизации математики.
IX. Бета-код Геделя
Рассуждение Геделя основано на арифметическом кодировании алфавита, строк и правил ФС. В самом деле, мы можем закодировать алфавит ФС числами. Когда мы это сделаем, правила переписывания строк ФС можно записать в виде арифметических операций над числами. О любом числе можно задать вопрос, является ли это число кодом лексически верной строки в данной ФС. Если ответ на него положительный, далее можно спросить, является ли это число также и кодом синтаксически верной строки. Если да - то мы имеем дело, на семантическом уровне, с кодом теоремы арифметики. Таким образом, выходит, что среди чисел есть подмножество кодов теорем арифметики. Множество всех остальных чисел можно назвать множеством не-теорем арифметики (либо они лексически недопустимы, либо не выводимы системой). Будем называть числа вычислимыми формальной системой, если они выводимы нашей закодированной числами ФС.
Для примера, закодируем нашу первую систему ХИХИ в виде чисел: заменим Х на 1, И на 2, А на 3 13. Начальная верная строка ХИ тогда первращается в число 12. Теперь перепишем на языке чисел правила системы.
1. К любому числу, заканчивающемуся на 2, можно дописать в конец 3. Математически это можно выразить так: если n вычислимое число, и остаток от деления его на 10 равен 2, то 10×n+3 тоже вычислимое число.
2. Любую «подстроку», следующую за 1, можно «удвоить». Операции «взятия подстроки» и «удвоения», разумеется, следует записать арифметически. Пусть наше число содержит в середине или в начале 1 (пример 23132). Часть, заканчивающуюся 1 (231 в примере) запишем как m×10+1, где m≥0 (в нашем примере m=23). Чтобы приписать к этому числу «хвост» (32), умножим его на 10n, где n - длина «хвоста» (у нас n=2, 10n=102=100): (m×10+1)×10n, в нашем примере это будет 23100, а затем просто прибавим «хвост», то есть запишем формулу как (m×10+1)×10n+j, где j обозначает «хвост» (у нас j=32). Чтобы он поместился в отведенное ему разрядное место, мы должны ввести ограничение j<10n. «Удвоить хвост» можно, еще раз умножив результат на 10n и прибавив j. Таким образом, правило (2) можно сформулировать так:
Если (m×10+1)×10n+j, где j<10n, вычислимое число, то и (m×10+1)×10n+j)×10n+j вычислимое число.
Запись правил (3) и (4) в арифметической форме оставим как упражнение читателю.
Все это выглядит чрезвычайно запутанным и искусственным, но нас сейчас не интересует сложность и «неинтересность» этого вывода. Самое главное здесь, что путем формального, механического преобразования можно перейти от записи правил операций над строками к записи правил в виде операций над их кодами, числами. А как только мы переведем описание ФС на язык арифметики, мы сможем сформулировать и задачи, ставящие вопросы об этой ФС, на том же языке арифметики. Например, задача о выводимости ХА переформулируется в таком виде: входит ли число 13 во множество чисел, вычисляемых данной, описанной в виде арифметических действий, ФС?
X. Теоремы Геделя
Ничто не препятствует нам распространить рассуждения о кодах ФС на самое арифметику, вернее, ее формальную систему - ФСЭА. Переписав ее правила в виде арифметических алгоритмов, мы закодируем каждое утверждение, получаемое ФСЭА, натуральным числом.
Что интересного произойдет, когда мы сделаем это? ФСЭА достаточно мощна, чтобы порождать язык арифметики. В тоже самое время, мы переписали ее правила на тот же самый язык! Иными словами, в таком выражении ФСЭА формулирует утверждения о себе. Например, мы можем спросить, входит ли число X во множество чисел-кодов утверждений ФСЭА? Тем самым, мы задаем вопрос, является ли число Х кодом верного утверждения, то есть теоремы, арифметики. Понятно, что число мы можем теперь рассматривать двояко: как собственно число, и как код утверждения о числах.
Гедель доказывает, что возможно (и показывает, как) сконструировать в ФСЭА утверждение «Число G не входит во множество кодов теорем, выводимых ФСЭА», таким образом, чтобы код этого утверждения в точности совпал с самим числом G 14. Каковы последствия существования такого числа?
Попробуем «спросить» арифметику об истинности этого утверждения. Верно ли на самом деле, что число G не входит во множество кодов теорем, выводимых ФСЭА?
Предположим, что ответом арифметики на этот вопрос будет «да». Это означает, что утверждение это выводимо в ФСЭА, а это в свою очередь, означает, что число G, его код, входит во множество кодов выводимых теорем… Но позвольте-ка, ведь если это так, то в арифметике оказывается противоречие: получается, что число G и входит во множество кодов теорем, и не входит в него - результат получается разным в зависимости от пути формального вывода, которым мы идем.
Предположим теперь, что число G, код утверждения о том, что G не является кодом теоремы, и на самом деле не является кодом теоремы. В таком случае, противоречие снимается. Однако, в этом случае арифметика оказывается неполной! У нас есть верное утверждение (о том, что G не является кодом теоремы), которое, хоть и верное, но не входит в число теорем арифметики. Получается тогда, что арифметика «не знает» всех верных утверждений о натуральных числах.
Это рассуждение и является основным в первой теореме Геделя о неполноте. Формулировка этой теоремы была в дальнейшем значительно усилена Россером; когда говорят о теореме Геделя, имеют в виду обычно первую теорему о неполноте арифметики в формулировке Россера.
Обратите внимание, что такое замыкание нашего рассуждения возможно не в любой ФС. Например, утверждения системы ХИХИ не являются таковыми о натуральных числах; строку системы ХИХИ нельзя интерпретировать как «x не входит во множество Z», ведь у нас нет отображения этих строк на утверждения о числах. Кроме того, она не описывает и системы кодирования утверждений на языке, который она производит. Таким образом, ФС, попадающая под обсуждение теоремы Геделя, должна быть достаточно мощна, чтобы выражать, в некоей интерпретации смысла, действия элементарной арифметики. Системы, для которых такая интерпретация в принципе возможна, мы, вслед за Подниексом [2] назовем фундаментальными.
Давайте теперь проговорим суть вывода теоремы Геделя-Россера:
Фундаментальная система теорем, выводимых формальной системой, не может быть одновременно полной и непротиворечивой.
Этот вывод остается верным применительно к любой фундаментальной системе (то есть, с различными наборами аксиом и правил), не только к конкретной ФСЭА. Например, вполне естественно включить G в число аксиом нашей системы. Раз уж мы знаем, что утверждение G истинно, давайте добавим его к списку аксиом нашей ФСЭА. К сожалению, это не снимает противоречия. Сделав это, мы получим другую формальную систему, ФСЭА′, в которой, по теореме Геделя, есть свое геделево число G′. Можно и его добавить к аксиомам ФСЭА′ - мы получим новую систему ФСЭА′′, но и в ней будет свое геделево число G′′ - и так далее до бесконечности.
Разрешения у этой проблемы нет: арифметика не может быть полностью выражена набором аксиом и механических правил вывода, то есть и арифметика, как и теория множеств, не обосновывает сама себя. Открытие Геделя предопределило крах программы Гильберта по поиску самообоснованной, самосовершенной, заключенной самой в себе арифметики - и математики вообще.
Здесь можно увидеть некоторое сходство с геометрией. Изменяя пятый Евклидов постулат о том, что через заданную точку проходит ровно одна прямая, параллельная заданной прямой, мы получим разные непротиворечивые системы геометрии. Существенная разница в том, что геометрия, в отличие от арифметики, не порождает языка, на котором можно выразить аксиомы и правила геометрии. Тем не менее, общая картина арифметического состояния дел нам ясна: имеются некоторые истинные, в смысле более сложных, «внешних» теорий, утверждения, которые не могут быть ни доказаны, ни опровергнуты в арифметике. В то же время, эти внешние теории страдают тем же недостатком: в них имеются свои геделевы утверждения - и так, опять же, до бесконечности. Единой совершенной теории арифметики не существует. Есть более сильные фундаментальные теории и более слабые - например, аксиоматическая теория множеств ZFC сильнее аксиоматической арифметики Пеано в том смысле, что первая доказывает утверждения, недоказуемые в последней, но «абсолютной» фундаментальной теории все-таки существовать не может,
Стоит, для полноты картины, привести здесь, без доказательства или рассуждения, формулировку второй теоремы Геделя о неполноте арифметики:
Если фундаментальная система теорем арифметики, выводимая формальной системой, содержит доказательство собственной непротиворечивости, тогда и только тогда эта система противоречива.
Далее нам следует порассуждать о последствиях результатов, полученных Геделем, для математики, и лишь затем мы рассмотрим различные аргументы о применимости этих результатов к моделям и сущности сознания и мышления.
1
2
3
4
5
6
7
__________________________________
⇧ 8. Множество аксиом ЭА счетно-бесконечно, они тоже выводятся правилами.
⇧ 9. В ЭА рассматриваются натуральные числа, поэтому переменная может принимать значения 1, 2, 3 и так далее. Если x переменная, то (x+1) будет иметь значения 2, 3, 4 - иными словами, 2 или больше.
⇧ 10. Совсем уж строго говоря, и это сомнительно, потому что аксиомы порождаются схемой, и их бесконечно много, поэтому все их проверить нельзя.
⇧ 11. Парадокс, обнаруженный Бертраном Расселом в теории множеств, популярно сформулирован в википедии (англ.) так. Введем признак «нормальности»: нормальное множество не является своим собственным подмножеством. Например, множество всех квадратов нормально, потому что оно само не есть квадрат. Его дополнительное множество, множество всех неквадратов, не нормально, потому что оно само не квадрат и, следовательно, должно включать и себя. Теперь возьмем множество всех нормальных множеств, и зададимся вопросом, нормально оно или нет? Это парадокс. Если мы предположим, что оно нормально, то оно входит само в себя, и, следовательно, не нормально. Если предположить, что оно не нормально, то его не будет среди всех нормальных множеств, и, значит, оно не подмножество себя - то есть, нормально. Противоречие возникает при любом предположении.
⇧ 12. Конструктивной в математическом смысле: требуется не только доказать существование алгоритма, доказывающего теоремы, но и отыскать сам этот алгоритм.
⇧ 13. Бета-код Геделя основан на взаимно-простых числах и формулируется сложнее, но делает дальнейшие доказательства более эффективными. Для наших качественных рассуждений, однако, конкретный способ кодирования не важен.
⇧ 14. Замечательное неформальное описание этого вывода дается в [1], глл. XIII и XIV, а формальный вывод в [2].