Вначале была аксиома. Гильберт. Основания математики
Шрифт:
Возникает важный вопрос: можно ли свести всю математику к теории множеств? Если истолковать объекты нашего языка первого порядка как множества, легко эмпирически убедиться, что большинство математических сущностей можно определить на основе множеств. Эта программа исследования основывалась на вышеупомянутой теории множеств ZF: на базе небольшого количества аксиом, сформулированных в первом порядке, эта теория множеств была способна охватить значительную часть математики того времени.
Снова, как в итоге понял Гёдель, цена этого теоретического богатства (выразимость) — метатеоретическая бедность, которая проявляется в нескольких ограничивающих результатах: теоремах о неполноте. В первой теореме доказывается, что существует истинная формула, которая недоказуема в ZF (хотя в работе Гёделя в качестве отправной формальной системы взят труд Рппсгрга mathematica, а его результаты справедливы для ZFи других смежных систем). А во второй — что невозможно доказать непротиворечивость ZF в ZF. Более того, доказательство
Кто из нас не возликовал бы, подними он занавес, за которым скрывается будущее, загляни он в последующие достижения науки и секреты ее развития?!
Давид Гильберт, из речи на II Международном конгрессе математиков в Париже
Парадокс лжеца был для Гёделя одним из двигателей доказательства теорем о неполноте. Поскольку доказательство было на грани перехода в цикличность, некоторые математики — в частности, 60-летний Цермело — не осознали его ценности. Гёдель придумал ловкий перевод на метаязык внутри языка: арифметизацию метаматематики. С помощью смелой цифровой кодификации, основанной на простых числах (которую с тех пор называют гёделизацией), он назначил номера знакам так, чтобы с каждой формулой (и также с каждым доказательством) можно было связать число, кодировавшее бы всю структуру. Пропозиции, в которых говорилось о свойствах формальной системы, выражались в рамках системы посредством арифметических формул. Доказуемость, например, была представлена в виде числового отношения.
В таких условиях Гёдель вышел из ситуации, составив формулу G, которая говорит сама о себе: «я недоказуемо». Эта формула стала примером неразрешимого утверждения внутри формальной системы: ни она, ни ее отрицание не являются теоремами, то есть чем-то доказуемым. Действительно, Іеделю удалось доказать, что G доказуемо тогда и только тогда, когда ¬G доказуемо. Следовательно, если мы хотим, чтобы формальная система была непротиворечивой, ни G, ни ¬G не могут быть таковыми. Если бы G было доказуемо, так как ¬G утверждает в метаматематических терминах, что G доказуемо (отрицает то, что оно недоказуемо, как сказано в нем самом), то было бы возможно доказать также ¬G и вывести противоречие (G^¬G). И наоборот, если бы ¬G было доказуемым, мы могли бы по той же причине доказать G и прийти к тому же противоречию. В итоге доказательство любой из этих двух формул автоматически предполагало бы противоречивость системы. Более того, если допустить, что формальная система непротиворечива, то G недоказуемо, но истинно. Если бы G было ложно, так как в G говорится: «я недоказуемо», то G было бы доказуемо, что невозможно. Следовательно, у нас есть высказывание G, которое, хотя и недоказуемо, является истинным.
Существование неразрешимого утверждения предполагает, что аксиомы теории не содержат ответа на все вопросы, формулируемые формальным языком, потому что ни утверждение, ни его отрицание не являются теоремами. И так как либо оно, либо его отрицание должно быть истинным, у нас есть истинная недоказуемая формула. Хуже всего, что если добавить неразрешимое утверждение в качестве аксиомы, появляются другие, новые. Математика вдруг очнулась от гильбертова сна — от мечты о полноте, в которой аксиоматические системы не содержат неразрешимых формул, а истинное всегда совпадает с доказуемым. Проще говоря, «непротиворечивый» предполагает «неполный», и наоборот, «полный» предполагает «противоречивый». Ни одна формальная система, содержащая привычную арифметику, не может быть одновременно и той и другой. Если мы предположим, что она непротиворечива, она всегда будет неполной, то есть будет содержать недоказуемые истины. Будут существовать некоторые истинные свойства формально неразрешимых чисел, то есть свойства, которые мы не можем ни доказать, ни отвергнуть на основе аксиом.
Но за первой теоремой о неполноте следует вторая: так как непротиворечивость равносильна утверждению, что формула 0/=0 недоказуема, Гёдель трансформировал это последнее математическое свойство в арифметическую формулу (назовем ее С) и заметил, что в первой теореме установлено, по сути, что «C->G». Непротиворечивость предполагает, что существует неразрешимое утверждение и, следовательно, неполнота. Так что доказательство С позволило бы нам исключить G из импликации «C->G» посредством modus ponens и, следовательно, доказать G, что невозможно, поскольку G недоказуемо. Это удивительное следствие сводится к тому, что непротиворечивость формальной системы, которая включает в себя арифметику, недоказуема в рамках формальной системы. Гёдель не доказал должным образом эту вторую теорему, он только высказался о ее приемлемости, но так никогда и не записал обещанного доказательства. Первое полное доказательство, очень тщательное, появилось, что любопытно, в 1939 году, во втором томе «Оснований математики» Бернайса и Гильберта.
Мало того, к синтаксическим ограничениям, которые открыл Гёдель, присоединилось другое ограничение — семантическое, формальных систем первого порядка: теорема, сформулированная Леопольдом Лёвенгеймом (1878-1957) и Туральфом Скулемом (1887-1963) около 1920 года (Скулем вернулся к ней в 1933 году). В 1930 году в рамках своего доказательства полноты логики первого порядка Гёдель мимоходом доказал, что любая непротиворечивая теория первого порядка имеет модель, в которой аксиомы проверяются, хотя и ничего не добавил о том, какие характеристики имеет эта модель и как ее построить. Лёвенгейм и Скулем до этого заметили, что любая непротиворечивая формальная система первого порядка имеет, по сути, счетную модель. Это порождает парадокс Скулема: если ZF непротиворечиво, то оно обладает счетной моделью. То есть несчетный континуум, которым мы намереваемся оперировать в ZF, может относиться к счетному множеству вне ZF. Теория действительных чисел, от которой мы ждем знакомой несчетной модели («настоящие» действительные числа), также имеет счетную модель.
ТЕОРЕМА ТАРСКОГО О НЕВЫРАЗИМОСТИ ИСТИНЫ
Альфред Тарский (1902-1993) считал себя лучшим из живущих математических логиков с ясным умом (чтобы избежать сравнения с Гёделем, страдавшим маниями и навязчивыми идеями).
В 1939 году этому польскому ученому удалось переехать в США и на несколько десятилетий превратить университет Беркли в мировую столицу математической логики. Он любил работать ночью и увлекался психотропными средствами, которые помогали ему бодрствовать и трудиться без устали, а также имел репутацию Казановы.
Тарский знаменит тем, что в 1933 году опубликовал огромную статью, в которой дал формальное определение истине и таким образом обозначил начало теории моделей. Если Гильберт в своей теории доказательства прояснил синтаксическое понятие формального доказательства, Тарский сделал то же самое с семантическим понятием истины.
Альфред Тарский, 1968 год.
Еще одна ограничительная теорема
В 1933 году, через два года, после того как Гёдель объявил о двух результатах о неполноте, Тарский извлек на свет другую ограничительную теорему, хотя она уже была провозглашена и доказана Гёделем в письме Цермело, датированном 1931 годом. В этой ограничительной теореме установлено, что любая формальная теория первого порядка, содержащая базовую арифметику, неспособна (если она непротиворечива) выразить свое собственное понятие истины. Интересные непротиворечивые теории не могут содержать выражения «быть истинным» в своем языке, поскольку в этом случае они породили бы парадокс лжеца. С помощью гёделизации можно воспроизвести формулу Г, которая утверждает о самой себе, что она ложная. Воспользовавшись выражением «быть истинным», которое, предположительно, существует в языке, мы придем к следующему противоречию: Т истинное тогда и только тогда, если оно ложное, поскольку именно это утверждает Т. Как в случае с лжецом: я говорю правду, если я лгу. Без сомнения, математические логики сумели применить цикличность, лежащую в основе парадоксов, с большой пользой.
ENTSCHEIDUNGSPROBLEM, ИЛИ ПРОБЛЕМА РАЗРЕШЕНИЯ
На IX Международном конгрессе математиков, проходившем в 1928 году в Болонье, Гильберт воспользовался случаем, чтобы предложить свой план по спасению математики и обозначить следующий вопрос: существует ли механическая процедура, которая решала бы все и каждую проблему математики, алгоритм, способный принципиально разрешить все математические вопросы, который при заданной математической пропозиции дал бы нам знать, является она теоремой или нет? Другими словами, является ли она разрешимой в математике? Как и на вопросы непротиворечивости и полноты, ответ на нее был отрицательным. После теорем Гёделя стало ясно, что ответ на эту проблему — категорическое «нет», поскольку математика является неполной: предполагаемый алгоритм в течение бесконечного времени «думал» бы над неразрешимым высказыванием, поскольку ни оно, ни его отрицание не являются теоремой. Следовательно, ответ на проблему разрешения оставалось дать только для логики первого порядка, которая, напомним, является полной. Однако в 1936 году Алан Тьюринг (1912-1954) и независимо от него Алонзо Чёрч (1903-1995) доказали, что логика первого порядка также неразрешима.