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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 32)

Сначала мы берем для основных типов ранга 1 замену со сплошными О-значениями. Эту замену мы символьно вносим в критические формулы и формулы е-равенства ранга выше 1. В результате этого мы получаем некоторый список формул Яе, имеющий ранг а. Теперь к этому списку мы применяем процедуру построения п,оледовательности общих замен. Каждая общая замена для осно1ных типов списка Я, вместе с заменами для основных типов ранга 1 списка Я дает нам некоторую общую замену для И.

Действительно, для каждого основного типа ранга 2 или выше эта замена получается из замены для соответствующего основного типа в И„который получен из исходного основного типа в результате внесения замен для подчиненных ему а-выражений. Так мы приходим к некоторой последовательности общих замен Е,„Е,„... для списка Я. Возможно, что эта последовательность замен оборвется. Однако это случится лишь в том случае, если в процессе построения общих замен для списка И, мы дойдем до резольвенты. Если при этом соответствующая замена для И тоже окажется резольвентой, то на этом вся процедура заканчивается.

Если же этого не произойдет, то по крайней мере одна критическая формула, принадлежащая списку И, при соответствующей общей замене Еь й должна будет превратиться в ложную формулу, причем эта критическая формула будет формулой ранга 1, потому что общая замена Еь ! получается из некоторой резольвенты для списка Я, и, значит, в результате этой замены критические формулы, имеющие ранг выше 1, превратятся в истинные формулы.

') См. утвержденна ! а 2 аа с, !30, е) См. с. 46. ПЕРВОНАЧАЛЬНЫЙ ГИЛЬБЕРТОВСКИЙ ПОДХОД 149 !48 исследОВАние АРЯФметики пРи помОши Б.симВОПА !Гл и 4 И С другой стороны, ни одна критическая формула второго рода, имеющая ранг 1, не может оказаться ложной, потому что замены для основных типов ранга 1 являются заменами со сплошными О-значенивми.

Таким образом, в результате общей замены Еь 4 по крайней мере одна критическая формула 'и'(1)-» 6(В Я(Л)) первого рода превратится в ложную формулу. При вычислении значений этой формулы, вообще говоря, необходимо пользоваться заменами для основных типов ранга 2 и выше. Но так как сама эта критическая формула является формулой ранга 1, то эти замены сказываются лишь на вычислении значений некоторых е-термов, входящих в формулу 4Л (с). Следовательно, как и в случае, когда имеются только В-термы ранга 1, по каждой критической формуле ранга 1, становящейся при общей замене Е, ! 4 ложной, мы получаем некоторую экземплярную, а затем по ней и минимальную замену. Зту минимальную замену мы потом сможем использовать для построения новой замены для основного типа того е-терма, с 'которым связана рассматриваемая формула. Мы построим теперь новые замены для основных типов ранга 1, изменив замены со сплошными О-значениями теми цифровыми и функциональными значениями, которые получаются из найденных минимальных замен.

Этн измененные замены мы затем внесем в критические формулы и формулы е-равенства ранга выше ! и в результате по этим формулам получим список формул И„ имеющий ранг а. К И, можно будет снова применить процедуру построения последовательности общих замен, и всякая полученная таким образом общая замена для И, дает нам вместе с заменами для основных типов ранга 1 некоторую общую замену для списка формул И. Итак, мы получаем некоторую последователь. ность общих замен для И: Еим Е,„... Эта последовательность может оборваться только тогда, когда мы получим резольвенту для списка И,.

Если соответствующая общая замена окажется резольвентой для И, то выполнение всей нашей процедуры заканчивается. В противном случае в результате рассматриваемой общей замены Р, ! хота бы одна критическая формула ранга 1 станет ложной, причем эта формула будет критической формулой первого рода. Действительно, в случае критической формулы второго рода и (1) — Р Б„Л (Б) -ь 1' терм ЕБЛ (Л) в результате этой общей замены получит либо значение О, либо такое цифровое значение, которое представляет собой минимальную замену [либо для самого терма е 4Л(х), если он является основным типом, либо — в противном случае — для терма, в который переходит терм Б 'Л(х) после внесения вместо встречающихся в нем аргументов его основного типа значений, получающихся из этой общей замены1.

