Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 105
Текст из файла (страница 105)
Но этот последний, как мы заметили, не>может совпадать ни с каким из термов >„5> (яп с); х> следовательно, он должен находиться среди терман ар 6> (у>), для которых при переводе [11 в [2] или соответственно [1х] в [2х1 соответствующие члены %(6>(у>)) не претерпевают никаких изменений. Поэтому вдесь окаэыэается возможным скомбинировать процедуру, посредством которой (в простейшем случае) формула (1) переводится в формулу (2), с процедурой перевода Н1 в [21, а также с процедурой перевода [1х] в [2х].
Тем самым во всех этих случаях редукция формулы (а) оказывается выводимой беэ использования >-символов. Теперь мы должны рассмотреть случаи, когда формула 3(с) содержит хотя бы один символ логики высказываний или квантор. В этих случаях 3(с) либо имеет один из видов >З,(с), 4>~З, (~), Лгй> (т), либо состоит иа двух формул 3> (с) и За (с), соединенных друг с другом при помощи одной из связок &, 'Ч', -а., К формуле 3> (с), фигурирующей в первых трех случаях, и к формулам 3> (с) и 3 (с), фигурирующим в остальных случаях, мы можем применить наше индукционное предположение.
Однако нам не нужно рассматривать все эти случаи в отдельности, так как свяэки логики высказываний можно выраэить через конъюнкцию и отрицание, а формулу 34Я(г) можно преобразовать в ТФ~ ] Я(х). Ввиду перестановочности оператора редукции с логическими операциями, эти преобраэования формул переносятся и на их редукции, причем таким образом, что если в результате этих преобрааований формула 3 (с) переходит в 3" (с), то в результате тех же самых преобразований И (3 (с)) перейдет в И (3* (с)), а И (3 (а Я (х))) — в % (3* (а „Я (х))).
Итак возможность вывода беэ а-символов формулы (И, Я, 3*) приведет к аналогичной возможности и для формулы (И, Я, 3). Поэтому — после того как для элементарных формул 3(с) мы установили выводимость (И, >[, 3) без использования >-символов — нам будет достаточно индукцией по числу логических символов в 3 (с) показать, что: (1) если наше утверждение о выводимости (%, Я, 3) без использования а-символов справедливо для формулы 3 (с), то оно будет справедливо и для формулы > 3(с); (2) если оно справедливо для формул З> (с) и 3 (с), то оно будет справедливо и для формулы 3, (с) & Зе (с); (3) если оно справедливо для формулы 3(а, с) (с отличной от с и не входящей в Я (х) свободной переменной а), то оно будет справедливо и для формулы а>рй (~, с). Во всех требующихся здесь доказательствах мы снова ь же польаоваться теоремой о дедукции, вследствие чего установление выводимости ге»>г д гаИ, .1, 3) сводится к установлению выводимости формулы [%, Я, 3(х)] 7х (% ('>! (х)) И (3 (а))) % (3 (а~Я (х))) фор у.
ц (И (Я)). Таким образом, для того, чтобы установить (1), мы должны удем — в предположении, что формула (И, Я, 3) может быть выведена с помощью 0 (% (Я)) без испольэования а-символов,— доказать, что без использования а-символов может быть выведена и формула [И, Я, > 3(х)1, т. е. 'Ух(%(Я (х))-+-%( ЗЗ(х))) — а-И (-> 3(>,Я (х))).
Формулы ]а (% (Я)) и (И, Я, 3) по схеме заключения дают эквивалентность [%, Я, 3 (х)]. Ваяв отрицания обеих ее частей и выполнив затем преобразования по правилам исчисления предикатов, мы получим формулу Зх (И](Я (х)) & -> И (3'(х))) -'~'И (З,(ахй (х))) и, вследствие перестановочности отрицания с оператором редукции, формулу йх(%(Я(х))8 %(.ч 3(х)))-%(-1 3(>,Я(л))). Иа формулы ц (И (Я)), как незадолго перед этим было эамечено, мы можем вывести формулы единственности для И (Я (а)), а из этих последних мы получим формулу [3] пх(И(Я (х)) & В(а)) чх(%(Я (х))-+ В(х)), и во всех этих выводах будут отсутствовать >-символы.
Иэ формулы [3], подставив И( > 3 (с)) вместо В(с), мы получим формулу 3х (И(Я (х)) & %(-> 3(х))) 'Фх(%(Я (х))-а И (-] 3(х))), которая вместе с полученной ранее эквивалентностью средствами исчисления высказываний дает нам искомую ло м л [%, Я, > 3 (х1). омую формулу Ввиду наличия вспомогательной формулы ц (И (Я)), в случаях (2) и (3) речь идет о том, чтобы иэ двух эквивалентносте" Я, 3> (х)1 и [%, Я, За (х)] вывести эквивалентность и !И, Я, 3> (х) & За (х)], а из [И, Я, 3 (а, х)] вывести эквивалентность [%, Я, 'Ф~й (х, а)] (мы здесь предполагаем, что переменная а не входит в Я (х)). э4 д. гильэерь и. верлаае 531 устРАнимость хАРАктеРистик и символов) 530 ИОнятие «тот, котОРыи«и его устРАнимость )гл.
Т111 Но эти все выводы мы немедленно получим с помощью исчисления предикатов, опираясь на перестановочность оператора редукции с логическими связками. б. Формулировка теоремы об устранимости; переводимость всякой формулы в ее редукцию; сравнение различных методов устранения. В общем и целом, наши последние рассуждения приводят к следующему результату: Будем исходить иа некоторой формальной системы, состоящей из расширенного (при помощи аксиом равенства) исчисления предикатов, к которому могут быть добавлены какие-нибудь собственные аксиомы, а также, быть может, аксиома индукции (соответственно схема индукции).
Если совокупность термов такой системы расширить путем соотнесения формулам Я(с) 1-термов 1 Я (5) и если дополнительно принять в качестве аксиомы формулу (1) или же добавить соответствующую схему формул, то зто не расширит запаса выводимых формул, не содержащих 1-символов. Или, как мы еще будем говорить: иг вывода любой формулы, не содержащей 1-символов,1-символы могут быть устранены.
Ввиду сказанного въппе '), устранимость эта будет иметь место и для выводов, в которых 1-термы вводятся и используются в соответствии с нашим первоначальным 1-правилом, и для выводов, использующих обобщенное 1-правило. Одновременно мы установили, что для всякой формулы, выводимой с использованием 1-правила, ее редукция выводима беа использования 1-символов. В дополнение к сказанному мы покажем, что если допустить выводы с использованием 1-правила г), то всякая формула 5 будет переводима в свою редукцию. Мы докажем это индукцией по числу логических знаков в $, причем 1-символы также будем причислять к логическим знакам.
Для случая, когда рассматриваемое число равно нулю, наше утверждение тривиально, так как 5 тогда не содержит 1-символов и тем самым Ж ($) совпадает с )у. Если 5 составлена из каких-либо других формул с помощью связок логики высказываний, то это утверждение может быть получено средствами исчисления высказываний на основе нашего индукционного предположения. В том случае, когда 5 имеет один иа видов ~У5$1 (5), 3551 (5), это утверждение совершенно аналогичным образом может быть получено средствами исчисления предикатов на основе имеющегося у нас индукционного предположения.
Остается рассмотреть случай, когда )у является элементарной формулой )р (1 Я, (51),..., 1 Я, (5 )) с внешними 1-термами Я 1 (Ь1) ° ° 151 Яг («1) ' 1) См с 515 †5 ') Гдэ фвгураруют, следоэателъио, толъно собственвые с-термы. редукция формулы 5 в этом случае имеет вид Г)51 Щ (Ж(Я1(5~)) & & Ж(я,(5,))-+ ~(5О ..., 5 )) На основании сделанного нами~индукционного предполо ен выводимы аквивалентности Ж(Я1(с~)) Я~ (с1), ..., Ж(Я,(с,)) (со свооодными переменными с„..., с ). Эти переменные мы выберем так, чтобы они не входили в формул У 11ъ Далее, для каждой формулы Я, (1 = 1,..., 1) мы распола- гаем соответствующими формулами единственности, из кото ых при помощи 1-правила и аксиомы равенства (31) могут быть выве- дены эквивалентности ') Я1(с1) с1=1 .Я~(51) (1=1, ..., 1).
Эти эквивалентности совместно с эквивалентностями, приве- денными вьпйе, дают формулы Ж(Я;(с1)) с1=1«,Я~(51) (1=1, ..., 1), из которых, применив нужное число раз аксиому равенства (3 ), мы получим импликацию Ж(Я (с))& . &Ж(Я1(се))- ($("г Я1(51) . 15 Яг(51))-'ф(с« ..: с4 а отсюда с помощью исчисления предикатов — формулу 5 — ъ)751 . )У51 (Ж (Я1 (51)) & ... & Ж (Ят (5г)) — ъ )Р (а1,, ле)), т.е.
формулу 5-~-Ж(5). С другой стороны, импликация Ж (5) -ъ 5 получается следую- щим образом. Мы исходим из импликации 'У51(Ж(Я1(51)) & & Ж(Яг(51))- ~~(51 51 )- (Ж(Я1(с1)) & " &Ж(Яг(сг))- $(с1 . сг)) выводимой средствами исчисления иредикатов. Посылка этой импликации представляет собой формулу Ж (5). Если вместо переменных сг,..., с, подставить 1-термы 1. Я, (51) 51) формула $. Таким образом, мы получим формулу Ж(5) (Ж(Я (1Г,Я й ))) & &Ж(Яг(17,Яг(51))) 5) Но формулы Я1(1 Я, (11)) (1 = 1,..., 1) выводимы с по- мощью 1-правила, и, следовательно, формулы 9'(Я. (1, Я ( ))) 11 1 (А1И ') Сы. с.
471. 1 5! СЛЕДСТВНЯ ИЗ УСТРАНИМОСТИ ХАРАКТЕРИСТИК 533 ПОНЯТИЕ «ТОТ, КОТОРЫЕ«И ЕГО УСТРАНИМОСТЬ [ГЛ. ЧН1 532 являются выводимыми (даже без использования с-символов). Следовательно, средствами исчисления высказываний получается формула Я(5) -«- 5. Из выведенных таким образом импликаций 5-+. Я(5) и Я(5) -«. 5 мы полечим эквивалентность Я(5) )7. Таким образом, опираясь на индукционное предположение, мы установили, что зта эквивалентность выводима во всех подлежащих разбору случаях. Замечание.
В первом издании атой книги доказательство устранимости с-символов было проведено прямо для первоначального с-правила, причем было показано, что всегда может быть устранено последнее введение с-герма. Индукция такого рода оказалась, однако, чрезвычайно утомительной. Курт Шютте привел существенно более простое доказательство!), в котором за основу берется то же самое первоначальное с-правило, но индукцня ведется таким образом, что уменьшается максимальная «степень» с-выражения, причем под степенью выражения с,сл(х) понимается число встречающихся в нем с-символов. Вместе с тем доказательство Шютте дает более сильный результат, так как оно относится и к таким формальным системам, в которых имеются свободные и связанные функциональные, а также связанные формульные переменные и в которых 1-символ употребляется в сочетании с функциональными, а также с формульными переменными, так что формализованными оказываются также характеристики функций и предикатов.
По сравнению с методом, предложенным Шютте, примененный нами метод Россера — Хазенъегера допускает несколько более легкую проверку, поскольку главная часть рассуждения ограничивается в этом случае рассмотрением одной-единственной схемы формул» 5). ') См. его работу: Я с Ь 6 1 с е К. Вде Е1!шш!егЬаг1сем йее Ьеес!шшсеа Агсйсе1е 1в Кой)1!Ьасев йег Ааа1уе!е.— МасЬ, Аэв., 1951, 123, Я. 166 — 186.
») Укажем также ва доказательство устраввысстя характеристик, пряэедеввсе э учебнике: К 1 е е п е Я. С. 1О1гсйас1шв сс Месашасйешас!се.— Аше1егйаш, 1952 (есть русский перевод: К л я в я С. К. Введение э ыетаматемагяку.— Ми ВЛ, 1957 — арин.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
