?

Log in

ещё о теореме Гёделя - Поклонник деепричастий [entries|archive|friends|userinfo]
Anatoly Vorobey

[ website | Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Links
[Links:| English-language weblog ]

ещё о теореме Гёделя [май. 13, 2003|10:02 am]
Anatoly Vorobey
[Tags|]

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

В 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 — неполная система. Этот факт опять-таки доказать несколько тяжелее, чем в случае первых двух версий теоремы, где можно было опираться на "истинность" — но уже не слишком тяжело после всей проведенной предварительной работы.
СсылкаОтветить

Comments:
[User Picture]From: flaass
2003-05-13 12:51 am

Vaaau!

Spasibo, Avva, dobavil mne v golovu nemnozhko porjadka:)
No Witgenstein, dazhe esli b vse eto i prochital i ponjal (a ja vse zhe podozrevaju, chto on vse eto ponimal), iz svoego tupika uxodit' by vse ravno otkazalsa. Ego problema nachinaetsa ran'she: kakoe my imeem pravo govorit' "obychnaja interpretacija simvola +"? Otkuda my ee vzjali, naskol'ko i pochemu my mozhem byt' uvereny, chto ona u vsex odna i ta zhe? Nu, i dal'she, voobshhe o "pravilax" - togda v krug ego somnenij popadaet i tretja formulirovka.
Kardinal'nym (i, poxozhe, edinstvennym) vyxodom javljaetsa platonizm. Witgenstein etot vyxod, konechno, videl, no, kak serjeznyj filosof, ne priznaval: mol, eto ne vyxod, a uxod ot problemy. Kak "Deus ex Machina", ili "a nautro ix vsex nashli v kanave".

PS. Iz Hofstadtera vspomnil:
"yields falsehood when preceded by its quotation" yields falsehood when preceded by its quotation.
I eshhe zadachka o programme, pechatajushhej svoj sobstvennyj text: osobenno s ogranicheniem, chto nel'zja ispol'zovat' chislovye znachenija simvolov kavychek.

(Ответить) (Thread)
[User Picture]From: pendelschwanz
2003-05-13 03:05 am

Спасибо за справку. Все утро сидел с африканцами вокруг костра и мы обсуждали все нюансы теоремы Геделя. У бушменов есть природное чувство конструктивности, которую они впитывают с молоком матери. Сама идея континуума, неполноты или алгоритмической неразрешимости приводит бушменских воинов в ярость, они хватаются за копья и бегут в атаку за теми кто это проповедует.
Когда вождь отряда программистов стал говорить мне что убьет всякого кто будет рассуждать об алгоритмической неразрешимости, я его успокоил.
Я сказал ему -
"Знаешь, Мванга,
если тебе удалось убить леопарда копьем - тебе повезло, духи охоты помнят о тебе. Охотник который не пользуется поддержкой духов, может бросать копье во все стороны неисчислимое количество раз - вероятность того что он попадет в леопарда, равна нулю.
Если тебе удалось доказать какое-то утверждение - тебе повезло, дух Гёлеля помнит о тебе. Математик который не пользуется поддержкой духов, может манипулировать аксиомами и правилами заключения неисчислимое количество раз - вероятность того что он докажет что-нибудь принципиально новое равна нулю.
Если тебе удалось найти решение какого-нибудь уравнения гидрадинамики или аэродинами - тебе повезло, духи Навье и Стокса помнят о тебе. Дифурщик который не пользуется поддержкой духов, может манипулировать формулами, моделями и численными методами неисчислимое количество раз - вероятность того что он решит какую-нибудь задачу кроме того небольшого круга решаемых задач описанных в учебнике равна нулю.
(Ответить) (Thread)
From: drw
2003-05-13 03:09 am

Очень интересно, спасибо!
(Ответить) (Thread)
[User Picture]From: ifyr
2003-05-13 05:26 am
Спасибо большое!
(Ответить) (Thread)
[User Picture]From: avva
2003-05-13 07:31 pm

Re:

