Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 135

Процедура эта состоит в следующем: мы рассматриваем те е-термы, с которыми связаны критические формулы, редуцирующиеся при замене Е в значение «ложын Среди основных типов этих е-термов мы берем тот, который в установленной нами последовательности основных типов идет первым. Пусть е«Я (х, а„..., а,) — этот основной тип, и пусть ((1, ..., 5„— критические формулы, связанные с какими-либо е-термами данного основного типа и редуцирующиеся при замене 1п в значение «ложын Терм, с которым связана какая-либо такого рода формула, имеет вид е Я(й, а„... ..., А,). При общей замене Е термы а1, ..., а„редуцируются в некоторые конкретные цифры й, ..., ~„а терм е Я(х, )1, .„ ..., ь) ввиду того, что данная замена является допустимой, редуцируется в цифру О, так как с термом е Я (х, «1, ..., а,) свя. ЕЗЗ ПРИЛОЖЕНИЕ 632 докАЗАтельстэо Аккепманл вана некоторая критическая формула, редуцирующаяся в зна- В чение «ложык Среди г-члеиных наборов цифр, выступаю их такой роли, мы берем тот, который в нумерации этих наборов Щ имеет наименьший номер.

(Мы считаем, что нумерация наборов производится по максимальной цифре, а при равных максимальных цифрах — в лексикографическом порядке ').) Пусть и„..., и,— этот набор. Те из формул 5„..., 5„у которых термы-аргументы связанного с ними е-терма редуцируются в цифры н„..., и„ представляют собой импликации с посылками вида 6((, а..., 1 ..., а,). Каждая иэ этих посылок при замене Э должна редуцироваться в значение «истина», в то время как термы и, ... а е р дуцируются в цифры и„..., п„а г редуцируется в некоторую цифру.

Пусть (е — наименьшая из цифр, в которые редуцируются эти термы й Пусть, далее, ~' — наименьшая из тех цифр и из списка О', О", ..., ~е, для которых формула 6 (и, и», ..., и,) редуцируется в значение «истина». (Цифру О мы исключаем из рассмотрения, поскольку формула Я(О, и„..., п,), как мы знаем, редуцируется в значение «ложые) Затем сопоставленная при замене 9 Основному типу е 6(х, а„..., а,) функция видоизменяется таким образом, что для набора аргументов и„..., п, ее значение полагается равным ~е, в то время как при остальных значениях аргументов ее прежние значения сохраняются.

Для тех основных типов, которые в нашей последовательности предшествуют основному типу е 6(у, аю ..., а,), сопоставленные им функции мы оставляем без изменений, а у следующих за ним основных типов мы возвращаемся к О-замене. Мы теперь покажем, что полученная таким образом, исходя из 9, общая замена Э' тоже является допустимой. Для этого требуется убедиться, что для каждого основного типа е 6(р, сы ..., Еа) из нашего списка основных типов выполняется следующее условие: для любого и-членного набора цифр В|, ..., В„такого, что терм з«6(у, Вд, ..., В„) при замене Э' редуцируется в отличную от О цифру й формула 6(В, гю ..., В„) редуцируется в значение «истина», в то время как для любой цифры р, меньшей й 6(р, й, ..., ~„) принимает значение «ложые При этом мы должны считаться с тем обстоятельством, что в том слУчае, когда основномУ типУ е 6(», Оы ..., Еа) подчинены какие- либо другие е-выражения, в формуле 6(й й, ..., ~,) или соответственно в 6(р, ~м ..., ~„) в качестве составных частей будут фигурировать соответствующие е-термы.

Например, если основной тип н„6(х, с) в подробной записи имеет вид е»Е(х, с, еаф(х, у, с)), ') ТакУю нУмерапню мы уже неволь»овала ранее, см, с. 21« то соответствующая формула 6 (й й) будет записываться в виде Е(Ь, йь Е,$(З, у, ЯИ и, соответственно, 6(р, ~,) будет иметь вид Е(р, (м еаау(р.

у 1»)) Фигурирующие таким образом в формулах 6(~, »,, ..., а„) и 6(р, 3ю ..., 1„) е-термы всегда имеют ранг, меньший ранга е-терма (основного типа) е 6(р, сю ..., Еа). Если теперь основной тип е 6(р, см ..., Ен) в последовательности наших основных типэв предшествует играющему в построении общей замены Э' главную роль основному типу е Я (у, аю ..., а„), который мы для краткости обозначим через е, то основной тип любого е-герма более низкого ранга и подавно будет предшествовать основному типу е, а потому при замене Э' ему будет сопоставлена та же самая функция, что и при замене Э.

Таким образом, основные типы, предшествующие в нашей последовательности основному типу е, при замене Э', как и при замене 9, удовлетворяют условию, сформулированному в определении допустимой общей замены. С другой стороны, для основных типов, следующих за е, это условие при замене Э' выполнено тривиальным образом, так как этим основным типам сопоставлена О-замена. Следовательно, остается рассмотреть основной тип е, т. е.

Е,Я (у, аю ..., а,). Замену 9' мы выбрали так, что для любого г-членного набора цифр ~ю ..., ~„, отличного от набора и„ ..., и„ терм е«6 (у, ~ю ..., ~,) при замене Э' редуцируется так же, как и при 9; кроме того, для любой цифры ( формула 6(й )„..., О) (которая, как мы знаем, может содержать только е-термы ранга меньшего, чем ранг е) при Э' редуцируется так же, как и при Э. Что же касается набора и„..., п„то терм е«6(й, нм ..., и,) при Э редуцируется в цифру ~е, а формула 6()е, пю ..., и,) редуцируется при Э, а потому и при Э'„ в значение «исгина», в то время как 6(р, и„..., и,) при любой цифре р, меньшей ~*, и при 9 и при Э' редуцируется в значение «ложын Таким образом, мы теперь в состоянии построить, исходя из О-замены, некоторую последовательность допустимых общих замен, обладающую тем свойством, что за каждой общей заменой, в результате которой не все критические формулы — здесь речь идет только о критических формулах первого рода — редуцируются в значение «истина», следует новая общая замена, отличающаяся от предшествующей одним значением функции, сопоставленной одному из основных типов (или, в простейшем случае, — сопоставленным этому основному типу числом).

ДОКАЗАТЕЛЬСТВО АККЕРМАНА 634 ппиложгние Теперь мы покажем, что в этой последовательности допустимых общих замен после конечного числа шагов наступает обрыв. Чтобы установить этот факт, мы', следуя Аккерману, введем ряд понятий, которые будут нам полезны в дальнейшем. Приписывание какого-либо отличного от 0 значения функции для одного из основных типов в одной из точек (соответственно приписывание какого-либо отличного от 0 значения для основного типа без аргументов) мы будем называть заменой примером'). Для каждой общей замены, за исключением начальной О-замены, среди основных типов имеется первый, такой, что приписанная ему функция (соответственно число) отличается от функции (числа), приписанной ему в предшествующей общей замене.

Номер этого основного типа в списке рассматриваемых основных типов мы будем называть характеристическим номером данной общей замены, а количество всех таких основных типов, начиная с данного, мы будем называть характеристическим числом этой общей замены. Рассматриваемые общие замены мы будем обозначать в порядке их образования посредством 9», 9„... Общую замену 9» мы будем называть прогрессивной по отношению к предшествующей ей общей замене 9ь если все замены примерами из 9, сохраняются и в 9». При (~й общая замена 9» всегда содержит некоторую замену примером, которая в 9; отсутствует.

Действительно, пусть 9)в замена из списка 9;„, ..., 9„с минимальным характеристическим номером. Тогда заменой 97 вводится некоторая замена примером, не фигурирующая в 9н и эта замена сохраняется и в возможных дальнейших общих заменах, образуемых в соответствии с нашей процедурой построения общих замен.

Пусть п„п„..., а„— список н-термов, каждый из которых имеет основной тип, входящий в наш список основных типов, и пусть вместе с каждым встречающимся в нем е-термом 1 в него входит и каждый е-терм, вложенный в 1, причем на более раннем месте. Чтобы удовлетворить последнему из этих условий, относящемуся к порядку следования е-термов в конечной их совокупности, достаточно нумерацию этих е-термов ввести таким образом, чтобы выполнялись следующие условия: различные е-термы получают различные номера и е-терм, являющийся собственной составной частью некоторого другого В-терма, имеет номер, меньший ') Этим названием отмечается то обстоятельство, что данное, отличное ог 0 значенне функции, вновь соогноснмое обшей заменой основному типу ахй)(г,а„ ....

а„) а точке ц, ..., Ы, прсдстааляег собой пример цифры Ь прн которой формула Ф (Ь ц, ..., 4,) втой общей заменой редуцируется я аначенне «астана». номера этого последнего'). Очередность для е-термов какой-либо совокупности при этом устанавливается так, чтобы эти термы располагались в порядке возрастания сопоставленных им номеров.

Мы зафиксируем какой-либо такой порядок е-термов, и будем называть список, удовлетворяющий указанному условию, норм а л ь и ы м списком В-термов. Под р еду к цио иным числом общей замены 9 относительно нормального списка е-термов п„пы .. и» мы будем понимать значение, принимаемое выражением па 2» + н, 2»-х +... + л»-х 2+ и», г е л (1'=О, ..., й) принимает значение 1 или 0 в зависимости от того, в какую цифру — равную нулю или отличную от него— редуцируется терм п~ при общей замене 9. Нас будут особенно интересоватЬ редукционные числа общих замен 9; относительно двух специальных нормальных списков и-термов: во первых, относительно (упорядоченного в установленной очередности) списка всех е-термов, входящих в рассматриваемые критические формулы первого рода, и, во-вторых, относительно (снова упорядоченного в указанной очередности) списка тех входящих в формулы 6(0, и„..., и,), 6(0', и,, и,), ..., 6()„пы ..., и„) е-термов, с помощью которых при замене 9«находится цифра 1» для следующей общей замены.