t'''и т.п. Штрихованные буквы t', t'',… вводятся нами в употребление, дабы не ограничивать число переменных, которые могут встретиться в произвольном выражении. Мы будем считать штрих( ') отдельным символом формальной системы, так что действительное количество символов в системе остается конечным. Помимо этого нам также потребуются символы для базовых арифметических операций =, +, х(«умножить»)и т.д.; для различных видов скобок (, ), [, ], и для обозначения логических операций, таких как &(« и»), =>(« следует»), V(« или»), <=>(« тогда и только тогда»), ~ (« не»). Дополнительно нам будут нужны еще и логические« кванторы»: квантор существованияEк.с.(« существует… такое, что») и квантор общностиAк.о.(« для любого… выполняется»). Тогда мы сможем такие утверждения, как, например, «последняя теорема Ферма», привести к виду:
—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к.о., позволяющими формулировать утверждения, подобные последней теореме Ферма). То, что мы не рассматриваем более общую область математики, не умаляет нашу задачу: арифметика и сама по себе обладает общностью, достаточной для применения процедуры Геделя. Если мы допустим, что благодаря программе Гильберта мы действительно располагаем такой всеобъемлющей системой аксиом и правил вывода для арифметики, то мы тем самым обретаем и определенный критерий для выявления «корректности» математического доказательства любого утверждения в области арифметики. Возлагались надежды на то, что подобная система аксиом и правил может быть полной в смысле предоставляемой нам принципиальной возможности решать, истинно или ложно произвольное утверждение, сформулированное в рамках этой системы.
Гильберт рассчитывал, что для любой строки символов, представляющих математическое утверждение, скажем, Р, можно будет доказать либо Р, либо ~ Р, если Р истинно или ложно, соответственно. Здесь мы в обязательном порядке оговариваем, что строка должна быть синтаксически корректна, где «синтаксически корректна» по сути означает «грамматически корректна» — то есть удовлетворяет всем правилам записи, принятым в данном формализме, среди которых будет правильное попарное соответствие скобок и т.п.— так чтобы Р всегда имело четко определенное значение «ложь» или «истина». Если бы надежды Гильберта оправдались, то можно было бы вообще не задумываться о том, что означает то или иное утверждение! Р было бы просто-напросто синтаксически корректной строкой символов. Строке было бы приписано значение ИСТИНА, если бы Р являлось теоремой (другими словами, если бы Р было доказуемо в рамках системы); или же ЛОЖЬ, если бы теоремой было ~ Р. Чтобы такой подход имел смысл, мы должны дополнительно к условию полноты наложить еще и условие непротиворечивости, гарантирующее отсутствие такой строки символов Р, для которой как Р, так и ~ Р были бы теоремами. Ведь в противном случае