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

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

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

Кроме терма г, здесь фигурируют только е-термы, имеющие основной тип е„(с=у). В качестве символов, играющих роль функциональных замен для этого основного типа, мы будем брать фУнкциональные знаки ф,(с), фе(с), ... Применяя к данному списку формул нашу процедуру построения общих замен, мы должны будем начать с замены основного типа е„(с=у) такой функцией ф,(с), которая всегда принимает значенйе О. Если мы внесем эту замену Е, в формулы (1) и (2), то получим формулы (1 ) (фг (!') = О -«; = 1) -«(фг (е;) = О -«г, = !), (2*) ( р, (6 (е,)') = О -«6 (гг) = !) -«г, Ф 6 (г,) ', где е, обозначает е терм е„(грг(х') =0-«х=1) ранга 1.

Для этой пары формул, в которой содержится единственный е-терм г„мы получим резольвенту в два шага Е;в и Е;, Функциональные замены проводить здесь не нужно, так как основной тип е, (ф,(х ) = а-«х = 6) терма е, повсюду фигурирует только с аргументамя О и !. Сначала мы заменим терм г, цифрой О. В результате этого формула (2*) станет истинной, а формула (1е) — ложной. Из (1е) мы находим для е, экземплярную замену 1, которая одновременно является и минимальной. Эта замена г, цифрой ! является резольвентой формул (1') и (2"). Однако общая замена Е,д, получающаяся из этой замены Е;, и замены Е„ не является резольвентой для формул (1), (2) и (3). Действительно, в результате этой общей замены терм г переходит в цифру 1, терм е„(г =у) переходит в цифру О, и потому формула (3) оказывается ложной. А теперь из формулы (3) мы для терма ее(!=у) получим экземплярную замену г, которая в то же время является и минимальной, Таким образом, мы должны теперь взять для герма е„(с = у) новую функцию замены ф,(с), принимающую значение ! в точке г и значение 0 в остальных точках.

В результате внесения этой замены Е, в формулы (!) и (2) мы получим формулы (! *") (р, ( ) = О-«! =,;) -«(гр, (г;) = 0-«г, = !), (2**) (грл (6 (гл)') = О-«6 (е,) =-.') -«е, ~ 6 (ге)', где е, обозначает терм е„(ф,(х') =0 — «х=г). Терм е, опять является единственным фигурирующим в этих формулах е-термам. Поэтому с помощью цифровых замен для г, мы в два шага Е;, и Е;н получим резольвенту, Сначала, при замене те)гма гл цифрой О, формула (2**) станет истинной, а фор- Ю исследовкние крнфметнки при помоши а-символл [гл.

и е 41 пегвонлчлльнып гильиеитовскип подход 161 мула (1**) — ложной. А затем из (1'а) мы получим для е, экземплярную замену !. Если бы мы не должны были заботиться о критической формуле второго рода (2), то резольвента тем самым уже была бы получена. Но экземплярная замена ! для герма е, не является минимальной, и это проявляется в том, что при замене герма ее цифрой ! формула (2'*) переходит в ложную формулу. Минимальную замену для ее дает предшествующая цифре)цифра ! — 1.

1В самом деле, формула сра((! — 1)') =О, как мы знаем, является ложной, и поэтому при замене с, цифрой ! — 1 заключение импликации (1**) становится истинным, в то время как при замене ее цифрой, меньшей чем ! — 1, формула (1**) становится ложной.! Таким образом мы должны теперь заменить терм е, цифрой 1 — 1 и эта замена Е;, является резольвентой для формул (1*а) и (2*а). Однако при получающейся из замен Е„', и Е, общей замене Е,л для формул (1), (2) и (3) формула (3) становится ложной, так как терм е получает значение 1 — 1, а терм е„(! — 1=у) — значение О.

Теперь нз формулы (3) для герма е„(1 — 1=у) мы получаем экземплярную замену ! — 1, которая вместе с тем является и минимальной. В соответствии с этим мы должны построить для основного типа в„(с=у) новую функциональнУю заменУ ~Ра(с), котоРаЯ длЯ аРгУмента 1 пРинимает значение й для аргумента 1 — 1 — значение 1 — 1, а для прочих аргументов — значение О.

Таким образом, перед нами случай, когда экземплярная замена, получающаяся при двух различных, но эффективно равных заменах из одной и той же критической формулы, ведет к двум различным минимальным заменам. Действительно, обе общие замены Е„и Еел дают для термов е, вр(!'=у), ер(е'=у), е„(6(е)'=у) и е„(е=у) значение О и, следовательно, они эффектйвно равны; обе они по формуле (1) дают для терма е экземплярную замену 1; однако онн дают различные минимальные замены. Действительно, в то время как при замене Е,, в качестве минимальной замены для е получается цифра 6 при замене Е„ в качестве минимальной замены для е получается ! — 1.

Если теперь проследить процедуру построения общих замен для формул (1), (2) и (3), то обнаружится, что она завершается только на (1+1)-й строке замен. В каждой из первых ! строк будут стоять по две общие замены. В последней строке будет стоять только одна. Общие замены Ер ! и Ер 2 (р= 2, ..., 1) устроены таким образом, что основной тип е„(с=у) заменяется в них функцией Фр(с), принимающей для ! значение 6 для ! — 1 значение е — 1, ..., для 1 — (р — 2) значение 1 — (à — 2), а в прочих случаях значение О, и что е-терм при замене Ер ! заменяется цифрой О, а при е,„— цифрой 1 — () — 1); при общей замене Е1+,, основной тип е„(с=у) получает замену в виде такой функции, которая для любой цифры г, удовлетворяющей условию О'(г =.1, принимает значение г, а при прочих значениях аргумента — значение О.

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

В самом деле, мы обнаружили, что необходимость перехода от экземплярных замен к минимальным, вследствие которой наличие критических формул второго рода сказывается на нашей процедуре, мешает лишь обоснованию утверждения 6'), а в остальных отношениях наше доказательство, оценивающее число требующихся общих замен, остается в силе.

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

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

!50. а) Ом. с. 153 и далее, 5 Д. Гааьберп П. Бьрааас 162 ИССЛЕЛОВАНИЕ АРИФМЕТИКИ ПРИ ПомощИ а-СИМВОЛА 1ГЛ. Н ПЕРВОНАЧАЛЬНЫЙ ГИЛЬБЕРТОВСКИЙ ПОЛХОД 1ВЗ 4 41 Возникает естественный вопрос: насколько шырок арифметический формализм, получающийся в результате наложения этого ограничения) Критические формулы второго рода появляются в нормированных доказательствах из-за того, что мы свели использование схемы индукции к использованию формулы А (а) — Е„А (х) Ф а' в сочетании с е-формулой, аксиомой равенства ()»), формулой а~О- б(а)'=а и средствами исчисления высказываний').

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