Тем самым любая критическая формула второго рода в результате этой общей замены перейдет в истинную формулу. Поэтому снова по крайней мере одна критическая формула первого рода, имеющая ранг 1, в результате этой общей замены должна будет стать ложной формулой, и, значит, мы получим одну или несколько экземплярных замен, а по ним — минимальные замены, которые для замен основных типов ранга 1 дадут новые отличные от О цифровые значения и значения функций. Поставив этн новые цифровые значения и значения функций на место прежних О-значений, мы получим новые замены для основных типов ранга 1. В результате внесения этих замен в критические формулы и формулы е-равеиства ранга выше 1 мы получим по этим формулам некоторый список формул И„ имеющий ранг а. К нему можно снова применить процедуру построения поеледовательности общих замен.

Каждая из получаемых при этом общих замен для И, дает некоторую замену для И, и мы получаем таким образом последовательность общих замен для И Е,„Е,„... Зта последовательность может оборваться лишь в том случае, когда мы получим некоторую резольвенту для списка И,.

Либо соответствующая общая замена списка И является резольвентой для И, и тогда вся наша процедура заканчивается, либо при рассматриваемой общей замене должна оказаться ложной какая- либо критическая формула ранга 1, причем это будет формула первого рода. Тогда снова получатся экземплярные и минимальные замены, которые ведут к новым заменам для основных типов ранга 1. Действуя таким образом, мы можем неограниченно продолжать эту процедуру до тех пор, пока на некотором этапе не будет получена резольвента. Тем самым по обладающей указанными свойствами процедуре построения общих замен для списков формул ранга а можно на самом деле получить процедуру, которая будет аналогичным образом работать над списками ранга а+ 1, а отсюда рекурсивно получится аналогичная процедура для списков с произвольным рангом.

Эта процедура устроена, в частности, таким образом, что при каждом переходе от одной общей замены к другой модификация этой замены заключается только в том, что либо вместо О-замены 150 исследоВАние АРиФметики при помощи е-симВОлА 1гл.!! ПЕРВОНАЧАЛЬНЫЙ ГИЛЬЕЕРТОВСКИЙ ПОДХОД 15! появляется некоторая другая цифровая замена, либо (в случае функциональной замены) функция замены для некоторых (в конечном числе) систем значений аргументов вместо старого значения, равного О, приобретает некоторое новое значение.

Отсюда также следует, что все фигурирующие в рассмотрении функции замены получают отличные от О значения лишь для конечного числа значений (или соответственно систем значений) аргументов. Замечание. Если исходный список формул И имеет ранг 2, то списки И„И„... суть списки ранга 1. Поэтому при получении резольвент для этих списков можно обойтись без метода функциональных замен, т. е. можно ограничиться одними цифровыми заменами.

Значит, в этом случае, не меняя нашей процедуры в прочих отношениях, можно ограничить применение основных типов для замен выражениями ранга !. Такая процедура целесообразна, в частности, тогда, когда все имеющиеся е-термы ранга 2 имеют степень, равную единице; в этом случае построение резольвент для списков И„ИМ ... удается осуществить рассмотренным вначале прямым способом. д) Построение резольвенты в случае, когда все критические формулы являются формуламн первого рода. Описанный метод построения общих замен пока еще не приводит нас к поставленной цели. Все еще остается нерешенной существенная задача— показать, что применение указанного метода всегда приводит к обрыву процесса. Такое доказательство удается получить лишь для случая, когда все критические формулы второго рода„входящие в рассматриваемый список, имеют ранг 1.

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

Эта Оценка строится рекурсивным образом. Как мы уже знаем '), для любого списка формул, имеющего ранг 1, количество общих замен, требующихся для построения резольвенты, не превышает 2", где и — число различных е-термов, входящих в данный список формул. 1) См, е, 145 В далее. Предположим теперь, что для любого конкретного числа В! нам известна оценка сверху Ч1(п) для наибольшего числа общих замен, требующихся для построения резольвенты с помощью нашей упрощенной процедуры (т. е. путем прямого использования экземплярных замен) для любого списка формул, имеющего ранг и!, состоящего только из критических формул первого рода и формул в-равенства и содержащего не более и различных е-термов. При этом предположении мы найдем соответствующую оценку для списков, имеющих ранг В1+!.

Характеристики

Список файлов книги