Книга: Новый ум короля: О компьютерах, мышлении и законах физики
Теорема Геделя
Теорема Геделя
Часть доказательства, приведенного Геделем, содержало некий очень сложный и детализированный кусок. Однако нам не обязательно разбираться во всех его тонкостях. Основная идея, в то же время, была проста, красива и глубока. И ее мы сможем оценить по достоинству. В «сложной» части (которая, впрочем, содержит много остроумных рассуждений) подробно показано, каким образом частные правила вывода и использование различных аксиом формальной процедуры могут быть представлены в виде арифметических операций. (Хотя в сложной части становится понятной плодотворность этих действий!) Для этого представления нам необходимо будет найти какой-нибудь удобный способ нумерации утверждений при помощи натуральных чисел. Один из способов мог бы заключаться в том, чтобы использовать своего рода «алфавитный» порядок для строчек символов формальной системы, имеющих одинаковую длину, упорядочить заранее строчки по длине. (Таким образом, за выстроенными в алфавитном порядке строками из одного символа будут следовать строки длиной в два символа, также упорядоченные по алфавиту; за ними идут строки из трех символов и так далее.) Это называется лексикографическим порядком[72]. В действительности Гедель использовал более сложную систему нумерации, но различия в данном случае для нас несущественны. Нас же должны в особенности интересовать функции исчисления высказываний одной переменной, наподобие введенной выше G(?). Пусть n-я (из пронумерованных выбранным способом строк символов) такая функция от аргумента ? обозначается
Pn(?).
Мы можем допустить, чтобы наша нумерация по желанию была несколько «либеральна» в отношении синтаксически некорректных выражений. (Это позволит значительно упростить перевод системы на язык арифметических операций по сравнению со случаем, когда мы будем стараться исключить из рассмотрения синтаксически некорректные выражения.) Если Pn(?) синтаксически корректно, то оно будет представлять из себя некоторое совершенно определенное арифметическое выражение, в котором фигурируют два натуральных числа п и ад. Каков будет конкретный вид этого выражения — зависит от особенностей системы нумерации, которую мы выбрали. Но эти детали рассматриваются в «сложной» части и сейчас нас не касаются. Пусть Пnбудет n-м доказательством. (Опять же мы можем использовать «либеральную нумерацию», когда для некоторых значений n выражение Пnне является синтаксически корректным и, тем самым, не доказывает никакую теорему.)
А теперь рассмотрим следующую функцию исчисления высказываний от натурального числа ? :
— Eк.с.x[Пx доказывает P?(?)].
В выражении в квадратных скобках частично присутствуют слова, но, тем не менее, это — абсолютно точно определенное выражение. Оно говорит о том, что доказательство номер х является доказательством утверждения Р?(), примененного к самому ?. Находящийся за скобками квантор существования с отрицанием позволяет исключить из рассмотрения одну из переменных («не существует такого х, что…»), приводя нас в конечном счете к арифметической функции исчисления высказываний, зависящей только от ?. В целом данное выражение утверждает, что не существует доказательства Р?(?). Я буду предполагать, что оно оформлено синтаксически корректным образом (даже если Рn(?) некорректно — поскольку тогда выражение было бы истинным за невозможностью существования доказательства синтаксически некорректного утверждения). На самом деле, в результате сделанного нами перевода на язык арифметики, написанное выше будет в действительности неким арифметическим выражением, включающим натуральное число ? (тогда как в квадратных скобках окажется четко определенное арифметическое выражение, связывающее два натуральных числа х и ?). Конечно, возможность представления этого выражения в арифметическом виде далеко не очевидна, но она существует. Рассуждения, приводящие к этому заключению, составляют наиболее трудную задачу в «сложной» части доказательства Геделя. Как и ранее, непосредственный вид арифметического выражения будет зависеть от способа нумерации и в еще большей степени от конкретной структуры аксиом и правил вывода, принятых в нашей системе. Поскольку все это входит в «сложную» часть доказательства, то в данном случае нас не интересует.
Мы пронумеровали все функции исчисления высказываний, зависящие от одной переменной, поэтому той, которую мы ввели выше, также должен быть приписан номер. Пусть этот номер будет k. Наша функция будет в таком случае k-й в общем списке. То есть
— Eк.с.x[Пх доказывает P?(?)] = Рk(?).
Теперь исследуем эту функцию при определенном значении: ? = k. Мы получаем:
Eк.с.х[Пх доказывает Pk(k)] = Pk(k)
Данное утверждение Pk(k) является абсолютно точно определенным (синтаксически корректным) арифметическим выражением. Может ли оно быть доказано в рамках нашей формальной системы? А его отрицание ~ Pk(k) — имеет ли оно такое доказательство? Ответ в обоих случаях будет отрицательный. Мы можем убедиться в этом путем исследования смысла, который лежит в основании процедуры Геделя. Хотя Pk(k) является просто арифметическим выражением, последнее было построено нами таким образом, что написанное в левой части утверждает следующее: «внутри системы не существует доказательства Pk(k)». Если мы были аккуратны в определении аксиом и процедур вывода, и не ошиблись при нумерации, то тогда в рамках системы такого доказательства найти невозможно. Если же доказательство существует, то значение утверждения, содержащегося в Pk(k) — о том, что такого доказательства нет, — будет ложным, а вместе с ним будет ложным и арифметическое выражение, отвечающее Pk(k). Но наша формальная система не может быть построена настолько плохо, чтобы включать в себя ложные утверждения, которые могут быть доказаны! Таким образом, в действительности, доказательство Pk(k) быть не может. Но это в точности то самое, о чем говорит нам Pk(k). То, что утверждает Pk(k), обязано, следовательно, быть верным, а поэтому Pk(k) должно быть верным как арифметическое выражение. Значит, мы нашли истинное утверждение, которое недоказуемо в рамках системы!
А как насчет ~ Pk(k)? Из предыдущих рассуждений видно, что доказательство этому утверждению внутри системы мы найти не сможем. Мы только что установили, что ~ Pk(k) должно быть ложным (ибо Pk(k) является истинным), а мы, по определению, не имеем возможности доказывать ложные утверждения в рамках системы! Таким образом, ни Pk(k), ни ~ Pk(k) недоказуемы в нашей формальной системе, что и составляет теорему Геделя.
- Программа Гильберта для математики
- Формальные математические системы
- Теорема Геделя
- Математическая интуиция
- Платонизм или интуиционизм?
- Теоремы геделевского типа как следствие результатов, полученных Тьюрингом
- Рекурсивно нумеруемые множества
- Является ли множество Мандельброта рекурсивным?
- Некоторые примеры нерекурсивной математики
- Похоже ли множество Мандельброта на нерекурсивную математику?
- Теория сложности
- Сложность и вычислимость в физических объектах
- Глава 4 Истина, доказательство и интуиция
- Теоремы геделевского типа как следствие результатов, полученных Тьюрингом
- Chapter 5. Kernel Initialization
- Кто такая Елена Ивашенцева?
- 11.2. Цели процесса
- Рис. 214. Имена почтовых серверов.
- Document
- ГЛАВА 3 Внутренняя структура .NET Compact Framework
- Джордж Буль Отец булевой алгебры