Всегда пожалста!
(Ответить) (Parent) (Thread)
[User Picture]From: abys
2003-05-14 03:57 am

Спасибо
(Ответить) (Thread)
From: (Anonymous)
2005-01-02 03:13 pm

Меня всегда больше интересовала интерпретация теорем


[u][b]
Вариации на тему Гёделя (http://www.litsovet.ru/index.php/material.read?material_id=21307)
[/b][/u]
Мат
(Ответить) (Thread)
[User Picture]From: alex_vinokur
2014-12-02 07:06 am

Наш мир - не предел совершенства

Был замысел. Он воспарил
До пятого времени года.
Иллюзию похоронил
Хирург математики - Гёдель.

Печален его епикриз.
Наш мир - не предел совершенства.
Исполнен не каждый каприз,
И так далеко до блаженства.

Потом из Европы сбежал.
(Но это отдельная тема)
Разрушила храм-идеал
Вторая его теорема.

http://alex-vinokur.livejournal.com/82695.html
(Ответить) (Thread)
[User Picture]From: gul_kiev
2015-05-06 09:50 am
Спасибо, очень интересно!
Однако, к сожалению, не всё понятно - а именно, ускользает, как понятия "смысл" и "истинность" участвуют в формулировках теорем и их доказательствах (а не просто в объяснениях).
Вот вы пишете:

> С точки зрения формальных доказательств система T не имеет "семантики"

И потом:

> первый и второй варианты теоремы Гёделя, хоть они и более просты для доказательства

Раз варианты с семантикой проще в доказательстве, значит, понятие "истинность" присутствует в какой-то внешней по отношению к T системе, в которой эта теорема доказывается (пусть это система M), и там эта истинность формализована? Без формализации её использовать в математическом доказательстве было бы невозможно. Но тогда это условная истинность, являющаяся по сути лишь синтаксическим термином системы M, ведь так?

Что есть истинность, скажем, для геометрии? Например, доказуемо, что сумма углов треугольника 180°. Но это относится к абстрактным (идеальным) треугольникам, и если у какого-то реального треугольника измеренные транспортиром углы в сумме дадут 179° (или между звёздами, или ещё почему-то), это не будет означать некорректность аксиоматики геометрии, формальное доказательство первично. То же, как мне кажется, и с числами (дефект масс не отменяет сложение чисел), и с множествами (нельзя сказать, верна ли "на самом деле" континуум-гипотеза) - аксиоматика первична.

Корректна ли геометрия Лобачевского? Пока не было интерпретации, видимо, нет, но с их появлением она стала корректна, так? Но в таком случае истинность высказывания и корректность системы оказывается субъективна, она зависит от того, что под терминами понимает тот или иной математик в конкретный момент времени. Но как тогда она участвует в формальных доказательствах?

У меня есть смутное (и, вполне возможно, неверное) ощущение, что "истинность" в математике - настолько же всем понятный, но ненаучный (субъективный и принципиально не поддающийся формализации) термин, как, скажем, "квалиа" в физике. Что автоматический доказыватель теорем настолько же не может оперировать понятием "истинность", как философский зомби не обладает квалиа. Я ошибаюсь?
(Ответить) (Thread)
[User Picture]From: gul_kiev
2015-05-06 10:06 am
Продолжая тему:
Консистентность аксиоматики Пеано была доказана в расширенной системе аксиом (с трансфинитной индукцией и, кажется, чем-то ещё). Но какой смысл в этом доказательстве, если нет (и не может быть) доказательства консистентности этой расширенной системы? Ведь получается, что это доказательство нисколько не добавило нам уверенности в том, что PA непротиворечива.
(Ответить) (Parent) (Thread)
[User Picture]From: avva
2015-05-06 11:31 am
Я отвечу, но не сегодня, сегодня времени нет.
(Ответить) (Parent) (Thread)
[User Picture]From: gul_kiev
2015-05-24 06:17 am
Спасибо, торопиться совсем некуда, особенно учитывая, что я оставил коммент через 12 лет после написания поста. :)
(Ответить) (Parent) (Thread)