е. когда в 6(с) переменная с не попадает в область действия каких-либо и-символов. Сказанное относится к формулам, получающимся после исключения кванторов (о помощью е-символа). Для интересующего нас арифметического формализма, содержащего кванторы, это сводится к требовани1о, чтобы переменная с в формуле 6(с) не попадала в область действия каких-либо кваиторов или е-символов.

Тем самым установлена непротиворечивость той части формализма (Х), которая получается путем ограничения схемы индукиии такими формулами 6(с), в которых переменная с не попадает в область дгиствия каких-либо кванторов или В символов. Это условие является несколько менее ограничительным, чем условие полного исключения связанных переменных, которое имелось в рассматривавшейся нами «ограниченной схеме индукции»'), Но для упомянутой части арифметического формализма мы получаем не только доказательство непротиворечивости, но и всю нашу нп-теорему ') в полном ее объеме.

В самом деле, непротиворечивость эта доказана нами в том смысле, что установлена истинность любой выводимой формулы без перемениых. Что же касается выводимых формул вида :-(~„" ЭВ,21(~„", Ц, ') См. с. 11В и далее. а) См. с. 1П вЂ” 119, а) См. с. 77 и далее. '] См. с. 59 и далее. у которых единственными входящими в них переменными являются Г,, ..., х„то любая такая формула в результате операции исключения переменных переходит в формулу вида 6(еи " Ре), где е,, е,— некоторые В-термы, такую, что вие этих термов она ие содержит никаких переменных, а внутри этих термов не содержит свободных переменных. Для формулы 6(е,, ..., е„) мы можем получить нормированное доказательство.

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

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