Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

ещё о теореме Гёделя

В некотором роде апдейт к записи на прошлой неделе на ту же тему.

В 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 — неполная система. Этот факт опять-таки доказать несколько тяжелее, чем в случае первых двух версий теоремы, где можно было опираться на "истинность" — но уже не слишком тяжело после всей проведенной предварительной работы.
Tags: logic
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 13 comments