Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 36

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 36)

Если вместо формульной переменной Л в эту формулу подставить логическую функцию Ф с двумя аргументами и обозначить соответствующее ей множество пар посредством Ч~, то получающееся при этом выражение ЗуФ (а, у) наображает такую логическую функцию от переменной а, которая принимает значение «истина» на тех и только тех элементах, которые встречаются в качестве первого члена по крайней мере у одной пары иэ «». Теперь мы уже можем ввести для формул понятия общезначимосл»и и выполнил«ости, которые мы определим так, как это делалось !гл.

Рз 168 исчисчииие пРвдикАТОВ ВОПРОСЫ СИСТВМАТИКИ в гл. 1 '), но в несколько более общем виде, включая в рассмотрение и формулы со свободными индизидиыми переменными. Формула исчисления предикатов называется общезначимой, если при любой подстановке логических функций вместо формульных переменных и элементов иидивидной области вместо свободных иидивидных переменных (если эти последние в формуле имеются) она принимает значение «истина»; формула называется выполнимой, если она принимает значение «истина» при подходящем выборе подстановок. Общезначимость и выполнимость двойственны по отношению друг к другу; именно формула общезначима тогда и только тогда, когда ее отрицание невыполнимо; отсюда в предположении, что для предикатов верен «)ег11аш поа йа1аг», получается, что формула выполнима тогда и только тогда, когда ее отрицание не общезначимо.

Далее, можно доказать, что всякая формула, выводимая в исчислении предикатов, общезначима. Именно, нетрудно убедиться, что исходные формулы исчисления предикатов общезначимы и что в результате применения правила подстановки и схем исчисления предикатов из общезиачимых формул всегда получаются снова общезначимые. А теперь воаиикает вопрос о том, верно ли обращение этой теоремы, т. е. является ли выводимой всякая общезиачимая формула исчисления предикатов. Тем самым мы возвращаемся к прежней теме, которая и привела нас к рассмотрению теоретико-множественной логики предикатов.

Вопрос этот получил свое решение благодаря следующей доказанной К. Геделем теореме о полноте з). Назовем формулу о и р о в е р ж н и о й, если выводимо ее отрицание; тогда имеет место следующая альтернатива; всякая формула исчисления предикатов либо опровержима, либо выполнима, и притом в индивидной области целых чисел '). ') Сы. с. 31. з) Доказательство этой теоремы составляет главное содержание работы: С б й е 1 К. П!е 'з'о))з«аай!3Ь«!! йзг Ах!оше й«з )об!««Ьеа Еаай!!оаеайз)- Ьй)з.

— Мова!«Ь. Мз!Ь. РЬуз., 1930, 37, Гй 2. з) Та часть этого результата Геделя, которая отаосатса з выаолааыости а области целых чисел, была ужз ранее получек« Лзезагейыоы, который з своей работе: Ь б и е и Ь е 1 ш Е. СЬег М3311сЬЬе!!еа па )1«)з!!«Ь«)ЬЬ1.— Мз!Ь. Ааа., 1915, 76 — з числе прочих зазчательаых теорем доказал, что ароазвоаьаая формула асчаслеаая ар«лак«таз, выаоааамза з какой-лабо вообще области, всегда будет выполнима а а аадаеадаой области целых чисел. Доказательство Лбвеагейыз было затеи упрощено Скол«азы, который аоздизе кока«за также, что здесь можно обойтись бзз праиеаеаая араацааз выбора, существенно асаользозазшегоса з первых доказательствах.

По данному вопросу за«ются следующие работы Сколемз; 8 Ь о 1 е ш Т. Еой!««Ь-Ьошб)- аз«огы«Ье Са!«гза«Ьаадза йбег й!е Ег!зПЬ«гйе!! ойег Веъ«1«Ьзгйе!«шз!ЬзшзИз«Ь«г 8«!зз п«Ь«! ешеаз ТЬ«огзш йЬег й!СЬ«з Мзайза.— у!й;8з)«Ь. 8йг. Кгы- Отсюда в качестве следствия получается, что каждая общезначимая формула выводима. Действительно, если Я вЂ” общезначимая формула, то ее отрицание )Я во всяком случае является невыполнимым; поэтому на основании упомянутой альтернативы формула -)Я опровержима и, следовательно, ) )Я выводима; а нз ~ ~Я может быть выведена и сама формула г1.

