A(b) A(?x A(x)).
(8)
При этом не обязательно выбирать представителя однозначным способом; наше конкретное правило действует лишь в случае, когда x пробегает множество чисел 0, 1, 2, ... Вместо этого мы будем считать, что квантор ?x обладает универсальной приложимостью и в каждом случае выбирает для нас некоторого представителя. Аксиома выбора Цермело оказывается, таким образом, вплетенной в принцип исключенного третьего. Это смелый шаг, но чем смелее, тем лучше; лишь бы быть уверенным, что мы остаемся в рамках непротиворечивости!
В формализме пропозициональные функции заменяются формулами, обращение с которыми должно быть описано без ссылок на их значение. В общем случае переменные x, y, ... будут встречаться среди символов некоторой формулы A. Мы говорим, что символ ?x связывает переменную x в формуле A, если он предшествует этой формуле 25, и говорим, что x свободна в формуле A, если она не связана квантором с индексом x. При этом x, y, , ?x представляют собой символы, входящие в формулу; готические буквы не применяются для обозначения таких символов, а используются для коммуникации. Нашу основную аксиому (8) более естественно рассматривать как правило для образования аксиом. Она выражает следующее: возьмите любую формулу A, в которой x является единственной свободной переменной, и любую формулу b без свободных переменных и с их помощью образуйте новую формулу
|
A(b) A(?x A). |
(9) |
Здесь A(b) обозначает формулу, полученную из A подстановкой всей формулы b на место переменной x всюду, где она входит свободно.
Таким образом, в соответствии с определенными правилами формулы могут быть получены как аксиомы. Дедукция основывается на правиле силлогизма: из двух формул a и ab, полученных ранее, первая из которых стоит слева от символа , мы получаем формулу b.
Каким образом предлагает Гильберт убедиться в том, что дедуктивная игра никогда не приведет к формуле 0?0? Вот его основная идея. Пока мы имеем дело только с «конечными» формулами, т.е. с формулами, не содержащими кванторов ?x , ?y , ..., вопрос об их истинности или ложности можно решить, просто посмотрев на них. С присутствием ? такое описательное суждение о формулах становится невозможным — самоочевидность больше не работает. Однако любая конкретная дедукция представляет собой последовательность формул, в которых участвует только конечное число аксиоматических правил типа (9). Предположим, что ?x является единственным квантором и всюду, где он встречается, за ним следует одна и та же конечная формула A. Другими словами, мы имеем дело с формулами типа (9):
|
A(b1) A(?xA), ..., A(bh) A(?xA). |
(10) |
Предположим, кроме того, что формулы b1, ..., bh конечны. В этом случае можно произвести приведение, заменяя формулу ?xA каждый раз, когда она встречается в нашей последовательности, некоторой конечной формулой r. В частности, формулы (10) примут вид