Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 39
Текст из файла (страница 39)
1). Вместе с тем, в результате произведенных замен формулы 9„..., 9) перейдут в формулы 9"„..., 91, так что вместо фор- мулы у нас появится формула 91* 81... Ее 9~ -е- Же, из которой с помощью элементарного преобразования мы получим дизъюнкцию ~9~ Ч ". Ч ) 9) Ч ~)* Значит, и эта дизъюнкция получается в результате подстановок из тождественно истинной формулы исчисления высказываний. Любая из формул 9;, ..., 91 имеет, как и соответствующие формулы из числа 9ь ..., 9б один из двух видов Е=Ь вЂ” 1.(А)(а)- Ал(Ь)), а=Ь- (((в)=1(Ь)), где АА — какой-либо предикатный символ, а ( — функциональный знак, отличный от знаков („..., )в (кРоме Указанных аРгУмен- тов эти символы и знаки могут иметь и какие-нибудь другие; отметим также, что Ае может быть и знаком равенства). К дизъюнкции мы применим правила ()е) и (ч)').
Применив нужное число раз )С,с, 178, ч 2) Включение Аксиомы (л! ВО ВТОРую е-теОРему 179 правило ()е) к дизъюнктивному члену )9"; (где ) является одним нз чисел 1, ..., 1), мы получим вместо него такой дизъюнктивный член ф), который получается из отрицания некоторой специальной аксиомы равенства в результате замены входящих в него свободных индивидных переменных переменными, связанными кванторами существования, стоящими в начале этого дизъюнктивного члена. Отрицание ) ф) любого такого члена можно перевести в такую формулу, которая получается из некоторой специальной аксиомы равенства в результате замены свободных индивидных переменных связанными и потому выводима из формулы (зе) с помощью исчисления предикатов. В результате применения правила (р) к дизъюнктивным членам )91, ..., ~97 из формулы ) 9е Ч " Ч 19) Ч ~* получится формула 4 Ч ".
Ч ФЧ~) * Так как входящие в нее формулы ф„..., ф не содержат свободных переменных, то применение правил (У) и ()е) к дизъюнктивным членам Т' может быть произведено таким образом, как если бы формула Х' стояла отдельно; как было показано ранее, мы можем таким образом преобразовать каждый, дизъюнктивный член формулы Т,е в формулу 6, так что в итоге получится формула $ Ч".ЧФ) Ч9Ч" Ч9 которую затем можно будет преобразовать в формулу ~$181...81 1$)-е Ж. Таким образом, эта формула выводима средствами исчисления предикатов. Но так как формулы 1А1„..., )ф, как ужеотмечалось выше, выводимы из (зе) с помощью исчисления предикатов, то мы получаем вывод формулы 9 из формулы ()е), осуществляемый средствами одного только исчисления предикатов. Тем самым показано, что вторая е-теорема остается справедливой и в том случае, если в рассматриваемый формализм Р будет включена аксиома равенства (Д,).
В частности, отсюда получается следую1цая. Т е о р е м а. Пусть Р— расширенный логический формализм, получающийся из исчисления предикатов путем добавления к нему знака равенства, аксиом равенства (з1) и (де), е-символа и е-формулы, Тогда всякая выводимая в формализме Р формула, не содер- 161 !80 е.СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ [ГЛ Ри ВКЛЮЧЕНИЕ АКСИОМЫ (Л1 ВО ВТОРУЮ е-ТЕОРЕМУ жащпя вхождений е-символа, будет выводима в г и без использования е-символа. Следовательно, если какая-либо формула, построенная из символов и переменных исчисления предикатов и знака равенства, может быть выведена с использованием, кроме правил исчисления предикатов и аксиом равенства (ЯА) и (3е), еще и символьных решений некоторых экзистенциальных формул, то эти символьные решения из данного вывода могут быть устранены.
Более того, из доказанного следует, что если какая-либо формула 6 выведена с помощью исчисления предикатов, аксиом равенства и каких-либо собственных аксиом, а также с привлечением операции символьного решения экзистенциальных формул и если ии один из введенных при этом символов в формуле (в не встречается, то эти символьные решения из вывода 6 могут быть устранены. Вместе с тем метод, с помощью которого нашу вторую е-теорему мы распространили на аксиому (Яе), позволяет также доказать следующее утверждение: Если формула 6, построенная из символов и переменных исчисления предикатов и каких-либо индивидных, функциональных и предикатны символоо, но не содержащая знака равенства, выводима с помощью средств исчисления предикптов, е-формулы и аксиом равенства, то она выводима и средствами одного только исчисления предикатов.
Из этого утверждения, в частности, следует, что из вывода любой формулы чх, обладающей указанными свойствами, производимого с помощью средств исчисления предикатов и аксиом равенства (,)А), (де), применение аксиом равенства может быть устранено. Эту теорему мы в свое время доказали для случая, когда формула 6 представляет собой формулу исчисления предикатов '). Приведенное там доказательство немедленно распространяется на случай формулы (у, содержащей индивилные или предикатные символы, но оно не может быть распространено на случай, когда в (у встречаются функциональные символы.
Доказательство мы снова начнем с замечания о том, что без ограничения общности можно считать, что формула СУ имеет вид сколемовской нормальной формы. Далее, в точности так же, как раньше, получается, что, используя вывод формулы К можно найти некоторую формулу и). л, 11 С1)- г ° обладающую следующими свойствами: .1) См. т. 1, с. 462 — 466. 1. Эта формула получается в результате подстановки из неко- торой тождественно истинной формулы исчисления высказываний.
2. Каждая из формул я, ..., Иу имеет один из двух видов а = Ь вЂ” (О (а) — А! (1 )), и = Ь е- (1 (о) = ( (Ь)), где Π— некоторый предикатный, а ( — некоторый функциональ- ный символ; эти символы, кроме указанного аргумента, могут содержать и какие-нибудь другие, причем последние в ~(а) и в О(Ь) и соответственно в 1(а) и в 1(Ь) должны быть совпадаю- шими. 3. От формулы ь* можно вернуться к формуле 6 с помощью средств одного только исчисления предикатов. Из связи, существующей между формулой Ве и формулой Аг., которая, по предположению, не содержит знака равенства, кроме того, вытекает, что формула хе тоже не содержит знака равен- ства. Действительно, формула ц-, как мы знаем, имеет вид 'ЗУ'"ЛУ,11«1" 1У«е«1(~м "., «е), а Же представляет собой дизъюнкцию, члены которой получаются из формулы е((ьх «е) в результате замены связанных переменных ум ..., «4 некоторыми термами.
Свойство 1 сохранится и в том случае, если в формуле ййе ф д (яе г е мы заменим формулой А 1~ ) А каждое встречающееся в ней равенство с одинаковыми термами в левой и правой частях и формулой Ай ПА — любое другое равенство. Действительно, совпадающие элементарные формулы при этом всюду будут заменены одинаковым образом. В результате этой замены всякая формула а = Ь вЂ” (О (а) — О (Ь)) или соответственно а=6-+-(((в) =((Ь)) перейдет, если терм а отличается по внешнему виду от терма Ь, в некоторую формулу АЬ1 А- ч), а если В совпадает с 1 — в некоторую ~(орчулу А ~/ 1 А — ~ (Св -+.
(з) Е.СИМВОЛ И ЛОГИЧЕСКИЙ ФОРМАЛИЗМ !гл.ш или соответственно в формулу А т/ ) А -+ А л/ 1А. Таким сбразом, в результате указанной замены каждая формула Е"; (1=1, ..., 1) перейдет в такую формулу (л)1, которая может быть получена подстановкой из некоторой тождественно истинной формулы исчисления высказываний, между тем как формула ллэ при этом останется без изменений. А теперь, так как формула (блй...3 олт-~Жэ и каждая нз формул 6л, ..., (лд! получаются подстановкой из некоторой тождественно истинной формулы исчисления высказываний, то же самое можно будет сказать и относительно формулы Т". Но из Ж' с помощью исчисления преднкатов может быть получена формула 6. Таким образом, как и утверждалось, формула 6 может быть выведена средствами одного только исчисления предикатов. Доказанная теорема немедленно может быть обобщена следующим образом: Если из какой-либо системы аксиом, состоящей из аксиом равенства (34), (Д,) и каких-либо собственных аксиом, не содержащих знака равенства, с помощью исчисления предикатов выведена некоторая формула 6, не содержащая знака равенства, то применен е аксиом равенства из ее вывода может быть исключена.
Зта усиленная вторая е-теорема позволяет нам получить новое доказательство теоремы об устранимости л-правила' ), так как с введением е-формулы л-правило становится производным, а е-символ берет на себя роль л-символа '). Но это доказательство устранимости л-правила распространяется только на такие формализмы, которые получаются из исчисления предикатов с л-правилом путем добавления каких-либо собственных аксиом и, может быть„аксиомы равенства (Ят), в то время как прежняя теорема была доказана с включением аксиомы полной продукции.
Наоборот, для формализма системы (Е), содержащего н аксиому индукции, справедливость утверждения второй з-теоремы можно вывести из теоремы об устранимости л-правила. Действительно, как было показано ранее'), в этом формализме при добавлении л-правила можно определить символ )л„А(х), для которого с помощью л-правила выводится формула А (а)- А ()А„А (х)). л) См.
т. 1, с З11, л) Слл. с. 34. э) См. т. 1, с. 479 — 482 или Приложение !. 4П ВКЛЮЧННИК АКСИОМЫ СЛ> ВО ЗтОРНЮ э-тИОРЕМН 183 Поэтому, если вывод некоторой формулы 6, принадлежащей формализму системы (Е), производится с помощью исчисления предикатов и аксиом системы (Х) с добавлением е-символа и е-формулы, то применения е-символа и е-формулы в этом выводе могут быть заменены соответствующими применениями л-правила. Но в силу упомянутой теоремы об устранимости л-правила эти применения л-правила могут быть исключены, так как в формуле 1х отсутствуют вхождения л-символа, и, таким образом, мы приходим к некоторому выводу формулы 6 из аксиом системы (Е), осуществляемому средствами одного только исчисления предикатов '). В тех случаях, когда устранимость л-правила может быть выведена из второй е-теоремы, конечно, можно иметь дело прямо с е-символом и е-формулой, а не с л-правилом.
В качестве примера мы рассмотрим вопрос о замене функциональных знаков предикатными символами. В свое время этот вопрос мы подвергали анализу с помощью теоремы об устранимости л-правила'). Идущее дзлее рассуждение имеет менее общий характер, поскольку оно не охватывает полной индукции; но, с другой стороны, нынешний результат, в отличие от прежнего, будет относиться не только к таким формализмам, которые включают в себя аксиомы равенства. Мы будем исходить из формализма Р, получающегося из исчисления предикатов добавлением знака равенства, аксиом равенства (лт) и (5э), а также некоторых дополнительных символов: индивидных, функциональных и предикатиых, вместе с какими- либо собственными аксиомами лЛА, ..., Яв.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