Конечно, геделевская теорема о полноте в рассмотренном нами виде не может быть перенесена в финитную теорию доказательств, поскольку она существенным образол! опирается пусть не на самые сильные нефинитиые вспомогательные средства, по все же, например, на «1ег1«иш поп йа!агз в применении к целым числам. Однако из геделевского доказательства можно извлечь некоторую финитную теорему о полноте, которая выражает тот факт, что для любой неопровержимой формулы в рамках формаливованвой (с включением принципа «!ег!!аш аоа йа!цгз) арифметики всегда имеется некоторая формальная модель, а также (на что здесь мы пока только намекнем) некий тип аппроксимативных моделей, состоящих из сколь угодно далеко продолжаемых конечных последовательностей систем предикатов, которые определены в конечных ипдизидиых областях и каждая из которых представляет собой продолжение предыдущей.

И обратно, согласно одной теореме, доказанной Эрбраном !), из существования такой аппроксимативной модели для данной формулы будет вытекать ее неопровержимость. Далее, тот факт, что формула, выполнимая в рамках формализованной арифметики является неопровержимой, следует из непротиворечивости арифметики, которая еще должна быть доказана. Весь этот пока лишь эскиано набросанный комплекс результатов мы подробно изложим в дальнейшей части нашего сочинения.

Здесь же мы только ограничимся констатацией того факта, что аналогия между исчислением высказываний и исчислением предикатов, которую мы предчувствовали в вопросе о полноте, окааалась действительно существующей, хотя и с известными ограни' чениями, вызванными финитной точкой зрения.

Напротив, попытка проследить другую, лежащую в сходном направлении аналогию, а именно аналогию с проблемой раарешимости, к цели не привела. Зта проблема, о которой мы уже говорили в гл. 1 '), заключается в том, чтобы попытаться распростра- !!за!а 1, Ыз!.-)Ча!. К1., 1920, уй 4; 8 Ь о1е ш Т. Еш13« Взшзгйаазза гаг зх1оша!!зсЬ«а Вейгйайаай йзг Ыеабза)«ЬР«.— Мз!Ь. Коабг. !. Не)з!аб!огз, 1922; 3 Ь о 1 з ш Т. 1)Ъег е!а!3е Сгзай!збеа!гад«а йег Мз«Ьешз!!Ь.— 8Ьг. аогзйе Ч!й;АЬзй. Оз)о, 1 Ыз«.-)Ч«!.

К1., 1929, А) 4. ') 06 этой теореме адет речь в пятой главе его докторской диссертации: Н з г Ь г з а й Х. ))е«Ь«г«Ь«з заг 1а !Ьзояе йе 1« йешоаз!га!!оа.— Рзг!з, !930. Во втором томе ыы подробно астааозаыса аз зтоц результате. з) Сы. с. 31. 171 ВОпРОсы снсткмьтики игл, гч исчислвнив пРндикАтОВ 470 нить на исчисление предикатов разрешающую процедуру исчисления высказываний, которая для любой формулы этого последнего поаволяла выяснить вопрос о том, является зта формула тождественно истинной или же при некоторых значениях переменных она оказывается лен«ной.

При рассмотрении проблемы разрешимости мы должны отличать друг от друга различные постановки вопроса. В теоретико- множественной логике предикатов зта проблема может быть представлена в виде двух по существу равносильных, а по форме двойственных друг другу проблем: проблемы распознавания общеаначпмости и проблемы распознавания выполнимости формул. Вследствие уже упоминавшихся ранее соотношений, существующих между общезначимостью и выполнимостью, выяснение общезначимости какой-либо форыулы Я равносильно выяснению выполнимости формулы 7Я. Поэтому, если для некоторой совокупности формул В имеется метод для распознавания общезначимости этих формул, то он одновременно представляет собой и метод для распознавания выполнимости формул той совокупности, которую образуют отрицания формул из В, и наоборот.

