Новый ум короля: О компьютерах, мышлении и законах физики

Необходимо будет несколько уточнить, что мы понимаем под «формальными математическими системами аксиом и правил вывода». Мы должны предположить наличие некоторого алфавита символов, через которые будут записываться математические выражения. Эти символы в обязательном порядке должны быть адекватны для записи натуральных чисел с тем, чтобы в нашу систему могла быть включена «арифметика». По желанию, мы можем использовать общепринятую арабскую запись 0, 1, 2, 3…, 9, 10, 11, 12… хотя при этом конкретные выражения для правил вывода становятся несколько более сложными, чем требуется. Гораздо более простые выражения получаются, скажем, при использовании записи вида 0, 01, 011, 0111, 01111… для обозначения последовательности натуральных чисел (или, в качестве компромисса, мы могли бы использовать двоичную запись). Однако, поскольку это могло бы стать источником разночтений в дальнейших рассуждениях, я буду для простоты придерживаться обычной арабской записи независимо от способа обозначения, которая может на самом деле использоваться в данной системе. Нам мог бы понадобиться символ «пробел» для разделения различных «слов» или «чисел» в нашей системе, но, так как это тоже может вызвать путаницу, то мы будем по мере необходимости использовать для этих целей просто запятую (,). Произвольные («переменные») натуральные числа (равно как и целые, рациональные и т. д.; но давайте здесь ограничимся натуральными) мы станем обозначать буквами, например, t, u, v, ω, х, у, z, t', t'', 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)],