Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 44
Текст из файла (страница 44)
При рассуждении с помощью символьного р ешения на месте тех Ч-переменных формулы 6, которым не предшествуют никакие =)-переменные, тоже появляются индивидные символы, потому символьного решения в этом случае должна при- меняться к таким формулам, которые получаются приведением формулы ) 6 к предваренному виду. А при этом преобразовании упомянутые 1г-переменные переходят в )-переменные без предше- ствующих им Ч-переменных. П и обратном переходе от дизъюнкции, истинной в логике высказываний, к формуле К в список терм ри ов 1л, ..., 1р мов, которые начинаются вновь вводимыми функ- кроме тех терм ены в качестве термов циональными знаками, должны быть включены в кратности 0 еще и вновь вводимые индивидные символы. С учетом всех этих предварительных замечаний наш результат может быть сформулирован в виде следуюших двух предложений: а) Любая данная предваренная формулам:выводима'средствами исчисления предикатпв тогда и только тог а, да когда может быть указана некоторая дизъюнкция, истинная в логшсе в логике высказываний 902 а-символ и лОГическиЙ ФОРмАлизм !гл, ги ТЕОРЕМА ЗРЕРАИА 4 31 и такая, что каждый ее член получается из формульс 6 отбрасыванием кванторов и зименой связанных переменных некоторыми термами так, чпго при этом вьгполняются следующие структурные условия: 1.
Термы, заменяющие связанные переменные, образуются из индивид ых переменных, из символов, входящих в формулу 6, а также из некоторых вновь вводимых, взаимно однозначно сопоставленных Ч-переменным формулы ьг'. индиэидных символов и функциональных знаков; это сопоставление обладает тем свойством, чпю любой Ч-переменной, которой не предшествуют никакие Ч-переменные, соответствует некотор я индивидная переменная, а любой Ч-переменной, которой предшествуют 1 Ч-переменных, соответствует некоторый функциональный знак с 1 аргументами. 2. Любая Ч-переменная, которой не предшествует ни одна З-переменная, в каждом члене этой дизъюнкции заменяется соответствуюи!им ей индивидным символом', любая Ч-переменная, которой предшесгпвует одна или большее число З-переменньгх, заменяется сопоставленным ей функциональным знаком, у которого в качестве аргументов фигурируют термы, стоящие на месте предшествую- и(их Э-переменных, причем они располагаются в порядке следования этих м-переменных. (Термы, спюящие на месте З-переменных, могут быть произвольны.ч образом построены из входящих в формулу 6 свободных индивидных переменных, индивидных символов и функциональных знаков, а также вновь вводимых символов.) б) По любой выводимой средспюами исчисления предикатов предваренной формуле 6 можно указать такую дизъюнкцию, что каждый член ее получается из Ж отбрасыванием кванторов, заменой Ч-переменных некоторыми свободными индивидными переменными и заменой Э-переменных некоторыми термами, построенными из некоторых свободных индивидньгх переменных и входящих в формулу й индивидных символов и функциональных знаков, причем эта дизъюнкция получается подстановкой из некоторой тождественно истинной формулы исчисления высказываний, а сама формула ьт может быть получена из нее.путем применения правил (р) и (ч) ') и вычеркивания повторяющихся дизъюнктивных членов.
Эти два утверждения, взятые совместно, и составляют содержание теоремы, которая была провозглашена (правда, в несколько иной формулировке) Ж. Эрбраном в качестве основной теоремы теоретической логики и которую мы поэтому называем теоремой Эрбрана в). 1) См, с 173, ') Она была доказана в его диссертации: НегЬгапб ).
кесьегсьеь ьнг 1з Гиеог!е бе 1а бьщапь1га1!оп. — ТЬеье бе Г!)п!ч. бе Рапь, !930. Опубликована в Тгачацх бе 1а Бос. без Бс!. е1 1л1, Ве )гагьач!е, !930. См. также вторую рабату Эрбрана: НегЬгапб 3. Биг !е ргоыеще !опбагпеи1а! бе !а !ак!Чць ща1ЬещанЧце. — С. г, Бос. Бс!. Чагьоч!е, !931, 24, С1. Н!. Доказательство Суть теоремы Эрбрана мы поясним сначала на одном простом примере. Возьмем две формулы ЧхЧ)7 (х ( гр (гр (у))) -ь Чхщу (х ( гр (у)) и Чту(х(гр(у))-эЧхЛу(х» гр(гр(у))).
Выводимость первой из них легко устанавливается непосредственно. Относительно второй ясно, что при арифметическом ее истолковании она истинна не всегда. Чтобы применить к этим формулам предложения а) и б), мы сначала должны будем привести их к предваренному виду. Это может быть сделано различными способами. Например, первая формула переводима в формулу ((1)) ЧхЗуЧг ( 1(у ( гр (ф (г))) ~/ х( гр (у)), а вторая — в формулу ((2)) ЧхВуЧЕ ( 1(у ( гр (г)) ~/ х (гр (гр (у))). Согласно предложению а), необходимое и достаточное условие выводимости формулы ((1)) закл.очается в возможности указать Эрбрана трудно лля чтения и требует некоторых исправлений, как было недавно показана Б. Дребеном [см.
ГГ ге Ь ел В, А п 4 ге ья ь А,, А а п б е г а а Бк га!ье Ьепппаь |п НегЬгапб. — Ви1!. Агпег. Мань Бас., !963, 69, р. 699 — 706. Более простое доказательство этой теоремы было дано уже Г. Генценом в его работе: Сг е п 1 ь е п Сг, 1)п1егьцсьцпкеи 6Ьег баь !ой!асье Бсы!ейеп, — Ма1Ь. с., !934, 39, № 2, 3; см., в частности, !ту.
АЬзсЬпп1, 4 2 (русский перевод этой работы: Г е н ц е н Г. Исследование логических выводов. — В кн: Математическая теория логического вывода. М„Физматгиз, !967, с, 9 — 74,— Прим. перев.) Это доказательство получается с помощью одной еще более обшей теоремы, применимой также к неиоторым подфармализмам исчисления предикатав.
Новые доказательства этой более общей теоремы предложены Куртом Шюттс: 5сЬ 011е К. Бсыпйме!ьепйаркй!е бег Ргйб!Ьа1еп!аг!Ь.— Ма1Ь. Аип., !950, 122, 5. 47 — 65, Хаскеллам Б. Карри: Сц гг у Н. В. А Тьеагу о! Гоггпа! )Зебцс!Ы!!)у. — На!ге 0аще Мапйегпа1!сз! 1.ес1цгеь, № 6, 1950 и Стефеном К. Клини: К! ее не 51ерьеп С. !и1гобпсиоп 1о Ме1аща)Ьегпа1!сз.
— Агиь1егбапт, 1952, 4 78 (имеется русский перевод этой книги: К л и н и С~ефен К. Введение в метаматематику. — Мл ИЛ, !957. — Прим, перев,). Как мы видели, теорема Эрбрана получается из теоремы аб элементарном выводе (см. с. 37).
Последняя была получена нами из первой в-теоремы и является, кроме того, частным случаем одной теоремы аб исчислении предикатов, доказанной Эриком Стениусам (см. сноску ! на с. 37). Доказательства Шютге и Стениуса относятся иепосрелственно к логическому исчислению рассмотренного нами типа, в то время как доказательства Генцена, Карри и Клини относятся к некоторому исчислению секвенций. Наконец, теорему Эрбрана можно также получить с помощью метода семанти ческих таблиц Э. В. Бета. Об этом см. его труд: В е1Ь Е. 97. ТЬе раапба1!апь а! Магпещапсь, — Ашь1егбащ, 1959, ьес.
90 — 92. Следует также упомянуть теоретико-множественные доказательства теорем Генцена и Эрбрана, даннйе Стигом Кангером: К апйег Бий. Ргоча. Ы1пу 1п 1ой!с, !)ррьа!а, 1957, Р. Сикорским: 81Ь а гай ! й. Оп НегЬгаиб з Тьеогещ.— Синай. Ма)Ь., 1958, 6, р. 55 — 58 и Е. Расевой и Р. Сикорским: к аз! аьча Н., 511гагь1;! Н. Оп 1Ье Пеп1хеп ТЬеогещ.— гцпбаш.
ща)Ь.. 1960, 48, р. 57 — 69. з 3! ФСИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ ТЕОРЕМА ЭРЕРАИА [гл. <ц некоторую дизъюнкцию, состоящую из членов вида )(1(ф(ф(ф(1)))) Ч а(ф(1) с некоторыми термами 1, построенными из переменных и из символов <р и ф и получающуюся подстановкой из некоторой тождественно истинной формулы исчисления высказываний. Такой дизъюнкцией является, например, формула (1 (а (ф (<р (<р (а)))) </ а( ф (а)) ~/()(ф(ф(а)) ф(ф(<р(ф(<р(а)))))) </а(ф(ф(ф(а)))). Следовательно, формула ((1)) выводима.
Если бы выводимой была и формула ((2)), то можно было бы соответственно найти некоторую дизъюнкцию, состоящую из членов вида 1(1(<р(<р(Е))) </ а(ф(<р(1)), которая получалась бы подстановкой из некоторой тождественно истинной формулы. Но для этого потребовалось бы, чтобы неко- торая из фигурирующих под знаком отрицания формул 1(ф(ф(1)) по внешнему виду совпала с какой-либо формулой а(ф(ф(<)), что невозможно, так как терм <р(<) не может совпадать с термо <р().
Тем самым мы убеждаемся, что формула ((2)) невыводима. м Теперь воспользуемся предложением б). Для формулы ((11), выводимость которой нами установлена, оно утверждает, что най-' дется некоторая дизъюнкция, состоящая из членов вида 1(1 =ф(ф(а))) Чь =<р(1) ны с переменными а и Ь и с некоторыми, составленными из перем х и функционального символа ф термами 1, причем эта дизь- ен- юнкция получается подстановкой из некоторой тождественно истин- ной формулы исчисления высказываний, а формулу ((1)) можно получить из нее с помощью правил (р) и (Р) и вычеркивания повторякчцихся членов дизьюнкции. В качестве дизъюнкции, обладающей этим свойством, можно, например, взять формулу ( 1(а (<р (<р (Ь)) 1/ а «р (а)) ~/ ( 1(<р (Ь) < ф (<р (с))) </ а «р (<р (Ь))).
Действительно, эта формула, с одной стороны, получается под- становкой из тождественно истинной формулы ()А 1/ В) 1/()С'1/ А), а с другой стороны, от нее можно прийти к формуле ((!)) сле- дую<цим образом: сначала применением правила (Р) к переменной а и последующим применением правила (1<) мы получаем формулу П (и ( ф (ф (Ь) )) <! а «р (а)) ~/ Лу<< г ( 1 (у ( <р (ф (г))) </ а «р (у)), з затем применением правила (ч) к переменной Ь и применением правила ((А) получим формулу Буча()(улаф(ф(г)))</а<ф(у))</чуыг( ~(уф(ф(г))йа =ф(у)). А теперь вычеркнем один из двух повторяющихся членов этой дизъюнкции.
Применив еще раз правило (Р), мы получим требующуюся формулу 'Входу<<<В (1(у (<р (ф (г))) ~/ х(ф (у)). Если у какой-либо предваренной формулы <г.' выражение, стоящее за кванторной приставкой, имеет вид дизъюнкции 'е(, </ ...й(<, члены которой Л„ ..., Л< представляют собой выражения без логических знаков или отрицания таких выражений, то с помощью предложения а) можно решить вопрос о выводимости К. Действительно, согласно этому предложению, для выводимости (Я необходимо и достаточно, чтобы можно было указать получающуюся подстановкой из некоторой тождественно истинной формулы исчисления высказываний дизъюнкцию 6, </ ...6п каждый член которой получается из формулы (Р вычеркиванием кванторов н заменой связанных переменных некоторыми термами так, что при атом соблюдаются некоторые структурные условия. При этом каждая из формул 6, (1=1, ..., 1) имеет вид некоторой дизъюнкции Й(<) ~/ ...
~/ Л(<), каждый член которой является либо элементарной формулой, либо отрицанием элементарной формулы. Для того чтобы формула 6, </... ~/ 6< получалась подстановкой из какой- либо тождественно истинной формулы исчисления выскззываний, необходимо и достаточно, чтобы среди 1 < членов этой дизъюнкции имелось по меньшей мере два таких члена, один из которых представлял бы собой отрицание другого.
Таким образом, данное в предложении а) необходимое и достаточное условие выводимости формулы Се сводится к тому, что среди выражений 'Л„ ..., Л< должны найтись два таких выражения е(„ и Л, для которых — после сопоставления «<-переменным формулы (г новых переменных и функциональных знаков †мож указать дее такие замены для 3-переменных формулы <Р, что— с учетом замен для Р-переменных формулы б', которые получаются из этих замен в соответствии с указанными структурными условиямк, †'формула, в которую в результате первой замены переходит формула Яр, совпадает с отрицанием той формулы, в которую в результате второй замены переходит формула <Лч.
Как легко видеть, могут быть явным образом сформулированы условия для возможности построения двух таких замен; так как 207 ТЕОРЕМА ЭРБРАИА 4 11 е-СИМНОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ !ГЛ П1 при этом количество входящих в рассмотрение пар выражений Яе, Я конечно, то это в конце концов дает нам решение вопроса о выводимости зх 1). Причиной того, что не может быть решен аналогичным образом вопрос о выводимостн произвольной заданной предваренной формулы, является то обстоятельство, что совершенно невозможно указать какую-либо оценку для числа дизъюиктивиых членов 9„..., 61. В рассмотренном частном случае эту дизъюнкцию можно бьзло считать двучленной с самого начала.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
