теорема Геделя говорит нечто о генерации некоторого специального вида текстов в некотором специальном типе формальных систем
можно различить три разных доказательства первой теоремы Гёделя о неполноте. они доказывают несколько разные вещи и исходят из несколько разных предпосылок
пусть у нас есть некая формальная система 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 - неполная система. этот факт опять-таки доказать несколько тяжелее, чем в случае первых двух версий теоремы, где можно было опираться на “истинность” - но уже не слишком тяжело после всей проведенной предварительной работы
вопрос - если система Principia Mathematica (или ZFC. выбор конкретной системы вроде бы не влияет на аргумент)не описывает N, то тогда как мы вообще определим само N? и совсем маленький вопросец - почему вы расселовскую систему обозначаете PA? она ж вроде Principia Mathematica?
мы можем определить N в ZFC, и мы можем определить в ZFC, что значит для утверждения φ быть истинным в N. но это само по себе не гарантирует, что для любого возможного φ мы сможем либо доказать, что оно истинно в N, либо опровергнуть (т.е. доказать противоположное). выбор - ZFC или PA (Peano’s Arithmetic, аксиоматическая система для арифметики; почему не PM - об этом ниже) здесь довольно важен, и непонимание различий приводит часто к путанице
очень важно понять, что теорема Гёделя сама по себе не нуждается в семантике - ей не нужно ни N, ни понятие “истинности” утверждений. она сугубо синтаксична. если есть некоторая теория, достаточно сложная (могущая доказать некоторые свойства натуральных чисел) и рекурсивная (множество аксиом конечно или бесконечно, но описывается алгоритмом), то эта теория неполна: неверно, что она может доказать или опровергнуть любое утверждение. здесь речь идёт только о возможности доказать/опровергнуть, т.е. о существовании каких-то формальных последовательностей символов (формальных доказательств из аксиом данной теории)
если наша теория T сформулирована в языке арифметики (константа 0, функции + и * итп.), то гёделево утверждение G, к-е мы для него построим, будет утверждением о натуральных числах, являющимся в некотором неформальном смысле формализацией утверждения “меня невозможно доказать”. если мы теперь обратим внимание на семантику, т.е. рассмотрим стандартную модель арифметики N и истинность в ней, окажется, что утверждение G истинно. само по себе это неудивительно, т.к. в некотором смысле (очень и очень неформальном) истинность G “встроена” в него на метаматематическом уровне (математический уровень - наши формальные доказательства в формальной системе T; метаматематический уровень - рассуждения о таких формальных доказательствах в T). по сути дела, в процессе доказательства теоремы Гёделя мы берём всякого рода метаматематические понятия (напр. доказуемость в T), и вталкиваем их в математическую вселенную путём их арифметизации (путём кодирования формул и доказательств числами, и составления утверждений об этих числах, соответствующих метаматиматическим свойствам исходных формул/доказательств)
следует различать использование слов, подобных слову “истинность”, на метаматематическом и математическом уровнях. на метаматематическом уровне такое использование неизбежно, неформально и ограниченно (например, на этом уровне мы говорим: система T доказывает утверждение φ . это высказывание может быть истинным или ложным. эта истинность или ложность - метаматематического характера). на математическом уровне мы рассматриваем истинность данного формального утверждения φ, например, в модели N (например, на этом уровне мы говорим: формула вида Thm_T(‘φ’) верна в N, где Thm_T(x) предикат, который мы построили для отображения в арифметике понятия доказуемости в T, а ‘φ’ - число, код формулы φ). этот вид истинности незаменим в теории моделей и в логике вообще, но он не нужен для доказательства теоремы Гёделя, это док-во не пользуется семантикой на математическом уровне
из того, что теория T неполна (синтаксическое доказательство Гёделя), мы можем мгновенно заключить, что она не “описывает” N, т.к. для “описывания” N ей пришлось бы доказывать все истинные в N утверждения и опровергать все ложные; т.к. любое утверждение либо истинно в N, либо ложно, T должна была бы быть полной теорией
теперь про ZFC
у ZFC просто нет канонической модели, в том смысле, в каком она есть у арифметики. когда мы говорим, что что-то “истинно” в ZFC, это всегда означает формальное доказательство из ZFC и ничего другого. к ZFC, однако, тоже можно применить теорему Гёделя, т.к. она мощнее чем, скажем, PA, для которой мы провели полностью док-во Гёделя, и PA можно в ней “интерпретировать”. для ZFC можно построить утверждение G, к-е не будет ни доказуемо, ни опровергаемо в ZFC. но говорить о его истинности мы можем теперь только с неформальной, метаматематической точки зрения
или вот ещё один способ посмотреть на то же самое. Гёделево утверждение G для PA верно в N (неформальный аргумент), и мы это можем формально доказать, но не в самой PA (она это не может доказать, потому что внутри неё вообще нельзя определить “истинность в N”), а в куда более мощной ZFC. ZFC мощна, и потому мы можем определить нашу семантическую “вселенную” N в ней в качестве синтаксического объекта-множества N, и свести любое семантическое утверждение об истинности в N к синтаксическому утверждению о доказуемости соответствующего утверждения о множествах. Гёделево утверждение G для ZFC в каком-то неформальном смысле тоже “истинно”, но формализовать эту “истинность” нам уже просто негде
я, кажется, сильно увлёкся и ушёл в сторону от вашего вопроса. поэтому попробую к нему вернуться. разница между PA и ZFC вот в чём. и та и другая - формальные теории, некий набор аксиом. однако для первой N не является частью теории, а является моделью, какой-то канонической моделью, которую мы выбрали, и в которой мы проверяем истинность или ложность утверждений PA или любых других утверждений в том же языке арифметики, когда нам это удобно. для ZFC же N - это объект, описываемый теорией, это множество, как любое другое множество, о котором ZFC что-то может доказать. если мы посмотрим на какую-то модель ZFC (очень гипотетически, т.к. существование такой модели мы не можем доказать вследствие 2-й теоремы Гёделя о неполноте), то N в ней будет элементом, а не самой моделью
N для ZFC - это как натуральное число для PA
и в контексте теоремы Гёделя ZFC выступает в двух очень разных ролях. с одной стороны, мы используем ZFC как некий универсальный формализатор всех математических методов: мы можем формализовать в нём само доказательство теоремы Гёделя, например, используя, в частности, его видение N как всего лишь множества, одного из рассматриваемых объектов. с другой стороны, мы можем к самой ZFC применить теорему Гёделя и найти в ней недоказуемое и неопровержимое утверждение; это возможно за счёт достаточнной внутренней сложности ZFC, рассматриваемой даже как “бессмысленная” система аксиом, вне зависимости от того факта, что на самом деле это та самая ZFC, к-ю мы используем для формализации всей математики
наконец, про PA/PM
система Principa Mathematica просто слишком громоздка и устарела, ей неудобно пользоваться. поэтому обычно пользуются PA (Peano’s Arithmetics) или другими формальными теориями арифметики; доказательство Гёделя работает для них практически без изменений (даже с некоторыми упрощениями)
PA - это теория в формальном языке, включающем в себя константный символ 0, функциональные символы + , * , S (x) (successor function). PA включает в себя следующие аксиомы:
S (x) = S (y) => x = y
(∀ x) (x != 0 <==> (∃ y) (S (y) = x))) ("у каждого числа, кроме 0, есть предыдущее")
x + 0 = x
x + S (y) = S (x+y) (рекурсивное определение сложения)
x * 0 = 0
x * S (y) = x * y + x (рекурсивное определение сложения)
и схема индукции: для каждой формулы вида φ (x) вводится аксиома
(φ (0) ∧ (∀ x) (φ (x) => φ (S (x)))) ===> (∀ x) φ (x)
Что "в любой республике можно устроить диктатуру чисто по закону" - вполне в духе Геделя утверждение. У него и позитивные результаты вполне были - например доказательства непротиворечивости аксиомы выбора и континуум-гипотезы - в данном случае как раз доказательства того что "тут дырок нет" - значит ими можно пользоваться по крайней мере без опаски. Но вообще-то это не игра и не маразм - такие вещи прояснять действительно очень полезно практически.
- А это он? Мне казалось, что Коэн.
Коэн доказал независимость AC и CG (что намного сложнее было) - непротиворечивость доказал как раз Гедель. Независимость означает что и утверждение и его отрицание можно добавить "без проблем". Непротиворечивость означает лишь что само утверждение добавить можно (но что оно не выводится из аксиом оно не доказывает - собственно любая теорема тривиально непротиворечивое утверждение - ее доказательство является одновременно и доказательством ее непротиворечивости - правда одновременно оно же является и доказательством ее зависимости - с потенциально независимыми так не проходит). Собственно отличный ликбез по теме оснований математики вообще как раз от Коэна книжка - "Континуум-гипотеза и теория множеств" в третьей главе он излагает доказательства Геделя. Первые две посвящены общем ликбезу без которых последние две главы были бы непонятны неподготовленному читателю.
> доказательства непротиворечивости аксиомы выбора и континуум-гипотезы
- Его, вообще-то, до сих пор нет.
Вас геделевское не устраивает? Ну там можно это конечно пообсуждать...
- Так Гёдель доказывал несколько не то, что Вы ему приписали.
Ну а что он доказал - именно что если ZF - AC имееет модель (т.е. непротиворечива) то и ZF + AC имеет модель в той же системе. Ну давайте не будем дальше углубляться в мелочи. По крайней мере если они несущественные и я и вы их заведомо знаете.
- Именно - "если противоречива ZF + AC, то противоречива и ZF". Импликация. Вы же ему выше приписали доказательство безусловного тезиса о непротиворечивости ZF + AC. Если таковое было уже у Гёделя - чем потом Есенин-Вольпин и Кузичев занимались?
Ну я что - должен везде говорить "относительно непротиворечиво" и указывать базу?
- Принимая во внимание, что тут мы имеем дело с одним из стандартных мифов (по которым и проходит водораздел между грамотными людьми и начитавшимися научпопа обывателями) - разумеется.
Вы думаете - от этого понятнее будет? Тем более что в том же Шенфилде еще на полном серьезе обсуждается возможность нетривиальных категоричных систем. Если там профи путались еще недавно - ну вот этими деталями-то зачем дилетантов грузить?
- Это - как раз не детали. Потому что при их опускании возникает совершенно превратное представление о вопросе.
We need real semantics to make sense of the informal “translation” of P as “P is unprovable”. But the semantics they give stays improperly subservient to syntax: if the theory PA changes it status and it turns out it doesn’t have N as a model, we suddenly must change our semantics to some other model of PA
There is no real reason to do it, though. PA is a theory under our investigation, and when we talk about the truth of a statement P about natural numbers, we use N not because N is a model of PA (what of it? plenty of other structures are models of PA too, but we don’t use them), but simply because it’s our canonical model which provides us with the very notion (the very fixed notion) of arithmetical truth