В FOM я решил не писать, так как, перечитав архивы, обнаружил что Torkel Franzen сделал это раньше меня и куда удачнее (лаконичнее). Ещё раз перечитал статью Floyd & Putnam и окончательно убедился, что лажа.
Стоит, однако, обратить внимание на разные варианты доказательства теоремы Гёделя, путаница между которыми часто приводит к печальным последствиям. Виттгенштейн, например, пересказывает неформальный семантический аргумент, при этом не понимая различия между семантикой и синтаксисом и не сознавая (тут кроется ирония), что семантика тут и не нужна на самом деле.
Update: вместо небольшого рассуждения о видах доказательств теоремы Гёделя у меня вышло что-то вроде введения в саму теорему и её доказательство. Всё это под элжекатом, вопросы и поправления (если где-то что-то забыл или перепутал) принимаются.
Можно различить три разных доказательства первой теоремы Гёделя о неполноте. Они доказывают несколько разные вещи и исходят из несколько разных предпосылок.
Пусть у нас есть некая формальная система T, т.е. некий набор аксиом, из которых мы, пользуясь фиксированных набором правил перехода и общелогических аксиом, можем доказывать какие-нибудь теоремы. Поставим несколько условий: пусть, во-первых, наша система T будет сформулирована на языке арифметики. Это значит, что формулы аксиом и теорем в T, кроме общелогических символов (таких, как переменные, скобки, ∧ "и", ¬ "не-" и прочие логические операции, знак равенства =, а также кванторы существования ∃ и всеобщности ∀) могут содержать такие символы, как 0 (константа), + (бинарная операция), * (ещё одна операция), < (отношение "меньше, чем"), S(x) (функция, обозначающая "следующий за x элемент", т.е. x+1). Во-вторых, пусть система T будет достаточно мощной, что в нашем случае значит, что она умеет доказывать некоторые достаточно простые формулы отношений между натуральными числами (подробности я опускаю). Например, если мы не внесём вообще никаких аксиом в T, то она ничего нетривиального не сможет доказать, т.е. будет недостаточно мощной и теорема Гёделя к ней относиться не будет. Но любой достаточно полный список аксиом арифметики (например, перечисляющий обычные тривиальные свойства операций умножения и сложения, отношения < и функции S(x)) оказывается достаточно мощным для наших целей. В-третьих, система T должна быть в некотором техническом смысле "легко описываемой" — в ней должно быть либо конечное количество аксиом, либо бесконечное, но описываемое с помощью какого-то заранее известного алгоритма. Любую формальную систему, отвечающую этим трём условиям, назовём подходящей (это не стандартная терминология, просто для удобства только в этой записи).
С точки зрения формальных доказательств система T не имеет "семантики", иными словами, смысл используемых в ней символов нам безразличен. Формальное доказательство есть всего лишь некоторая длинная цепочка строк, в которой каждая строка есть аксиома T, общелогическая аксиома, или получена из предыдущих строк применением одного из разрешённых правил перехода. Мы обозначили, скажем, одну из операций языка арифметики символом *, потому что она соответствует нашему пониманию умножения; но с точки зрения формальной системы T * — всего лишь символ, который ничего не означает. Вместо него мог быть любой другой символ, скажем, %, и все доказательства оставались бы в силе; просто если бы мы захотели определить смысл аксиом или доказываемых нами теорем, нам пришлось бы понимать % как "умножение".
Сказать, что какое-то утверждение доказуемо в T — значит сказать, что есть некоторое формальное доказательство, которое к нему приводит. Доказуемость — синтаксическое свойство, а не семантическое. С другой стороны, сказать, что какое-то утверждение истинно — значит, сказать, что если мы интерпретируем его согласно обычной интерпретации символов T (т.е. * будем понимать как "умножение", символ 0 — как число 0, итп.), то получаем истинное утверждение о натуральных числах.
Доказуемость необязательно влечёт истинность. Предположим для простоты, что для каждого натурального числа n в нашем языке есть константа n, позволяющая "говорить" о числе n в формулах нашего языка (на практике мы можем "симулировать" такие константы, не объявляя их, с помощью цепочки терминов: 0, S(0), S(S(0)), S(S(S(0))) итп.). Теперь возьмём формальную систему T, в которой есть следующая аксиома: 2+2=5. Тогда утверждение
"2+2=5" доказуемо в системе T (т.к. оно даже является аксиомой), но, естественно, ложно (является ложным утверждением о натуральных числах).
Есть формальные системы, которые доказывают только истинные утверждения. Таковы системы, в которых все аксиомы — истинные утверждения (можно доказать, что тогда все правила перехода между аксиомами сохраняют истинность). Такие формальные системы называются корректными.
Формальная система называется консистентной, если она не может доказать одновременно какое-то утверждение и его отрицание, т.е. доказать противоречие. Неконсистентная формальная система — это плохо и практически бесполезно, т.к. можно легко показать, что из доказательства противоречия можно получить доказательство чего угодно. Неконсистентная формальная система доказывает вообще любое утверждение, так что ничего интересного в ней нет.
Если система корректна, то она автоматически консистентна: ведь она доказывает только истинные утверждения, а какое-то утверждение и его отрицание не могут одновременно быть истинными: одно из них будет истинным, а другое ложным. Заметим, однако — это важно! — что "консистентность", как и "доказуемость" есть свойство синтаксическое, не зависящее от смысла формул и их интерпретации; а вот корректность системы есть свойство семантическое, требующее понятия "истинности".
Наконец, формальная система называется полной, если для любого утверждения φ она может доказать либо φ, либо ¬φ ("не-φ"). Доказательство ¬φ называется также опровержением φ ; таким образом, полная система может либо доказать, либо опровергнуть любою утверждение. В некотором смысле она "на все вопросы даёт ответ". Что ни скажешь про натуральные числа — она сможет либо доказать это, либо опровергнуть. Это свойство полноты — тоже синтаксическое, не пользующееся понятием "истинности".
Теперь мы можем определить три формулировки теоремы Гёделя о неполноте следующим образом:
1. Пусть T — "подходящая" (см. выше) формальная система, и предположим также, что T — корректная система. Тогда множество утверждений, которые T может доказать, и множество истинных утверждений не совпадают (а так как все доказуемые с помощью T утверждения истинны, отсюда сразу следует, что есть истинные утверждения, недоказуемые в T).
2. Пусть T — "подходящая" формальная система, и предположим опять, что T корректна. Тогда мы можем построить конкретное утверждение G (называемое "гёделевым утверждением"), обладающее следующим свойством: G истинно, но недоказуемо в T.
3. Пусть T — "подходящая" формальная система, и предположим, что T консистентна. Тогда T не является полной системой, т.е. существует утверждение G такое, что T не может его ни доказать, ни опровергнуть; более того, мы можем построить такое конкретное G (называемое "гёделевым утверждением").
Неполнота системы T утверждается в качестве результата только в третьей версии, но легко видеть, что она сразу следует из заключения и в первых двух версиях. В них мы заключаем, что существует какое-то истинное, но недоказуемое утверждение. Такое утверждение T не доказывает, но и опровергнуть его — доказать его отрицание — она не может, т.к. его отрицание ложно, а T (в первых двух вариантах теоремы) корректна и доказывает только истинные утверждения. Поэтому T не может ни доказать, ни опровергнуть такое утверждение G и, следовательно, T неполна.
Но вот что действительно отличает первые две версии от третьей: условие теоремы. В первых двух версиях от системы T требуется быть корректной; в третьей версии она должна быть всего лишь консистентной — намного более слабое требование. Есть бесчисленное количество консистентных, но некорректных систем. Ещё более важен тот факт, что и в условии, и в заключении третьей версии теоремы используются только синтаксические понятия, не требующие понятия "истинности", не требующие семантики. Третья версия теоремы и есть та, которую первоначально доказал Гёдель в начале 30-х годов прошлого века.
(если быть совсем точным, формулировка Гёделя включала дополнительное синтаксическое условие для теории T, называющееся w-консистентностью (произносится "омега-консистентность"). Однако через пять лет после публикации статьи Гёделя Россер доказал, что от этого условия можно избавиться и достаточно одной консистентности)
То, что в самой сильной и общей своей формулировке теорема Гёделя не накладывает на T никаких существенных семантических условий, и заключение её тоже вполне синтаксично — это очень важно понять. Важно не только и не столько потому, что иногда мы хотим применить теорему Гёделя к некорректным системам, хоть и это тоже верно. Важно в основном по следующим двум причинам.
Во-первых, первая теорема о неполноте Гёделя используется в доказательстве второй теоремы о неполноте Гёделя, которая доказывает, что "подходящая" (в несколько другом, но схожем с описанным выше, смысле) формальная система T не может доказать собственную консистентность, если она консистентна (если она неконсистентна, то она может доказать всё что угодно, включая собственную консистентность, как ни парадоксально это звучит). Я не буду вдаваться в подробности, но замечу лишь, что в процессе доказательства второй теоремы о неполноте необходимо показать, что доказательство первой теоремы о неполноте можно формализовать внутри системы T. Иными словами, не просто "если T консистента, то она неполна" (третья версия первой теоремы о неполноте, см. выше), но также это утверждение (точнее, его арифметический аналог) можно доказать в самой системе T. Но в то время, как можно формализовать "внутри" системы T такие понятия, как "формальная система", "консистентность" и "полнота", оказывается, что понятие "истинности" формализовать внутри T невозможно в принципе. Поэтому первый и второй варианты теоремы Гёделя, хоть они и более просты для доказательства, не могут быть использованы для доказательства второй теоремы Гёделя.
Во-вторых, теорема Гёделя о неполноте применима не только к формальным системам, сформулированным в языке арифметики (т.е. говорящим о натуральных числах), но также к бесчисленному множеству других формальных систем, от которых требуется только, чтобы они были "подходящими" в нужном техническом смысле; главное требование здесь — чтобы они были не менее мощными, чем теория T в языке арифметики, для которой мы собственно доказываем теорему Гёделя, а это требование обеспечивается возможностью интерпретировать T в такой новой теории. Например, формальная система ZFC, используемая для формализации теории множеств, а вместе с ней и практически всей современной математики, намного более мощна, чем какая-нибудь простенькая арифметическая T, для которой мы доказали теорему Гёделя; этот факт можно строго описать (предъявив интерпретацию, т.е. способ перевести утверждения из языка T в утверждения языка ZFC, и показав, что ZFC тогда доказывает "перевод" всех аксиом T) и из него тогда будет следовать, что и ZFC тоже неполна, т.е. в ней тоже есть какое-то гёделево утверждение G, которое нельзя ни доказать, ни опровергнуть.
Проблема, однако, в том, что в отличие от арифметических формальных систем, для утверждений которых у нас всегда есть удобный и обычный способ определить их истинность (посмотреть на то, верны ли они как утверждения о натуральных числах), для других формальных систем, таких, скажем, как ZFC, понятие истинности вообще не определено или определено очень плохо. Для них первая и вторая версии теоремы Гёделя оказываются неподходящими именно потому, что эти версии опираются на корректность данной системы и на существование определённого понятия истинности утверждений. Подходит только третья, чисто синтаксическая версия.
Виттгенштейн в своём высказывании о теореме Гёделя пересказывает неформальный аргумент, подходящий как раз ко второй версии теоремы, сформулированной выше. Такой неформальный аргумент — "найдём утверждение G, которое выражает собственную недоказуемость; тогда она должно быть истинным, т.к. если бы было ложным, то было бы доказуемым, но корректная система T не доказывает ничего ложного; а раз G истинно, то оно действительно недоказуемо, как оно и утверждает" — есть, пожалуй, самое часто используемое неформальное "объяснение" теоремы Гёделя, но важно понять, что оно описывает относительно слабый и намного менее важный вариант этой теоремы. Преимущество этого варианта в том, что его значительно легче доказать и легче понять (например, с помощью такого неформального аргумента).
О том, как различаются доказательства трёх вариантов теоремы Гёделя.
Главный "фокус", который придумал Гёдель, заключается в том, что можно перенести обсуждение формальных систем на язык арифметики, закодировав с помощью натуральных чисел логические символы. Тогда у каждой формулы будет свой номер, какое-то число, соответствующее только этой формуле, а операции с формулами (например, подстановка числа вместо переменной внутри формулы) станут операциями с числами, которые можно будет в свою очередь описать с помощью формул. Тогда можно будет построить формулы, которые в некотором смысле будут утверждать что-то о себе самих (они будут утверждать что-то о числах, являющихся на самом деле кодами их самих).
Сначала мы фиксируем некоторую гёделеву нумерацию, ставящую в соответствии любой формуле нашего языка натуральное число (подробности опускаю). Условимся обозначать число, соответствующее формуле φ, через [φ]. Если φ — это формула, например, "(∀x)(∃y) x+y = 0", то [φ] — это какое-то число, однозначно эту формулу кодирующее (например, 123249432943245). Потом мы проводим процесс арифметизации, сопоставляющий операциям с формулами и списками формул (формальное доказательство можно представить в качестве конечного списка формул) операции с числами. После долгого процесса такой арифметизации мы приходим, например, к следующему: мы получаем некоторую формулу Provable(x) , зависящую от одной переменной, и обладающей следующим свойством:
(*) Утверждение φ доказуемо в системе T тогда и только тогда, когда утверждение Provable([φ]) истинно.
Таким образом, мы связали доказуемость какой-то формулы с истинностью какого-то утверждения о натуральных числах, если в него подставить номер этой формулы.
Вспомним, что наша система T корректна (мы сейчас доказываем первую и вторую версии теоремы Гёделя). Обозначим через Pr множество номеров всех доказуемых в системе T утверждений, а через Tr — множестве номеров всех истинных утверждений на языке арифметики. Заметим, что Pr и Tr — множества не формул, а номеров формул, т.е. множества натуральных чисел. Pr — подмножество Tr, т.к. система корректна.
Мы только что показали, что для множества Pr есть формула Provable(x), так что число n принадлежит множеству Pr тогда и только тогда, когда Provable(n) истинно. Если для какого-то множества натуральных чисел X выполняется такое условие — т.е. есть какая-то формула E(x), которая выражает X в том смысле, что E(n) верно тогда и только тогда, когда n находится в X — тогда такое X называется выразимым множеством. Мы только что показали, что Pr — выразимое множество. Но можно довольно легко доказать, что Tr — невыразимое множество; иными словами, множество истинных утверждений не поддаётся выражению с помощью формулы. Это так называемая теорема Тарского, красивая и полезная, но далеко не столь глубокая, как теорема Гёделя.
Если множество Pr можно выразить, а Tr нельзя, значит, они не совпадают. Значит, и исходные множества формул (доказуемых и истинных) тоже не совпадают. Мы доказали первую версию теоремы Гёделя. Это самый быстрый путь к доказательству хоть какой-нибудь версии теоремы Гёделя.
Доказательство второй версии сложнее, но ненамного. Пользуясь формулой Provable(x), мы можем сконструировать утверждение G, обладающее следующим свойством: G истинно тогда и только тогда, когда ¬Provable([G]) — т.е. тогда и только тогда, когда нет формального доказательства G в системе T. Далее мы пользуемся несколько более точной формулировкой неформального аргумента, приведенного выше, и заключаем, что G истинно, но недоказуемо.
А вот для доказательства третьей версии надо немного больше попотеть. Дело тут в том, что в ней мы не используем понятий "истинности" и "корректности", а работаем только с "бессмысленными" формулами; поэтому такое определение
(*) Утверждение φ доказуемо в системе T тогда и только тогда, когда утверждение Provable([φ]) истинно.
надо заменить на, скажем, следующие два свойства другой формулы Proof(x,y):
(**)
Если последовательность формул Φ является доказательством утверждения φ в системе T, то T доказывает утверждение Proof([Φ], [φ]).
Если последовательность формул Φ не является доказательством утверждения φ в системе T, то T опровергает утверждение Proof([Φ], [φ]).
Иными словами, вместо истинности каких-то утверждений нам надо показать, что они доказуемы в системе T (вовсе необязательно корректной к тому же). Это тяжелее сделать, и требует намного более тщательного внимания к техническим мелочам (которые я все здесь опускаю). В частности, формула Provable(x) оказывается слишком "сильной", система T не может в общем случае доказать все её свойства, поэтому нужно подойти к этому осторожнее и использовать формулу Proof(x,y). (формулу Provable(x) можно потом определить так: Provable(x) = (∃y)Proof(y,x) — т.е. "существует такое y, которое является кодом доказательства формулы с кодом x" — и использовать это определение в процессе доказательства).
После того, как мы построим формулу Proof(x,y) и её друзей, мы получаем гёделево утверждение G примерно тем же способом, что и раньше, но теперь мы доказываем не то, что G "истинно, но недоказуемое" (истинность для нас в этом варианте теоремы — табу), а то, что G "недоказуемо и неопровержимо", из чего следует, что T — неполная система. Этот факт опять-таки доказать несколько тяжелее, чем в случае первых двух версий теоремы, где можно было опираться на "истинность" — но уже не слишком тяжело после всей проведенной предварительной работы.
