x
свободна
x
x
y
x
x
A(b) A(?x A).
x
(9)
Здесь A(b) обозначает формулу, полученную из A подстановкой всей формулы b на место переменной x всюду, где она входит свободно.
x
всюду, где она входит свободно
Таким образом, в соответствии с определенными правилами формулы могут быть получены как аксиомы. Дедукция основывается на правиле силлогизма: из двух формул a и ab, полученных ранее, первая из которых стоит слева от символа , мы получаем формулу b.
получены как аксиомы
Дедукция
полученных ранее
получаем
Каким образом предлагает Гильберт убедиться в том, что дедуктивная игра никогда не приведет к формуле 0?0? Вот его основная идея. Пока мы имеем дело только с «конечными» формулами, т.е. с формулами, не содержащими кванторов ?x , ?y , ..., вопрос об их истинности или ложности можно решить, просто посмотрев на них. С присутствием ? такое описательное суждение о формулах становится невозможным — самоочевидность больше не работает. Однако любая конкретная дедукция представляет собой последовательность формул, в которых участвует только конечное число аксиоматических правил типа (9). Предположим, что ?x является единственным квантором и всюду, где он встречается, за ним следует одна и та же конечная формула A. Другими словами, мы имеем дело с формулами типа (9):