Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 101
Текст из файла (страница 101)
Наши соглашения относительно обращения с г-символами, которых, как мы видели, вполне достает для математического обихода, с точки зрения теории доказательств имеют определенные недостатки. Один из них вытекает непосредственно из того обстоятельства, что выражение «„Я(х) мы допускаем в качестве терма лишь тогда, когда для Я(с) выводимы соответствующие формулы единственности. Отсюда в частности следует, что свойство выражения быть термам не распознаваемо по его внешнему виду и может зависеть от доказуемости того или иного предложения з). Еще одним недостап«ом Оправила является то, что при добавлении этого правила перестает действовать теорема о дедукции.
В самом деле, обычное доказательство этой теоремы здесь не проходит, так как схема Оправила при добавлении соответствующей посылки к ее формулам пе сохраняет своего вида,атакжеине г) Сы. с. 468. «) На зго обстоятельство указывал, е частности, Р. Кзрвап е своей кппге «Меашпз ппй Иесе»ецу» Я 7. 1пд«УМпа1 Пееспр«1опе) . (Иыеетея русский перевод: К е р и а и Р. Значение и необходимость. — М., ИЛ, 1959; сы.
с. 72.— Прим. нерее.) 542 ПОНЯТИЕ аТОТ, КОТОРЫИа И ЕГО УСТРАНИМОСТЬ [ГЛ. Ч111 »4[ УСТРАНИМОСТЬ ХАРАКТЕРИСТИК 4а СИМВОЛОВ) 548 переходит в такую схему, выводимость которой непосредственно усматривалась бы. Мы сможем устранить оба зти недостатка, если, во-первых, условимся выражение 4 Я(5) (с какой-либо связанной перемен- ной 5) считать термам всякий раз,когда ![(е) является формулой, и, во-вторых, примем в качестве формальной аксиомы соответ- ствующую схеме 4-правила формулу ЗхА (х) 84 'Фх1Уу (А (х) 84 А (у) -р. х = у) -а А (4 А (х)). Этой аксиоме мы можем придать и несколько более простой вид, использовав то обстоятельство, что формула ЗхА (х) 84 'Ух'Фу (А (х) 81 А(у) -а- х = у) переводима с использованием аксиомы равенства (3») в формулу Эх (А(х) 84'Фу (А(у) -+-х = у)), а эта последняя переводима с использованием обеих аксиом равенства в формулу З [у(А(у) = ). В соответствии с этим, в качестве формальной «4-аксиомы» мы можем взять формулу (4) ЭхЧу (А(у) у = х) -э А (1„А(х)).
Исходя из атой аксиомы и воспользовавшись формулой ЗхА(х)АЧх'Фу(А(х)84А(у)-а-х=у)-+-Зх~Уу(А(у) у=х), мы немедленно получим схему 4-правила в качестве производного правила. Таким образом, с формальной точки зрения неограниченное допущение выражений 4 о[(8) в качестве термов н придание формуле Ы статуса формальной аксиомы являются обобщением 4-правила. С другой стороны, это обобщение оказывается несущественным, поскольку с помощью исходного 1-правила мы можем ввести такие термы, которые будут играть роль 4-термов в смысле обобщенного 4-правила.
Это удается проделать способом, совершенно аналогичным тому, с помощью которого мы в арифметическом формализме при посредстве исходного 4-правила ввели символ [4 4 (х), длн которого затем оказалось возможным вывести формулы (р,), ([4»), ([4») '), Обозначим посредством Ц(А) формулу ЛН~Ь (А (и) Р = и). ') Сн. с. 48[ — 482. Применим 4-правило к формуле ([4(А) -~ А (а)) 84 ( 1Я(А) -~ а = 4[), которую сокращенно обоаначим посредством 6(а). С помощью исчисления высказываний можно получить формулы Я (А)-а-(б (а) А (а)) и Ю (А)-э(6 (а) а = 8), а отсюда, так как переменная а не входит в ЩА), можно получить Я (А)-а-'ФЗ(4» (Х) А (З)) И ~Я (А) -4.1ЗЗ(6 (г) Х= 4[).
Первая из этих формул вместе с формулой Ц(А) -~ Зх А (х) 84 'Фхуу (А(х) й А (у) -э х = у) (которая, согласно сказанному выше, мо1кет быть получена с помощью исчисления предикатов и аксиом равенства) при помощи средств исчисления предикатов дает формулу Я(А) — ~Эх 5 (х) АЧУхаУу(6(х) А 6(у)-а-х=у).
Вторая иэ пих совместно с формулой Зх (х = 8) 84»[хну (х = д А у = 8 — ~ х = у), которая получается с использованием аксиом равенства, аналогичным же образом дает формулу ~0 (А) -р Эх б,(х) 84 ЧМу(Ж(х) 81 6(у)-+ х=у). Две полученные таким образом формулы дают нам 3х % (х) 8а 1Ух'Фу ([4 (х) А. 4» (у) — г х = у). Тем самым мы вывели конъюнкцию обеих формул единственности для 4» (а).
Поэтому, согласно 4-правилу, мы можем ввести выражение 4„6 (х) в качестве терна и сверх того получить 6( „6(х)), а счедовательно и [[(А) А ( „а (х)), ~[[(А) „„Е (,) Коли мы теперь положим 4(юА (х) = 4„4»(х), т. е. введем определение 4ы1А(х)=4,((Ю(А)а-А(х)) 8а( ~[[(А) — а-х=д)), то полученные нами формулы перейдут в Эи1УР(А(р) О=и)-~А(4~ 1А(х)), 1ЛПЧР (А (р) и= и) а- 41"1А (х) = 4[, 88 д. Грльбарт, П. Варнава 514 ПОННТНЕ «ТОТ, КОТОРЫИ» И ЕГО УСТРАНИМОСТЬ !ГЛ, УП! 1 3! устРАнимость хАРАктеРистик (г симВОлОВ> 515 В силу первой нз этих двух формул терм де)А (х) будет играть ту роль, которая обобщенным ыпраеилом отводится терму г„А (х). Далее, для каждой формулы Я (с) (не содержащей переменной х) !(ЮЯ (х) также является термам, а формула 11 (Я) -ьЯ (г„Я!(х)) (с быть может требующимся переименованием переменных) является выводимой формулой, В том случае, если формулы единственности для Я (с) окажутся выводимыми, мы получим Я (»!е)Я (х)) и (непосредственно с помощью г-правила) Я(!„Я (х)), а тем самым и !<")Я (х) = = !„Я (х).
С другой стороны, если одна из формул единственности для Я (с) окажется опровержимой, то мы получим г(е)Я (х) = д. Что касается свободной переменной Н, которая фигурирует в нашем рассуждении в качестве параметра, то вместо нее мы можем взять какой-либо индивидяый символ, если в формальной системе, в которой мы вводим характеристики, такой символ содержится; тогда тем самым будет устранена зависимость от этого параметра. В противном случае, для того чтобы избежать нежелательных совпадений, мы возьмем вместо д такую свободную переменную, которая не будет встречаться в рассматриваемых нами выводах.
Содержательный смысл выражения ф>Я (х) заключается в следующем. Если Я (с) представляет собой какой-нибудь предикат, а д — какой-нибудь объект индивидной области, то в том случае, если этот предикат выполняется в точности для одного объекта пндгшидной области, »(юЯ (х) как раз и будет являться этим объектом; в противном случае !!зе)Я (х) будет представлять собой объект д. Применительно к нашей цели, состоящей в доказательстве устранимости характеристик, проведенное нами рассмотрение дает следующий результат: Ясли бы мы располагали способом, повеоляющим устранять такие ытермы, которые вводятся по первоначальному ипраеилу, то мы смогли бы устранить и применение ытермое, вводимых на основании обобщенного ыпраеила (мы всюду предполагаем, что речь идет о выводах, заключительные формулы которых не содержат г-символов).
Действительно, в любом выводе, использующем обобщенное ыправнло, всякий встречающийся в нем терм ! Я (5) мы смогли бы заменить соот- 5 ветствующим термам з~~)Я (5), а этот терм мы могли бы ввести в соответствии с первоначальным ыправилом; в самом деле, соответствующие формулы единственности могут быть получены из формул Эх (5 (х), »((х'((у (б (х) дг Я (у) -~- х = у), выводимость которых была установлена ранее, путем подстановки Я (с) вместо формульпой переменной А (е). Из преобразованного таким образом вывода !-Термы, согласно нашему предположению, могут быть устранены.
Таким образом, устранимость исимволов достаточно будет доказать для первоначальной версии иправнла. 2. Россеровский подход и его упрощение, произведенное Хазенъегером; подстановка г-термов; аксиома (3); свойства рассматриваемых формальных систем. И все-таки для целей нашего доказательства оказывается выгодным воспольаоваться такой формализацией характеристик, которая представляет собой нечто среднее между нашим первоначальным и обобщенным иправилами.
Втот способ формализации характеристик, восходящий к Россеру '), заключается в том, что, хотя для каждой формулы Я (с) (не содержащей связанной переменной 5) выражение г Я (5) и допускается в качестве герма, тем не менее возможность подстановки ытермов вместо свободных индивидных переменных ограничивается такими термами, для которых соответствующие им формулы единственности оказываются выводимыми. Термы такого типа мы будем называть собственными !-термами. В этом случае, как и в случае обобщенного иправила, в качестве аксиомы мы возьмем формулу [ь[: )1 (А) -» А (1„А (х)), а подстановку ытермов формализуем с помощью аксиомы ') [!, В] 0 (А) -ь (»((х В(х) -+.
В (г„А (х))). Пользуясь атой аксиомой и правилом подстановки вместо свободных индивидных переменных, ограниченным термами без Оснмволов, можно произвести все те подстановки вместо свободных индивидных переменных, которые могут быть осуществлены, если за основу взять наше первоначальное иправило.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
