В конце раздела VI "Понятие "доказательство" - в быту и математике" предыдущей главы мы назвали "возражающими аксиомами" такие аксиомы, которые не позволяют доказать недоказуемость какого-либо утверждения в данной теории.
Предыдущее предложение выглядит устрашающим, поэтому поясню: если в теории есть "возражающие аксиомы", то она не исключает, что в ней доказано все. Она не "самоуверенна" и придерживается "философского мнения", что "в принципе, всё возможно". И эти "возражающие аксиомы" не позволяют доказать мнение, противоположное данному "философскому мнению". "Не позволяют доказать" - то есть, невозможно доказать в случае, если эта теория непротиворечива.
Напомню, что "доказуемым" может стать все что угодно при соответствующем расширении теории, а внутри исходной теории нет, и не может быть достоверной информации, что эта теория не является частью более широкой теории. Поэтому, если "возражающие" аксиомы способны выразить принцип "расширяемости" теории, то доказать недоказуемость какого-либо утверждения в рамках такой теории станет невозможно.
Но при наличии "возражающих" аксиом нельзя доказать и теорему в духе:
"Нельзя доказать, что недоказуемо утверждение 2*2=5"
Каким же образом "возражающие аксиомы" могут тогда выразить невозможность недоказуемости? Ведь, по сути, недоказуема именно недоказуемость. Но любая теорема о недоказуемой недоказуемости сама была бы утверждением недоказуемости. Появление теоремы (или аксиомы) о недоказуемости приводит к противоречию. Вот этот факт (противоречие из недоказуемости) и должен быть виден из теории с "возражающими" аксиомами. Поэтому аксиомы или теоремы о недоказуемости должны вносить в теорию примерно такой смысл:
Если доказано, что "недоказуемо равенство 0=1", то появиться возможность доказать, что "0=1 доказано".
Но обязательно ли добавлять в качестве "возражающих" аксиом утверждения такого специфического вида для того, чтобы теория отразила принцип расширяемости? Ведь утверждение о недоказуемости утверждения G в рамках теории T - это, по сути, утверждение о том, что всякий вывод (всякое доказательство) в теории T не является доказательством утверждения G.
Примитивная теория не способна делать выводы про свои доказательства. Примитивная теория формируется доказательствами (как и всякая другая теория), но "не понимает", как это происходит. Но давайте рассмотрим такую теорию, которая способна делать выводы о своих собственных доказательствах. Не обнаружится ли в такой теории "возражающей" теоремы?
Ведь такая теорема соответствует реальности, соответствует принципу расширяемости теории и мы вправе надеяться, что в случае более богатого отражения реальности теорией теория тоже начнет выражать принцип расширяемости и сможет доказать подобную "возражающую" теорему. "Поймет", в свете принципа расширяемости, что она не может сказать что-то определенное про все возможные свои доказательства.
Допустим, у нас есть теория, которая в состоянии работать с текстами своих доказательств. И в рамках этой теории можно построить такие функции, которые:
1. Проверяют текст доказательств теории на корректность (т. е. проверяют, что соблюдаются правила логики при выводе очередного утверждения из предыдущих утверждений, начальными утверждениями вывода являются аксиомы);
2. Возвращают текст результата доказательства по тексту самого доказательства;
и т.д.
Какое утверждение нам хочется получить в рамках такой теории в качестве "возражающего" утверждения? Нам необходимо какое-то такое утверждение G (G большое), которое удовлетворяет 4м условиям:
1. Оно выражает недоказуемость какого-то утверждения g (g малое), и если утверждение g будет доказано в рамках данной теории, то это будет означать противоречивость теории;
2. Недоказуемое утверждение g должно противоречить теории, ведь в том и состоит проблема с непротиворечивостью, что нельзя доказать недоказуемость даже того утверждения, которое явно противоречит теории;
3. Само по себе утверждение G истинное, так как выражает принцип расширяемости теории, который соответствует реальности;
4. Противоречие должно строиться на конфликте между доказательством g (если бы оно было проведено) и требованиями к этому доказательству со стороны утверждения G.
Первые три пункта мы "подсмотрели" на предыдущем примере: "Если доказано, что "недоказуемо равенство 0=1", то появиться возможность доказать, что "0=1 доказано"". Четвертый пункт получается из направления нашего поиска - мы рассматриваем теорию, способную выражать свои доказательства и, следовательно, способную формулировать противоречие между своими требованиями к доказательствам и самими доказательствами.
Итак, утверждение G должно конфликтовать с доказательством "подчиненного ему" g. Самый очевидный конфликт и противоречие - отрицание. Вот и возьмем этот наиболее очевидный вариант. Утверждение G должно выражать недоказуемость g. Для достижения противоречия приравняем G и g (тоже самый простой путь) и тогда G должно выражать собственную недоказуемость. Итак, наше утверждение G представляет собой разновидность классического "парадокса лжеца":
"Это утверждение нельзя доказать"
Разумеется, утверждение G не является аксиомой и даже его - как мы увидим - нельзя доказать в рамках той теории, для которой оно будет сформулировано. Но утверждение G соответствует смыслу, который создают аксиомы теории. О чем уже говорилось в текущем разделе: "аксиомы или теоремы о недоказуемости должны вносить в теорию примерно такой смысл".
Теперь займемся технической стороной (на популярном уровне, разумеется). Мы применили ряд упрощений в попытке построить "возражающее" утверждение, и не исключено, что оно окажется негодным. Тогда будем думать, как поправить. Но, может, оно окажется таким, какое нам нужно.
Начнем с того, что в логике нет понятия "это". Может, такое понятие и можно как-то формализовать, но мы (как и логики-математики до нас) решим проблему иначе. Утверждение способно "выписать" свой текст. Или, выражаясь ближе к формальной логике, утверждение может содержать функцию, результатом которой является текст самого утверждения. Чтобы не быть голословным, я составил практический пример. Следующая программа на VBA (Visual Basic for Application) выводит в редакторе Word свой собственный текст:
Sub dolly(): x = ": Selection.InsertAfter (" + Chr(34) + "Sub dolly(): x = " + Chr(34) + " + Chr(34) + Replace(x, Chr(34), Chr(34) + " + Chr(34) + " + Chr(34) + " + Chr(34) + " + Chr(34)) + Chr(34) + x): End Sub": Selection.InsertAfter ("Sub dolly(): x = " + Chr(34) + Replace(x, Chr(34), Chr(34) + " + Chr(34) + " + Chr(34)) + Chr(34) + x): End Sub
Эта программа не имеет механизма обращения к файловой или иной "внешней" сложной системе (как это делают многие компьютерные вирусы), чтобы получить свое "тело" целиком и воспроизвести готовый (изготовленный "снаружи") результат. Поэтому назовем ее условно "компьютерная бактерия". Вирус не "клонирует" себя сам, он поручает это сложным внешним механизмам. Приведенная же программа клонирует себя сама, используя в качестве "внешних" лишь базовые возможности среды (интерпретатора VBA и редактора Word). Базовыми возможностями являются, например, операции присваивания, замены и соединения строк, аналоги которых имеются и в математическом формализме.
Из базовых возможностей среды можно скомбинировать бесконечное множество алгоритмов. Нужную комбинацию компьютерная бактерия несет в себе и воспроизводит самостоятельно. Вирус же обращается к некой внешней комбинации базовых возможностей (например, к весьма сложным механизмам операционной системы, чтобы получить информацию о собственном файле), и эту комбинацию он не воспроизводит. Поэтому вирус нуждаются в наличии "ксерокса" во внешнем мире. И этот "ксерокс", кстати, не только не клонируется, но даже зачастую уничтожается в процессе воспроизводства вирусов. Вот в чем принципиальное отличие между "бактериальным" и "вирусным" механизмами размножения.
Хотя, если бы процесс размножения являлся базовым для мира, тогда вирус принципиально не отличался от бактерии. Тогда, собственно, размножаться могло бы все что угодно. И снежинка, и дом, и куча песка. Но мы знаем, что в нашем мире все что угодно самопроизвольно не размножается. А поэтому между бактерией и вирусом имеется принципиальное отличие. Ни компьютер, ни теория изначально не присутствуют в мире. Но внутри компьютера и внутри теории есть какие-то базовые возможности для "живущих" в них объектов - для программ и формул. И относительно этих базовых возможностей тоже есть свои вирусы и бактерии.
Приведенный простенький пример можно усложнить как угодно. Любой сложный алгоритм можно дополнительно "научить" выписать собственный текст. Не буду углубляться в технику, потому что желающие догадаются и разберутся сами в нюансах, но и без нюансов возможность "клонироваться" довольно очевидна. Этим, например, занимаются самые разные бактерии и не только. Они тоже опираются на среду - используя свойства материи, например.
Итак, с понятием "это" разобрались, более-менее. Теперь разберемся со словами "нельзя доказать".
Понятие "доказательство" довольно легко формализуется. Я уже приводил 2 важнейших пункта такой формализации в начале раздела. Доказательство существенным образом опирается на аксиомы. Поэтому "нельзя доказать" мы раскроем как "нельзя доказать в теории с аксиомами <перечень аксиом>".
Итак, в результате нашего разбирательства из первоначальной "рыбы" "Это утверждение нельзя доказать" мы получили утверждение G такого вида:
"Для утверждения <функция, возвращающая текст данного утверждения> не существует текста доказательства в теории с аксиомами <перечень аксиом>".
Если представить, что утверждение G доказано, то из текста данного доказательства можно сделать текст доказательства отрицания G в рамках T. Действительно, G утверждает отсутствие текста своего доказательства, но раз текст доказательства G предъявлен, то текст доказательства G не отсутствует, и теория T в состоянии "понять" этот факт. А это значит, что в T тогда будут доказаны и утверждение G и его отрицание, что приведет к противоречию.
И гарантировать, что такого противоречия не возникнет, невозможно в рамках T. Действительно, в случае доказательства недоказуемости G (существование текста доказательства недоказуемости) мы докажем недоказуемость G. Но G как раз утверждает свою недоказуемость, G как раз эквивалентно своей недоказуемости. И это тоже "понимает" теория T. Поэтому из текста доказательства недоказуемости G будет получен текст доказательства G (при помощи эквивалентности между G и недоказуемостью G). А наличие текста доказательства G позволит доказать доказуемость G (доказать, что текст доказательства G существует). Доказуемость и недоказуемость G войдут друг с другом в противоречие.
Поэтому, если теория T непротиворечива, то она не может исключить, что в ней доказано G, не может исключить, что в ней имеются - в силу неустранимой угрозы доказуемости G - противоречия. Такова идея доказательства теоремы Геделя, которая утверждает, что теория не может доказать собственную непротиворечивость.
Поэтому, если мы требуем от теории T доказательств в жестком "бытовом" смысле, то такое наше требование оказывается невыполнимым. Напомню, что "бытовой" смысл понятия доказательства включает в себя требование отсутствия противоречий. Об этом было сказано в разделе VI "Понятие "доказательство" - в быту и математике" предыдущей главы. Но Гедель довел свои рассуждения до логического конца. Он показал, что нет даже более слабого доказательства непротиворечивости, которое соответствовало бы логическому смыслу понятия "доказательство".
Поясню разницу между доказательствами непротиворечивости в "бытовом" и логическом смыслах:
Не исключено, что теория может доказать - в логическом смысле - недоказуемость какого-то утверждения. Например, недоказуемость утверждения 0=1. Тогда она может сделать вывод о том, что она непротиворечива - ведь из противоречия следует все (в формальной логике), в том числе 0=1, и поэтому недоказуемость 0=1 означает отсутствие противоречий (непротиворечивость). Такое доказательство недоказуемости не докажет недоказуемость G (иначе возникнет противоречие). Поэтому фактически гарантий от противоречий все равно нет, но формально доказательство недоказуемости утверждения 0=1 можно было бы считать доказательством - в логическом смысле - непротиворечивости теории T.
Каким способом Гедель доказал свою теорему о невозможности даже "слабого" доказательства непротиворечивости внутри непротиворечивой теории, мы разберем через 1 раздел - в разделе IV "Теорема Геделя - "техническая" часть" текущей главы. Но прежде разберем, почему утверждение Геделя (формула G) оказывается "не по зубам" теории T. Формальные объяснения уже приведены, но надо понять по существу, иначе остается впечатление какого-то фокуса.