Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 102
Текст из файла (страница 102)
В самом деле, в первоначальном варианте г-правила в подстановках вместо свободных индивидных переменных могут фигурировать только такие термы, которые либо не содержат ы символов, либо являются собственными ытермами,либо построены из собственных !-Термов с помощью функциональных знаков, ') В о в з о г У. В. Оп !Ье Сопв!3(енсу о! !)и!пе"в «)»(вк Роппбзиопв !Ог Ма!Ьзша!!са1 Ьой(с».— !. БугпЬо!!с Ьов!с, 1939, 4, рр.
15 — 24. Зто формальное пзложенкз харзктсркстпк Россер проводит здесь з рамках определенного орызлкзыа и указывает точный метод устрзнепня »-снызолов нз выводов ормул, не содержащих этих спинозов. ') Вместо этих двух акспоы Россвр, который пе пользуется форнульпымп переменными, берет зпалогпчные ны схемы формул.
Заметим, что если в основу рассыотренкя положить обобщенное Олрззпло, то формула [К В), н дзжв '((вп(г) -» В (»„А (з)), оказыэавтся выводимой. 33* 515 понятие «тот, котОРыня и его устРАнимость 1гл ч!и 1 41 УСТРАНИМОСТЬ ХАРАКТЕРИСТИК («-СИМВОЛОВ) 517 Для собственного 1-герма «гЯ (5) формула Я (Я) является выводимой (быть может, с переименованными переменными и и о); поатому аксиома [1, В] дает нам формулу «((х В (х) -1- В (1 «)[ (5)). Пусть теперь й] (с) — формула, в которую вместо переменной с требуется подставить терм 1 Я (5). (Мы предполагаем, что в ре. зультате атого не возникает коллизий между связанными переменными,) Предположим, что в [8(с) не входит переменная х.
Тогда с помощью средств исчисления предикатов мы сможем перейти от [8 (е) к '((х«п (х). А эта формула вместе с ранее полученной формулой )Ух В(х) -«- В (1 ~Я (5)) при помощи подстановки [8 ())) вместо именной формы В (1)) и с применением схемы заключения дает искомую формулу Я (1 «)[ (5)). (если бы переменная х входила в [8(с), то, может быть, потребовалось бы предпринять некоторые переименования.) И наконец, что касается подстановки таких термов, которые построены из собственных 1-термов и функциональных знаков, то эти подстановки могут быть разбиты на подстановки термов без 1-символов и подстановки собственных 1-термов. Пусть, напРимеР, У нас имеетсЯ теРм «]1 («„Я (х), 1Р («о[8 (У))), гДе ф— какой-либо одноместный а «[1 — двуместный функциональный анак.
Пусть 1„«)[ (х) и «Р3(у) — собственные с-термы, и пусть требуется подставить терм «]«(«хе[(х), 1р («Р3(р))) в формулу Ж(е) вместо переменной с (снова предполагается, что при этом не возникнет никаких коллизий между связанными переменными). Тогда мы можем действовать следующим образом: выбрав какую- нибудь не входящую в «е(с) свободную переменную (например, Ь) и какую-нибудь не входящую ни в 6,(е), ни в Я(с) свободную переменную (например, с[), мы сначала подставим вместо с терм ф (Ь, 1р (д)), а затем в получнвгпуюся формулу подставим вместо Ь СОбетВЕННЫй 1-тсры сх'ЛМ(Х) И, НаКОНЕц, В ПОЛуЧЕННуЮ таКИМ образом формучу вместо «1 подставим собственный 1-терм «РВ(у).
Таким образом, мы видим, что с помощью аксиом Россера можно осуществить (в переведенном виде) все те выводы, которые оказываются возможными на основе обобщенного «-правила. А потому, если у нас будет способ, позволяющий устранять характеристики, формализованные в соответствии с аксиомами Россера, то тем самым у нас будет и способ, позволяющий устранять применения «-правила, а также, как мы выяснили, и способ для устранения обобщенного «-правила.
Россеровская формализация характеристик теперь может быть упрощена путем объединения аксиом [1] и [1, В] в формулу (1) «[(А) -«- (я((х (А (х) -я- В (х)) -я. В («„А (х))). В самом деле, подставив в эту формулу А (с) вместо В (с) ') и используя выводимость формулы чх (А (х) — А (х)), мы получим средствами исчисления высказываний формулу [1]; а формула [1, В] получается из (1) при помощи исчисления высказываний с использованием выводимой формулы ЧхВ (х) -я- ух (А (х) — ~ В (х)). С другой стороны, (1) можно получить на [1] и [1, В], подставив в [1, В] А (е) -а. В (с) вместо В (с), что даст нам формулу ЩА) -я- (Я(«х (А (х) -я.
В (х)) — ~ (А («„А (х)) -э В («„А (х)))), которая вместе с [1] средствами исчисления выскааываний дает формулу (1». На возможность такого объединения аксиом Россера в одну- единственную аксиому указал Гисберт Хазенъегер, который разработал и во многих отношениях упростил предложенный Россером метод устранения 1-термов в применении к произвольным теориям, формализуемым в рамках исчисления предикатов с аксиомами раненства ').
В дальнейших рассмотрениях мы по существу будем придерживаться данного им доказательства. Наконец, для подготовки планируемого нами устранения 1-термов целесообразно методом возвратного переноса подстановок в исходные формулы исключить, как это делалось в гл. «(1 з), подстановки вместо формульных переменных. Но атот метод должен ограничиться исключением подстановок вместо формульных переменных. Сами формульные переменные могут и не исключаться; они остаются для образования алементарных формул. Но вместо тех исходных формул, которые содержат формульные переменные, мы должны будем использовать соответствующие схемы форяиул. Теперь напомним структуру тех формальных систем, для которых мы после проведенных приготовлений будем доказывать устранимость «-символов.
Формулами их являются либо элементарные формулы, либо формулы, образованные из других формул при помощи символов ') Подстановки вместо фсриульиых псремеииых ыы здесь ие сгрзиичиеаеы. Впрочем, фсрыульиые переменные вскоре будут исииючеиы из рессыстэеиия. ) Этз работа «Вег Ьез11шш1е Агс!ие1 пп Ргзйраа«евйа1йи1« (мзрт 1952 г.) з печати ие появлялась. Положенный з вей е осисеу изложения формализм расширенного исчисления предииетсз отличается ст формализма, призедеиисгс з гх. 1У и га. У, ие считая других иезизчихеэьиых различий, теы что е иеы иет подстаисзок вместо фсрыульиых переменных.
Впрочем, Хазеиъегер псиьзуетси ие формулой (1), з дедуктивно рззисй ей (изиду аксиом равенства) формулой 1~х (А (х) х = «) Е«В (с) -я В («хй (х)) ичи соответствующей ей схемой формул. а) Сы. с. 275 и далее. 519 понятия ятот, которыя» и нго Устрлнимость 1гл, Уп) ы УстРАнимость ХАРАктвРистик 1ысимВОлОВ) 519 логики высказываний и кванторов. Внелогическими символами являются знак равенства и, быть может, какие-нибудь другие предикатные символы, а также индивидные символы и функциональные знаки. В качестве переменных в них имеются свободные и связанные индивидные переменные, а также, быть может, свободные формульные переменные. Всякая элементарная формула состоит либо из формульной переменной без аргумента, либо ив формульпой переменной с термами в качестве аргументов, либо из предикатного символа с термами в качестве аргументов.
Терм есть либо свободная переменная, либо индивидный символ, либо функциональный знак с термами в качестве аргументов, либо «-терм, т. е. терм вида ) Я (т), где Я(с) — формула, содержащая свободную переменную с и не содержащая связанной переменной Х. В качестве исходных формул у нас имеются: 1) собственные аксиомы; 2) формулы, построенные по одной из следующих схем формул: а) схемы тождественно истинных формул исчисления высказываний; формулы, построенные по схеме такого рода, мы будем называть формулами, истинными в логике высказываний; б) схемы, соответствующие основным формулам (а) и (Ь) исчисления предикатов: 'ФхЯ (х)-ьЯ (а), Я (а) — ьЭхЯ (х); в) схема, соответствующая аксиоме равенства (г»): а = Ь -+ (Я (а) -)- Я (Ь)); г) схема, соответствующая аксиоме ()): Эх7у (Я (у) у = х) -ь- ()ех (Я (х) -ь.
ц) (х)) -)- Й («„Я (х))); д) быть может, схема, соответствующая аксиоме индукции '): Я (О) А. )) х (Я (х) -«- Я (х')) -+ Я (а). В качестве правил вывода у нас имеются: схема заключения, схемы (а) и (Р) для кванторов всеобщности и существования, правило подстановки вместо свободных индивидных переменных термов, не содержащих )-символов, и правило переименования свяаанных переменных.
Среди аксиом должна быть формула а = а, если она не является выводимой. 3. Определение редукции формулы и сведение требующегося доказательства к доказательству выводимости без «-символов для формул, построенных по определенным схемам. Устранимость 1) Если рассматриваемая формальная система содержит схему индукции з качестне праннла, то »то праннло (кан показано в гл. Ч1, с.
324 — ЗЗО) может быта сведено к степе формул, соотнвтствуюшей аксиоме индукции. «-символов из выводов таких формул, которые сами )-символов не содержат, будет устанавливаться таким образом, что каждой формуле Я будет сопоставляться некоторая ее «редукция» з((г1) '), которая является формулой беа )-символов и которая совпадает с Я в том случае, если Я является формулой бев «-символов.
С учетом такого определения редукции провозглашенная нами устранимость будет доказана, если из каждого Вывода формулы 6, осуществленного в формализме описанного типа, мы сможем извлечь вывод формулы зт()й), не содержащий )-символов. Этот факт будет установлен, если мы сможем показать, что: 1) редукция всякой исходной формулы может быть выведена без использования 1-символов; 2) если в применении какого-либо правила ыы заменим посылки этого правила их редукциями, то из этих редукций можно будет без испольаования )-символов вывести редукцию формулы, получаемой по этому правилу. Теперь речь пойдет о том, чтобы ввести соответствующее понятие редукции формулы.
С этой целью мы условимся, что редукция формулы, построенной из элементарных формул с помощью логических символов исчисления предикатов, будет в точности тем псе самым способом строиться иа редукций элементарных формул. Таким обравом, редукцией формулы Я й )Э будет э1(Я) сч )з((ц)), редукцией формулы )Я будет 1%(Я); аналогично для Ч', -ь и . Редукцией формулы У 5 Я(5) будет 752((Я(З)), редукцией формулы ЗЗЯ(р) будет Эуй(')1(~)) (здесь Я(Я(З)) означает выражение, которое получается ив формулы о((Я(с)) со свободной переменной с, не входящей в Я(т), в результате замены с на т). Эти соглашения мы будем кратко называть перестановочностью оператора редукции с логическими операциями. Теперь нам нужно еще дать определение редукции для случая элементарной формулы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
