Гильберт рассчитывал, что для любой строки символов, представляющих математическое утверждение, скажем, Р , можно будет доказать либо Р , либо ~ Р , если Р истинно или ложно, соответственно. Здесь мы в обязательном порядке оговариваем, что строка должна быть синтаксически корректна, где «синтаксически корректна» по сути означает «грамматически корректна» — то есть удовлетворяет всем правилам записи, принятым в данном формализме, среди которых будет правильное попарное соответствие скобок и т. п. — так чтобы Р всегда имело четко определенное значение «ложь» или «истина». Если бы надежды Гильберта оправдались, то можно было бы вообще не задумываться о том, что означает то или иное утверждение! Р было бы просто-напросто синтаксически корректной строкой символов. Строке было бы приписано значение ИСТИНА, если бы Р являлось теоремой (другими словами, если бы Р было доказуемо в рамках системы); или же ЛОЖЬ, если бы теоремой было ~ Р . Чтобы такой подход имел смысл, мы должны дополнительно к условию полноты наложить еще и условие непротиворечивости, гарантирующее отсутствие такой строки символов Р , для которой как Р , так и ~ Р были бы теоремами. Ведь в противном случае Р могло бы быть одновременно и ИСТИНОЙ, и ЛОЖЬЮ!
Такой подход, согласно которому можно пренебрегать смысловыми значениями математических выражений и рассматривать их лишь как строки символов некоторой формальной математической системы, в математике получил название формализма. Некоторым нравится эта точка зрения, с которой математика превращается в своего рода «бессмысленную игру». Однако я сам не являюсь сторонником таких идей. Все-таки именно «смысл» — а не слепые алгоритмические вычисления — составляет сущность математики. К счастью, Гедель нанес формализму сокрушающий удар! Давайте посмотрим, как он это сделал.
Теорема Геделя
Часть доказательства, приведенного Геделем, содержало некий очень сложный и детализированный кусок. Однако нам не обязательно разбираться во всех его тонкостях. Основная идея, в то же время, была проста, красива и глубока. И ее мы сможем оценить по достоинству. В «сложной» части (которая, впрочем, содержит много остроумных рассуждений) подробно показано, каким образом частные правила вывода и использование различных аксиом формальной процедуры могут быть представлены в виде арифметических операций. (Хотя в сложной части становится понятной плодотворность этих действий!) Для этого представления нам необходимо будет найти какой-нибудь удобный способ нумерации утверждений при помощи натуральных чисел. Один из способов мог бы заключаться в том, чтобы использовать своего рода «алфавитный» порядок для строчек символов формальной системы, имеющих одинаковую длину, упорядочить заранее строчки по длине. (Таким образом, за выстроенными в алфавитном порядке строками из одного символа будут следовать строки длиной в два символа, также упорядоченные по алфавиту; за ними идут строки из трех символов и так далее.) Это называется лексикографическим порядком [72]. В действительности Гедель использовал более сложную систему нумерации, но различия в данном случае для нас несущественны. Нас же должны в особенности интересовать функции исчисления высказываний одной переменной, наподобие введенной выше G ( ω ). Пусть n - я(из пронумерованных выбранным способом строк символов) такая функция от аргумента ω обозначается
72
Мы можем представить себе лексиграфический способ упорядочивания как обычный способ, используемый для натуральных чисел, только сделанный «по основанию