Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 50
Текст из файла (страница 50)
Аналогичные выводы можно построить, основываясь на форму- ле (Ь) и схеме (р). Еще одной исходной формулой, содержащей формульную переменную с аргументом, является вторая аксиома равенства а = Ь -+. (А (а) -э А (Ь)). Если мы подставим в нее вместо именной формы А (с) формулу ф (а) = ф (с), то получится формула а = Ь -«. (ф (а) = ф (а) -+. ф (а) = ф (Ь)), а из этой последней — перестановкой посылок— ф (а) = ф (а) -+.
(а = Ь -~ ф (а) = ф (Ь)). Если мы теперь учтем формулу ф (а) = ф (а), ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ 238 239 РЕШЕНИЕ ПРОБЛЕМЫ РАЗРЕШИМОСТИ 1гл, Р то которая получается из формулы (1,) в результате подстанов , применив схему заключения, получим формулу кн, а = Ь -)- )р (а) = ц) (Ь). Совершенно аналогичным образом можно вывести следующие две формулы: а = Ь -» ф (а, е) = ф (Ь, с), а = Ь -э. ф (е, а) = ф (е, Ь); производя подстановки во второй из них, мы получим с = д -». ц) (Ь, с) = ф (Ь, д), а из формулы а =Ь вЂ” ~(Ь=с — )-а=с) в результате подстановок получается ф (а, с) = »Р (Ь, е) -»- (ф (Ъ, е) = ))) (Ь, д) -)- ф (а, с) = ф (Ь, г()) Эта формула вместе с двумя предшествующими а = Ь-+.)))(а, с) =ф(Ь, с), е = д-)- )() (Ь, е) = ф (Ь, а)) по правилам исчисления высказываний дает нам формулу а = Ь с«с = г(-)- ф (а, е) = ф (Ь, д).
Вообще, тем же самым способом, что и формулу а = Ь -»- )р (а)= ц) (Ь), можно вывести любую формулу а = Ь -«- 1 (а) = 1 (Ь), где 1 (а) и 1 (Ь) получаются из герма 1 (с), содержащего перемен- ную с, в результате замены этой переменной переменными а и Ь соответственно. Во всякой такого рода формуле а = Ь -)- 1(а) =1( ) вместо а и Ь могут быть подставлены произвольные тер- мы; тем самым из данного вывода равенства а = Ь мы всегда сможем получить и некоторый вывод равенства 1(а) = 1(Ь). Другое замечание общего характера, относящееся к термам, заключается в том, что из формулы 1 = а, где 1 — произвольный терм, с помощью второй аксиомы равенства (1 ) может быть выведена фо м ла д формула а = а.
В самом деле, как уже ранее упоминай лось '), применив (1»), можно получить формулу а = Ь ». (а = с -)- Ъ = е), а отсюда подстановками получим ') Е.. 2)). так что формулу а = а можно будет получить с помощью формулы 1 = а двукратным применением схемы заключения. Поэтому, если в какой-нибудь формальной теории имеется аксиома вида 1 = а (или же 1 = ь с произвольной переменной ь) и аксиома равенства (1,), то аксиома равенства (У«) оказывается излишней. На этом мы закончим рассмотрение формального аспекта введения функциональных знаков.
Что же касается содержательного истолкования, то надо сказать, что с этой точки зрения функциональным знакам будут соответствовать математические функции. Эти функции отличаются от логических функций, т. е. от предикатов, тем, что значения их снова являются элементами индивидной области, в то время как значение любой логической функции всегда представляет собой одно из двух истинностных значений — «истина» или «ложь». 5 2. Решение проблемы разрешимости; теоремы о полноте 1. Распознавание выводимости таких предваренных формул исчисления предикатов, у которых все кванторы всеобщности предшествуют всем кванторам существования; разрешимость в конечном.
После этих дополнений к нашему формализму мы вновь вернемся к основному ходу наших мыслей. Мы поставили перед собой задачу доказать, что каждая формула одноместного исчисления предикатов, тождественная в конечном, выводима средствами исчисления предикатов. Кроме того, еще должна быть решена проблема разрешимости для одноместного исчисления предикатов. Имея в виду эту цель, мы сведем рассмотрение формул одноместного исчисления предикатов к рассмотрению формул специального вида 1гу'чг ... »Уи ЗхЯ (х, у, з, ..., и), где Я (х, у, г,..., и) обозначает выражение без кванторов, а Зх представляет собой единственный квантор существования.
Сначала мы обсудим вопрос о выводимости формул этого вида. Эта дискуссия будет интересна и сама по себе, тем более что она будет отгюситься пе только к одноместному исчислению предикатов, но и ко всему исчислению предикатов в целом. Прежде всего мы докажем следующузо теорему: Если формула вида ЗхЯ (х), не содержащая, кроме квантора Зх, никаких других кванторов и такая, что в ней встречается не более 1 свободных индивидных переменных, является Ч-тождественной, то она являетея также и выводимой. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ игл ч РЕШЕНИЕ ПРОБЛЕМЫ РАЗРЕШИМОСТИ Рассмотрим сначала случай, когда Я (х) не содержит пи одной свободной индивидной переменной. В этом случае наша теорема утверждает, что если формула Зх Я(х) 1-тождественна, то она выводима. Зто (1ействительно так.
В самом деле, если рассматриваемая формула 1-тождественна, то формула Я (1) должна получаться подстановкой из некоторой тождественной формулы исчисления высказываний. Если цифру 1 всюду, где она встречается в атой подстановке в качестве аргумента формульной переменной, мы заменим переменной а, то у нас получится подстановка, дающая формулу Я (а), Таким образом, формула Я (а) тоже получается подстановкой из некоторой тояйдественной формулы и, значит, она выводима. Но формула ЗхЯ (х) моя1ет быть получена из нее применением схемы (р).
Теперь допустим, что в Я (х) имеются свободные индивидные перевекные; пусть а, Ь,..., г — полный список этих переменных и пусть число их равно п. По предположению, и ~( 1, в так как формула Лх Я (х) 1-тождественна, то она и и-тоскдественна. Интерпретация формулы Зх Я (х) на индивидной области, состоящей из цифр 1,..., и, дает дизъюнкцню Я(1) ~/ Я(2) ~/ ... ~/ Я(п), и если вместо переменных а, Ь, ..., г мы подставим соответственно цифры 1,2, ...,п (вследствие чего Я (х) перейдет в некоторое выражение Яе (х)), то в результате получится Я*(1) ~/ Яе(2) ~/ ...
~/ Яе(п). Значит, эта формула (по определению п-тождественной формулы) должна получаться подстановкой из тождественной формулы исчисления высказываний. Если мы теперь внесем изменения в подстановку, заменив цифру 1 всюду, где она встречается в качестве аргумента в подставляемой элементарной формуле, переменной а, цифру 2 — переменной Ъ,..., цифру п — переменной г, то в результате этой модификации подстановки получится формула Я (о) Ч Я (Ь) Ч " Ч Я (г). Таким образом, эта формула получается подстановкой из некоторой тождественной формулы исчисления высказываний и, следовательно, является выводимой. Но от нее с помощью выводимой формулы А(а) ~/ А(Ь) ~/ ...
~/ А(г) -и ЛхА(х) можно будет перейти к формуле ЗхЯ (х). Доказанная теорема немедленно может быть обобщена следующим образом: Если формула вида чучз ... ТиЗхЯ (х), не содержащая никаких кванторов, кроме укаэанных, 1-тождественна (1 ) 1) и если сумма числа кванторов всеобщности в этой фор.нуле и числа встречающихся в ней свободных индивидных переменных (каждое иэ этих чисел может быть равно нулю) не превосходит 1, то эта формула выводима. Действительно, пусть Ь, с, ..., в — свободные переменные, не встречающиеся в этой формуле, и пусть число их равно числу свяаанных переменных у, з, ..., и. Тогда из рассматриваемой 1-тождественной формулы по правилу (е') выводима формула ЛхЯ(х, Ь, с, ...,в).
Значит, эта формула тоже 1-тождественна, так как совокупность 1-тождественных формул, как было показано в гл. 1У, дедуктивно замкнута. Кроме того, число свободных индивидных переменных в атой формуле не превосходит 1. Отсюда, по только что доказанной теореме, получается, что формула ЗхЯ(х, Ь, с, ...,в) выводима средствами исчисления предикатов беа использования формулы 'Ру ... ЧиЗхЯ(х, у, ..., и).
Но от формулы ЛхЯ(х, Ь, с, ...,в) мы по правилу (з) снова придем к формуле 'з'у ... РиЗхЯ (х, у, ..., и). Тем самым оказывается, что эта формула тоже выводима средствами исчисления предикатов. Впрочем, предположение о том, что в рассматриваемой формуле встречается в точности один квантор существования, для доказанной теоремы является несущественным; теорема остается СЗ Л. Гильберт, П. Бернайс РЕШЕНИЕ ПРОБЛЕМЫ РАЗРЕШИМОСТИ 243 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ !ГЛ. Ч 242 в силе и в том случае, если квапторов существования нет вообще или если вместо одного квантора существования имеется несколько идущие подряд кванторов существования, т, е.
в случае пред- варенной формулы вида 'УХ1 ... 'УХ1ДУ1 ... ЗуАЯ (Х1 ° ° ° Хс у1 ° ° ° ул) где все кванторы всеобщности предшествуют всем кванторам существования. Доказательство опять можно свести к случаю, когда квакторы всеобщности отсутствуют вообще. Требующееся здесь рассуждение может быть проведено совершенно тем же самым способом, что и в случае формулы с одним квантором существования. Для примера рассмотрим случай, когда формула имеет вид зхлуЯ (х, у), причем Я (х, у) не содержит кванторов, а а и Ь являются единственными встречающимися в ней свободными индивидными переменными. Для всякой такой формулы наша теорема утверждает, что в случае 2-тождественности она является выводимой. По аналогии с ранее проведенным доказательством это может быть показано следующим образом.
Из предположения о том, что эта формула является 2-тождественной, мы получаем, что формула Я (а, а) ~/ Я (а, Ь) Ч' Я (Ь, а)111/ Я (Ь, Ь) может быть получена подстановкой из некоторой тождественной формулы, а потому является выводимой. Но от этой формулы мы можем перейти к формуле ЗХЗУЯ (х, у), воспользовавшись выводимостью формулы А (а, а) ~/ А (а, Ь) Ч1 А (Ь, а) !/ А (Ь, Ь) -+.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
