Формальные математические системы
Необходимо будет несколько уточнить, что мы понимаем под «формальными математическими системами аксиом и правил вывода». Мы должны предположить наличие некоторого алфавита символов, через которые будут записываться математические выражения. Эти символы в обязательном порядке должны быть адекватны для записи натуральных чисел с тем, чтобы в нашу систему могла быть включена «арифметика». По желанию, мы можем использовать общепринятую арабскую запись 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 », и, возможно, использовать для «возведения в степень» обозначение, более подходящее к рассматриваемому формализму; но, как уже говорилось, я буду придерживаться стандартной системы записи во избежании ненужной путаницы.) Это утверждение (если читать его до левой квадратной скобки) звучит как: