Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 134
Текст из файла (страница 134)
«) См, с. 43 — 46. ») См. аналогичное»амечанне на с. 32. 4 П докАзАтельство АккеРИАнА 621 Основной тип данного е-герма мы будем заодно считать и основным типом любого е-выражения, получающегося из рассматриваемого е-герма в результате замены некоторых его свободных переменных связанными. 6. Выбор значений для е-термов целесообразно производить с использованием основных типов.
Нормированные доказательства устроены так, что встречающиеся в них е-термы свободных переменных не содержат. Любой такой е-терм либо совпадает со своим основным типом, н тогда этот основной тип не имеет аргументных переменных и в качестве его значения может быть взята какая- либо цифра; либо же этот е-терм получается из своего основного типа е,«((Е, е,, ..., е») с аргументами переменными е„..., еа в результате замены этих переменных некоторыми термами 1,, ..., 1„. В качестве значения такого основного типа берется какая-нибудь функция, зависящая от переменных вм ..., е„, аргументами и значениями которой являются цифры, причем такая, что ее значение отлично от нуля только для конечного числа наборов значений аргументов.
Пусть Ч~(э„ ..., е») †функц, которая оказывается на месте основного типа е Е (г, е„..., е»). Тогда выбор значения е-герма е Я(х, 1„..., 1„) сводится к нахождению значения ~р(1„..., 1„), а тем самым— к нахождению значений термов 1„..., 1„. Каждый из этих термов либо является цифрой, либо строится из цифр и вычнслимых функций, так что его значение получается в результате соответствующего вычисления, либо же он снова является е-термом или содержит один или несколько е-термов в качестве составных частей.
Тогда для этих е-термов в свою очередь должны быть выбраны их значения. Однако этот процесс в конце концов завершается, так как любой е-терм, фигурирующий в е-терме е Я(е, 1, ..., 1„) в качестве его составной части, имеет меньший ранг. При таком вычислении е-термов вложенным друг в друга е-термам соответствуют вложенные друг в друга арифметические функции, сопоставленные основным типам соответствующих е-термов. Только тем е-термам, которые не содержат в качестве составных частей никаких других термов, соответствует не функция, а число.
Такой способ приписывать значения е-термам, основанный на использовании их основных типов, нацелен прежде всего на то, чтобы избежать циклов, которые могли бы появиться в том случае, если бы мы стали приписывать значения непосредственно самим е-термам. Действительно, в таком случае могло бы оказаться, что совокупность термов, которым должны приписываться значения. в свою очередь зависит от этих значений, Это обнару- 21" 628 ДОКАЗАТЕЛЬСТВО АККЕРМАНА ПРИЛОЖЕНИЕ живается, например, в случае, когда мы имеем дело с критической формулой первого рода, связанной с термом вида Е„Я(х, е»6(х, у)). Если данный е-терм для краткости обозначить посредством е, то всякая связанная с ним критическая формула первого рода будет иметь вид 6((, еваз(1, у))-ьЯ(е, Е„З(е, у)).
Чтобы найти истинностное значение заключения этой импликацин, нам потребуется знать значение терма Е„Я(е, у), и в зависимости от того, какое значение 1 будет придано терму е, нам придется вычислЯть тот или иной е-теРм е»8(1, У). При вычислениях значений с помощью основных типов такого рода осложнений возникать не будет.
Действительно, в этом случае совокупность основных типов, которым должны быть сопоставлены арифметические функции, наперед определяется совокупностью е-термов, фигурирующих в рассматриваемом нормированном доказательстве. Кроме того, описываемый способ обладает тем преимуществом, что при нем формулы, построенные по схеме равенства, всегда, т. е. без дополнительных предосторожностей, принимают значение «истина».
В самом деле, всякая такая формула имеет вид а = 8 -э (Я (а) -ь Я (8)). Если термы а и 8 получат различные значения ш и и, то посылка внешней импликации примет значение «ложь», а значит, вся формула в целом — значение «истина». Если же оба эти герма получат одно и то же значение, то в соответствии с нашей процедурой формуле 6(а) во всех случаях будет отнесено то же самое истинностное значение, что и формуле 6(8), так как каждому терму, входящему в 6 (а) и содержащему а в качестве составной части, в 6 (8) соответствуег терм, тем же самым способом устроенный с помощью терма 8, а потому и в этом случае вся формула в целом снова получит значение «истина». Таким образом, задача установления непротиворечивости нашего формализма сводится к тому, чтобы путем придания е-термам соответствующих значений сделать истинными те критические формулы первого и второго рода, которые могут фигурировать в качестве исходных формул в каких-либо нормированных доказательствах.
С этой целью мы сначала выпишем в некоторой последовательности основные типы всех е-термов, встречающихся в этих критических формулах. Последовательность эту мы выберем таким образом, чтобы основные типы более низких рангов предшествовали основным типам с более высокими рангами. Какое-либо сопоставление этим основным тинам арифметических функций мы будем называть общей заменой'). Любая общая замена однозначно определяет значения в-термов, входящих в критические формулы, а также и всех тех в-термов, которые получаются нз этих термов в результате замены в них одного или нескольких подтермов какими-нибудь цифрами. О терме, который в результате какой-либо общей замены получает в качестве значения цифру 1, мы будем также говорить, что он при этой общей замене редуцируется в цифру 1.
В аналогичном смысле о заданной формуле мы будем говорить, что при рассматриваемой общей замене она редуцируется в значение «истина» или в значение «ложы. Мы будем также говорить, что формула 5 при общей замене Ю редуцируется в формулу е)ы если 5, получается из ет в результате замены фигурирующих в ет термов теми цифрами, в которые они редуцнруются при общей замене 9. Замысел первоначального гильбертовского подхода к устранению е-символов ') заключается в том, чтобы построить некоторую последовательность общих замен, а затем доказать, что уже на некотором конечном шаге она приводит к такой замене, при которой все критические формулы принимают значение «истина». Основная идея этого подхода такова: по критической формуле первого рода 6 (1) -ь Я (е«6 (х)), принимающей при какой-либо общей замене ЕЗ значение «ложы,.
мы сначала находим такую цифру 1„ что формула Я (1) при данной общей замене принимает значение «истина». А именно, если при замене 9 терм 1 редуцируется в цифру 1, то посылка Я (1), а значит и 6 (1), при замене Э должна принимать значение «истина», так как по условию наша критическая формула при этой замене должна быть ложной. Затем от этой цифры 1 можно перейти к наименьшей из цифр и, входящих в список О, О', ..., 1 и таких, что при данной замене Ф формула 6(п) редуцируется в значение «истинаш Обозначим эту цифру через )е. Тогда всякая критическая формула (первого или второго рода) в результате общей замены 9 при замене в ней терма е«Л(у) цифрой 1е будет редуцироваться в значение «истина».
Для критических формул второго рода 6(1)-ье 6(х) ФГ ь) Такое употребление термина «общав эамена» было введено в гл. и на с. 188. Еще раньше этот термин испольэовалсв в несколько ином смысле (см, с, !28). а) См. с. 124 и следующие. ззо ПРИЛОЖЕНИЕ покАЗАтельстзо АккеРмАИА » 11 это верно потому, что для цифры 1п, в которую при общей замене Е редуцируется терм (, либо верна формула («Ф1п', либо — в пРотивном слУчае — из того, что 1п меньше йь следУет, что Я(1п), а значит, и Я(() редуцируется в значение «ложь». И все же попытка воспользоваться этим обстоятельством для построения очередной общей замены наталкивается на трудности из-за большого разнообразия возможных вложений и подчинений е-термов, и потому требуются дополнительные соображения, которые могли бы обеспечить некоторый прогресс при построении очередных общих замен. Такое соображение, выдвинутое В.
Аккерманом, заключается в том, что процесс построения замен должен быть организован таким образом, чтобы каждая общая замена Е удовлетворяла следующему дополнительному условию: если Е,Я (е, с1, ..., с,) — какой-либо основной тип из нашего списка основных типов, а й, ..., ~, — произвольные цифры, и если )— цифра, в которую при общей замене Е редуцируется терм Е„Я (х, й, ..., ),), то либо ) представляет собой цифру О, либо формула Я (й й, ..., ь) редуцируется при этой замене в значение «истина», в то время как для любой меньшей цифры р формула Я(Э„)„..., ~,) при рассматриваемой замене редуцируется в значение «ложыс Общую замену, удовлетворяющую этому условию, мы будем называть допустимой.
Примером допустимой общей замены может служить О-замена„при которой каждому основному типу без аргументов сопо, ставляется цифра О, а каждому основному типу с аргументами— функция с тем же самым числом аргументов, тождественно равная О. В последовательности производимых нами общих замен О-замена всегда будет играть роль исходной. Заметим, далее, что при любой допустимой общей замене И всякая критическая формула второго рода редуцируется в значение <истина». Действительно, любая такая критическая формула, связанная с основным типом е«Я(ь, аы ., а,), имеет, как мы знаем, вид Я(1, а„..., а„) Е,Я(ь, а„..., а,) Ф1', и если при общей замене 9 термы 1, а„..., 1, редуцируются в цифры и,;,„..., ~„а терм е Я(х, )„..., ~,) в цифру й то эта критическая формула редуцируется в формулу Я(п, )1, ..., ),)-+)~п'.
Либо заключение этой формулы является истинным, либо цифры и' и ( совпадают, а тогда и меньше й и потому при общей замене Е, являющейся по условию допустимой, посылка этой формулы редуцируется в значение «ложыь Таким образом, если мы в дальнейшем будем иметь дело с только допустимыми общими заменами, то критическими форму- лами второго рода можно будет больше не интересоваться. Далее, из определения допустимой общей замены вытекает, что при любой такой замене (Э всякий раз, когда какой-либо е-терм, с которым связана динная критическая формула первого рода, редуцируется в цифру, отличную от О, эта критическая формула редуцируется в значение «истина».
Действительно, всякая такая формула Я(х, а„..., а,)-«-Я(е«Я(к, «1, ..., а,), «1, ..., «,) при общей замене Е редуцируется, как мы знаем, в формулу Я (и, ь1, ..., 3,)-+ Я (й )1, .„, Ц, где и, я„..., ь суть цифры, в которые при Е редуцируются термы 1, «1, ..., Е„а ) — значение, принимаемое сопоставленной при этой замене основному типу Е,Я(~, а„..., а,) функцией при аргументах.1„..., ),. Если ~ отлично от О, то формула Я(й )„..., О), а потому и рассматриваемая критическая формула, при допустимой общей замене Ю редуцируется в значение «истина». Кроме того, мы укажем некоторую процедуру, позволяющую по любой допустимой общей замене Е такой, что хотя бы одна критическая формула первого рода редуцируется этой заменой в значение «ложып получить новую допустимую общую замену.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
