Роджер Пенроуз - Новый ум короля: О компьютерах, мышлении и законах физики
— Eк.с.ω, х, у, z [(x + 1)ω+3+
+ (у + 1)ω+3 = (z+1)ω+3]
(см. главу 2, «Неразрешимость проблемы Гильберта»). (Я мог бы написать «0111» для «3», и, возможно, использовать для «возведения в степень» обозначение, более подходящее к рассматриваемому формализму; но, как уже говорилось, я буду придерживаться стандартной системы записи во избежании ненужной путаницы.) Это утверждение (если читать его до левой квадратной скобки) звучит как:
«Не существует таких натуральных чисел ω, х, у, z, что…».
Мы можем также переписать последнюю теорему Ферма при помощи Aк.о.:
Aк.о.ω, х, у, z [~ (х + 1)ω+3+ (у + 1)ω+3 = (z+1)ω+3],
которое будет читаться следующим образом (заканчивая символом «не» после левой квадратной скобки):
«Для любых натуральных чисел ω, х, у, z не может быть выполнено…»,
что логически эквивалентно написанному ранее.
Нам понадобятся еще и буквы, обозначающие целые утверждения, для чего я буду использовать заглавные буквы Р, Q, R, S… Таким утверждением может, к примеру, служить и вышеприведенная теорема Ферма:
F = ~ Eк.с.ω, х, у, z [(x + 1)ω+3+ (у + 1)ω+3 = (z+1) ω+3].
Утверждение может также зависеть от одной или более переменных; например, нас может интересовать формулировка теоремы Ферма для некоторого конкретного[71] значения степени ω + 3
G(ω) =~ Eк.с.x, y,z[(x + 1)ω+3+ (y+ 1)ω+3 = (z+1)ω+3],
так что G(0) утверждает, что «куб не может быть суммой кубов положительных чисел»; G(1) говорит о том же применительно к четвертым степеням и так далее. (Обратите внимание на отсутствие ω после символа Eк.с.). Тогда теорема Ферма гласит, что G(ω) выполняется для любого ω :
F = Aк.о.ω[G(ω)].
G() является примером так называемой функции исчисления высказываний, т. е. утверждением, которое зависит от одной или более переменных.
Аксиомы нашей системы будут представлять из себя перечень утверждений общего характера, чья справедливость в рамках принятого символизма предполагается самоочевидной. Например, для произвольных утверждений или функций исчисления высказываний Р, Q, R() мы могли бы указать среди прочих аксиом системы такие, как
(P&Q) => Р,
— (~ Р) <=> Р,
— Eк.с.х[R(x)] <=>Aк.о.x[~ R(x)],
«априорная истинность» которых уже заключена в их смысловых значениях. (Первое утверждение означает лишь, что «если выполняется Р и Q, то выполняется и Р»; второе устанавливает равносильность утверждений «неверно, что не выполняется Р» и «Р выполняется»; а третье может быть проиллюстрировано эквивалентностью двух способов формулировки теоремы Ферма, данных выше.) Мы можем также включить основные аксиомы арифметики:
Aк.о. х, у[х + у = у + х],
Aк.о. х, у, z[(x + у) х z = (x х z) + (у х z)],
хотя некоторые предпочитают определять арифметические операции через более простые понятия и выводить вышеуказанные утверждения как теоремы. Правила вывода могут вводиться в виде (самоочевидных) процедур типа
«Из Р и Р => Q следует Q».
«Из Aк.о.x[R(x)] мы можем вывести любое утверждение, получающееся путем подстановки конкретного натурального числа x в R(x)».
Такие правила являются инструкциями, следуя которым, можно с помощью утверждений, чья истинность уже доказана, получать новые утверждения.
Теперь, отталкиваясь от системы аксиом и раз за разом применяя правила вывода, мы имеем возможность построить достаточно длинные цепочки новых утверждений. На любой стадии этого процесса мы можем использовать снова и снова любую из аксиом, а также обратиться к любому из уже выведенных нами производных утверждений. Каждое утверждение из корректно выстроенной цепочки называется теоремой (несмотря на то, что многие из них достаточно тривиальны и неинтересны с точки зрения математики). Если у нас есть некое утверждение Р, которое мы хотим доказать, то мы должны подобрать такую цепочку, выстроенную в согласии с действующими правилами вывода, которая заканчивается утверждением Р. Такая цепочка предоставит нам доказательство Р в рамках системы; а Р тогда будет являться, соответственно, теоремой.
Идея программы Гильберта состояла в том, чтобы найти применительно к любой отдельно взятой области математики набор аксиом и правил вывода, который был бы достаточно полным для всех возможных в данной области корректных математических рассуждений. Пусть такой областью будет арифметика (с добавленными кванторами Eк.с. и Aк.о., позволяющими формулировать утверждения, подобные последней теореме Ферма). То, что мы не рассматриваем более общую область математики, не умаляет нашу задачу: арифметика и сама по себе обладает общностью, достаточной для применения процедуры Геделя. Если мы допустим, что благодаря программе Гильберта мы действительно располагаем такой всеобъемлющей системой аксиом и правил вывода для арифметики, то мы тем самым обретаем и определенный критерий для выявления «корректности» математического доказательства любого утверждения в области арифметики. Возлагались надежды на то, что подобная система аксиом и правил может быть полной в смысле предоставляемой нам принципиальной возможности решать, истинно или ложно произвольное утверждение, сформулированное в рамках этой системы.
Гильберт рассчитывал, что для любой строки символов, представляющих математическое утверждение, скажем, Р, можно будет доказать либо Р, либо ~ Р, если Р истинно или ложно, соответственно. Здесь мы в обязательном порядке оговариваем, что строка должна быть синтаксически корректна, где «синтаксически корректна» по сути означает «грамматически корректна» — то есть удовлетворяет всем правилам записи, принятым в данном формализме, среди которых будет правильное попарное соответствие скобок и т. п. — так чтобы Р всегда имело четко определенное значение «ложь» или «истина». Если бы надежды Гильберта оправдались, то можно было бы вообще не задумываться о том, что означает то или иное утверждение! Р было бы просто-напросто синтаксически корректной строкой символов. Строке было бы приписано значение ИСТИНА, если бы Р являлось теоремой (другими словами, если бы Р было доказуемо в рамках системы); или же ЛОЖЬ, если бы теоремой было ~ Р. Чтобы такой подход имел смысл, мы должны дополнительно к условию полноты наложить еще и условие непротиворечивости, гарантирующее отсутствие такой строки символов Р, для которой как Р, так и ~ Р были бы теоремами. Ведь в противном случае Р могло бы быть одновременно и ИСТИНОЙ, и ЛОЖЬЮ!