В части нахождения и описания разрешающих процедур более наглядные результаты получаются при рассмотрении выполнимости формул. С точки арения теории доказательств место проблемы распознавания общезпачимости формул занимает проблема распознавания их выводимоети. Как общезначимости формул соответствует их вызодимость, так выполнимости формул соответствует их неопровержимость. Исследование вопроса о неопровержимости формул теснейшим образом связано с проблемой непротиворечивости систем аксиом. Именно, имеет место следующая Т е о р е и а.

Луста задана неквторан система аксиом, которые с помощью наших логических символов, связанных индивидных переменны и вполне определенных предикатных и индивидных символов представлены в виде формул Ям..., Я1 без свободных переменных; допустим, что основные предикаты, представленные предикатными символами, охарактеризованы только посредством этих аксиом. Тогда непротиворечивость рассматриваемой системы аксиом (постольку, поскольку раеематриваютел лишь обычные способы умова лючений, допускающие формализацию в р мках исчисления предикатов) совпадает е неопровержимостью той формулы, которая получается из Я,д«...

д«ЯВ если вместо каждого из предикатных символов подставить некоторую новую формульную переменную с тем же салым числом аргументов, а на место индивидных символов подставить различные свободные индивидные переменные. В агой теореме, которую мы получим ниже в качестве следствия из другого более общего утверисдения '), находит выражение тот факт, что методическая перестройка, которую мы осуществили в гл. 1, представляет собой не что иное, как переход от проблемы выполнимости к проблеме неопровержимости. В то же самое время в связи с материалом, рассмотренным в гл.

1, мы должны обратить внимание на то, что предположение о том, что неявное описание всех фигурирующих в системе аксиом основных предикатов является полным, в наиболее употребительных системах аксиом выполняется пе всегда, поскольку в ннх чаще всего фигурирует равенство в качестве содержательно-логически определенного отношения. Учитывая эти обстоятельства, мы имеем далее две возможности. О одной стороны, если система аксиом имеет рассматриваемый тип, то существует возможность ликвидировать выделенное положение равенства, охарактеризовав его добавлением специальных аксиому с другой стороны, понимание равенства как логически определенного отношения мы мон«ем реалиаовать в виде специального расширения логики предикатов (зависящего от того, на какой точке зрения мы стоим — содержательной или формальной) и в соответствии с этим обсуждать проблему разрешимости для этой расширенной путем присоединения равенства логики предикатов.

Оба метода в дальнейшем будут нами изложены. Наряду с распознаванием неопровержимости формул в теории доказательств важную роль играет также исследование их выполнимости. При этом принимаются в расчет три типа выполнимости: выполнимость в конечной индивидной области (коротко — «в конечном»), выполнимость в какой-либо модели финитной арифметики и выполнимость в рамках какого-либо охватывающего исчисление предикатов непротиворечивого формализма в смысле возможности указания для формульных переменных рассматриваемой формулы таких подстаяовок, после выполнения которых формула оказывается выводимой внутри этого формализма. При каждом из этих трех подходов выполнимость какой-либо формулы влечет за сооой ее неопровержимость.

Действительно, формула Я, выполнимая в конечном, не может быть опровержимой, потому что в противном случае формула 7 Я (как выводимая формула) была бы тождественной в конечно»С Далее, неопровержимость любой формулы, выполнимой при помощи какой-либо модели финитной арифметики хотя и не усматривается непосредственно — как можно было бы думать,— но все н«е вытекает из уже упоминавшейся ранее теоремы Эрбрана. А в случае выполнимости в рамках какого- либо формализма опровержимость формулы оказалась бы несовместимой с непротиворечивостью этого формализма. ') Ся. с.

200. исчисление пРедикАТОВ 172 1гл. 1У 1 11 изучение ФОРИАчизмА исчисления пРедиклтов 173 Мы подробно поговорили о подходе к проблеме разрешимости и о ее аначении. Теперь, что касается полученных результатов, то к настоящему времени удалось найти распознающие процедуры только для одноместного исчисления предикатов, а также для нескольких других частных случаев, которые в дальнейшем еще будут указаны более подробно 1). Этн случаи изучались главным обрааом с позиций распознавания общеаначимости или соответственно выполнимости формул.

Характеристики

Список файлов книги