Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 108
Текст из файла (страница 108)
Тем самым мы произвели переход от системы (2) к такой рав. носильной ей системе аксиом, в которой вместо функциональных знаков фигурируют предикатные символы. В этой системе аксиом формулы единственности Бх Ай(а, Ь, х) и БхМр(а, д, х) как аксиомы оказываются ненужными. Действительно, формула БхАй(а, Ь, х) с помощью модифицированной аксиомы индукции и формулы единственности Эх ЯЧ (а, х) может быть выведена из тех двух формул, которые представляют рекурсивные равенства для а + Ь; аналогично, формула ЗхМр (а, Ь, х) с помощью модифицированной аксиомы индукции и формулы БхАй(а, Ь,с) может быть выведена из двух формул, появившихся вместо рекурсивных равенств для а Ь.
Таким образом, после замены связанных переменных свободными во вторых формулах единственности для символов Бч, Ай и Мр, мы вместо системы (2) получим, не считая аксиом равенства, следующие аксиомы: зх ЯЧ (а, х), ЯЧ(а, Ь) АЯЧ(а, с)-»Ь=с, ЯЧ (а, с) 8с ЯЧ (Ь, с) -». а = Ь, 1Бч(а, О), Ай(а, Ь, с) 8сАй(а, Ь, й)-~-с=й, Ай(а, О, а), Ай (а, Ь, с) 8» ЯЧ (Ь, г) 8» ЯЧ (с, г) — ~ Ай (а, г, г), Мр(а, Ь, с)8»Мр(а, Ь, й) — ~с=8, Мр (а, О, 0), Мр (а, Ь, с) А ЯЧ (Ь, г) йс Ай (с, а, з) -» Мр (а, г, г), А (0) 8» Чх Чу (ЯЧ (х, у) 8»А (х) -~А (у)) — |-А (а).
Количество аксиом при переходе от системы (2) к (Хе) увеличи- лось на четыре; а именно, добавились две формулы единственно- сти для Яч и по одной для Ай и для Мр. Теперь еще можно будет исключить при помощи явного опре- деления символ О. В самом деле, из аксиомы -1 ЯЧ (а, 0) 544 поннтие етот, кОтОРый» и его УстРАнимость 1гл, Рш СЛЕДСТВИЯ ИЗ УСТРАНИМОСТИ ХАРАКТЕРИСТИК средствами исчисления предикатов мы получим сначала 'Фг-1 Яб[ (г, 0), а затеи 3х'Уг 1Яц(г, л). Тем самым оказывается выведенной первая фориула единствен- ности для Уг ~ Яц (г, а). Вторую формулу можно получить из формулы ЪЪ-~ Яц(г, а)-а.а =О, которая сама получается применением модифицированной аксиомы индукции.
Теперь ь-правило в сочетании с только что приведенноййформулой дает нам равенство [4[ 0 = Ь„'Рг -1 Яь[ (г, Х). Аналогично току, как мы поступали при исключении функциональных символов, мы можем снова обратить дедуктивную связь, ваяв в качестве аксиом формулы единственности Зх'Рг ~Я~[(г, х), 'йх1ау фг 1ЯИ(г, х) бе'Рг 1ЯО(г, у)-е х=у), которые мы ранее вывели с использованием символа О, а в каче- стве явного определения для символа 0 равенство [4) (после введения при помощи ь-правила терма гиЧг-МЯЧ (г, х)).
Теперь, опираясь на эту модификацию формалиама, мы можем следующим образом провести исключение символа 0: сначала вместо этого символа мы всюду подставим определяющий его г-терм, а затем применим процедуру исключения ь-символов. Если для замены б-терна б„1гг -1 Яц (г, х) при выполнении нашей процедуры взята переменная Ь, то аксиома -1 Яб[ (а, 0) перейдет в выводимую средствами исчисления предикатов формулу 'Р г -1 Яб[ (г, Ь) -э ~ Яц (а, Ь), а три остальные формулы системы (Ее), содержащие символ 0 (т. е.
формулы Аб[ (а, О, а), Мр (а, О, 0) и модифицированная аксиома индукции), превратятся соответственно в формулы 'Рг -1 Яе[ (г, Ь) — Ай (а, Ь, а), 'Р г -1 Яд (г, Ь) — ь Мр (а, Ь, Ь) и ~г -1 Яц (г, д) А А (Ь) бс Чх Чу (Яц (х, у) А- А (х) -ь Л (у)) — ь А (а), которые нужно будет взять в качестве аксиом вместо этих формул. 11аконец, сказывается еще и то обстоятельство, что из аксиомы индукции в новом ее виде может быть выведена вторая из связанных с терман ь„)гг -1 Яд (г, х) формул единственности, которую мы взяли в качестве аксиомы. Действительно, если вьы в новой аксиоме индукции вместо формульной переменной с ниенной формой Л (с) подставим формулу Рг-1Яц(г,с)-+.с = Ь, которую сокращенно обозначим посредством е[ (с), то ввиду выводимости фориулы й (Ь) а- т Уу (Яи (., у) б И (. ) -.
й (у)) мы получим формулу Чг -1 Яб[ (г, Ь) — ь- Я (а), которая в подробной записи имеет вид Чг -1 Яь[ (г, Ь) -+- (Чг -~ Яц (г, а) — +- а .—..- Ь); из этой формулы элементарным преобразованием с заменой свободных переменных связанными мы получим нужную нам формулу единственности. Таким образом, в качестве аксиомьг она оказывается ненужной. Другая формула единственности Зхуг ~ Яц (г, г) в новой системе аксиом замещает прежнюю аксиоиу 1 Яь[ (а, 0). В итоге вместо системы (Е) мы получили некоторую систему (Е*а), не содержащую никаких основных арифметических знаков, кроке предикатяых сииволов Яц, АЙ и Мр.
Изложенный на этом примере метод исключения функциональных знаков и нндивидных символов играет важную роль в вопросах сведения целого ряда проблем, имеющих отношение к аксиоматическоиу методу, к проблемам специального типа. С другой точки зрения введение функциональных знаков и инднвидных символов может оказаться, наоборот, выгодным; в частности, иногда оно может быть использовано для частичного исключения экзистенциальных аксиом и для замены оставшихся 35 д. Гиньберт, П. Бернайс ДОБАВЛЕНИЕ 546 ПОНЯТИЕ «ТОТ, КОТОРЫЕ» И ЕГО УСТРАНИМОСТЬ [ГЛ.
У[Н 1 з) такими аксиомами, в которых встречаются только свободные переменные. Например, если мы произведем обратный переход от системы (Езз) к системе (Е), то в результате введения штрих-функции аксиома йхЯ[1 (а, х) окажется ненужной, а вместо аксиомы лх)[[я [ Яг[ (з, х) появится аксиома а' чь О, не содержащая связанных переменных. В расчете на это упрощение мы ввели в гл. у1 штрих-символ и символ О ~), и с помощью этих символов паы удалось описать общу[о модель двух систем формул (Ж) и ($) при помощи системы аксиом без связанных переменных. Теперь возникает вопрос о том, всегда ли исключение экзисз тенцнальных аксиом путем введения функциональных знаков и иядивидных символов может быть реализовано в виде перехода к некоторой равносильной системе аксиом.
Этим вопросом, который нашими предыдущими рассмотрениями был положительно решен лишь в отдельных случаях '), мы займемся в общем виде в начале следующего раздела нашего сочинения. Обсуждение этого вопроса попутно приведет нас к доказательству уже упоминавшейся ранее теоремы Эрбрана з), а отсюда — к преодолению той проблематики, с рассмотрения которой и начались наши исследования (мы имеем в виду наши зомнения в достаточности моделей финитной арифметики для установления непротиворечивости тех или иных систем аксиом). Но проблема установления непротиворечивости ни в коем случае этим не исчерпывается, дая е если мы ограничимся формализмом системы (Е) с добавлением фуякции )[ А (х).
Мы только знаем из теоремы об устранимости з-символов, что в предположении непротиворечивости системы (Е) непротиворечивой оказы- ') См. с. 267 — 279. То, что штрпх-сяызол, введенный язык з целях язображзяия ззаямво однозначного соответствия [з смысло модели форкул (Й)), з то же самое время поззаляет усилить зкзязтеяцизльяую аксиому лу (з ( у) до аксиомы а' С а, валяется сзззобразвой особенностью давяого случая. з) К зтяы случаям ыы еще вернемся при общем обсужлепяя проблемы з) См.
гл. [У, с. 169. вается и та система, которая получается из (Е) в результате присоединения символа )з 4 (х) и добавления к числу аксиом фо м л ( ) ( ) и ()з ). Но непротиворечивость самой системы (Е) не вытекает ни из предыдущих результатов, з р ормул )[з, )зз ии из тео емы Эрбрана. К доказательству непротиворечивости системы (Е) и к связанным с этим фундаментальным вопросам мы вернемся в последнем разделе нашего сочинения.
з 6. Добавление: распространение теоремы о возможноств замены аксиомы равенства (1з) в случае добавления з-правила Здесь мы покажем, что доказанная в гл. У11 теорема о возможности замены аксиомы равенства (уз)или соответственно схемы равенства а = Ь-+. (Я (а) — »- Я (Ь)) специальными собственными аксиомами равенства ') остаетси справедливой и в случае добавления ыправила з).
Наше рассмотрение с самого начала будет относиться к формализмам беа фо [ульных переменных, и в соответствии с этим аксиома равен- форму ь ства будет нами приниматься в виде схемы. Мы будем исходить из рассуждения, приведенного в гл. чУ 1. '111 Нами было показано, что если формула Я (а) построена из индивидных переменных, предикатных символов, индивидных символов и знаков для математических функций с помощью символов исчисления предикатов, то формула а = Ь -»- (Я а) -»- и (Ь)) ( может быть выведена средствами исчисления предикатов из сле) дующего списка аксиом, который мы для краткости обозначим через (1): 1. Формулы а=а, а = Ь -».
(а = с-«. Ь = с). 2. Формулы вида а = Ь-». (%(а)- »)з(Ы). ') Сы. с. 456. ') В первом вздзнви язшзй книги зто доказательство проводилось вучеы установления устрапвмостп»-сиыззлоз. В новом пзыевеввоы зариавтз этого доказательства вак вет пзобходвмзстя отдельно рассматрвззть случай, когда»-сяыволы ужз устрзяены.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
