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