2. Экскурс в теоретике-множественную логику предикатов; предварительные замечания к вопросу о полноте; проблема разрешимости и ее уточнение с дедуктивной точки зрения.

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

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

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

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

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

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

значения «истина» или «ложь», здесь значения какой-либо переменной

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

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

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

рассматриваемой индивидной области, для которых эта функция принимает значение «истина»; аналогично, функции трех аргументов соответствует множество упорядоченных троек элементов и т. д.

Применяя истинностные функции логики высказываний, мы из заданных логических функций получим новые функции этого рода, которым снова будут сопоставлены некоторые множества.

Пусть, например, представляет собой логическую функцию одного аргумента. Тогда будет представлять такую функцию, которая значение «истина», соответственно «ложь», принимает на тех элементах индивидной области, на которых принимает значение «ложь», соответственно «истина». Множество, соответствующее функции является дополнением к множеству, соответствующему функции

Если и две логические функции, то представляет собой такую функцию, которая принимает значение «истина» на тех и только тех элементах, на которых обе функции принимают значение «истина». Соответствующее множество является пересечением множеств, соответствующих функциям е. множеством элементов, принадлежащих обоим этим множествам одновременно. Точно так же функции соответствует объединение множеств, соответствующих функциям и

Операции, соответствующие кванторам всеобщности и существования, понимаются как конъюнкция и дизъюнкция, распространенные на всю индивидную область. Поэтому для произвольной логической функции выражение

принимает значение «истина» или «ложь» в зависимости от того, совпадает или не совпадает множество, соответствующее функции со всей индивидной областью, а

принимает значение «ложь» или «истина» в зависимости от того, пусто или непусто множество, соответствующее

Если теперь в какой-либо формуле исчисления предикатов мы подставим вместо формульных переменных логические функции с тем же самым числом аргументов и при этом все индивидные переменные окажутся связанными, то в силу указанной интерпретации эта формула получит одно из значений «истина» или «ложь». Если же в этой формуле имеются свободные индивидные переменные, то при всякой подстановке логических функций вместо формульных переменных рассматриваемая формула будет принимать в качестве значения некоторую новую логическую функцию.

В соответствии со сказанным, формула без свободных переменных представляет собой некоторое высказывание о логических функциях, могущих быть подставленными вместо формульных переменных, или же о множествах, сопоставленных этим функциям; это высказывание является истинным или ложным в зависимости от того, какое значение — «истина» или «ложь» — доставляют рассматриваемой формуле подставляемые логические функции или соответствующие им множества. Рассмотрим, например, формулу

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

равнозначна высказыванию о том, что является подмножеством множества Аналогично, формула

выражает тот факт, что множества совпадают, а формула

говорит о том, что множества и имеют непустое пересечение. Пример другого рода представляет собой формула

Если вместо формульной переменной в эту формулу подставить логическую функцию с двумя аргументами и обозначить соответствующее ей множество пар посредством то получающееся при этом выражение

изображает такую логическую функцию от переменной а, которая принимает значение «истина» на тех и только тех элементах, которые встречаются в качестве первого члена по крайней мере у одной пары из

Теперь мы уже можем ввести для формул понятия общезначимости и выполнимости, которые мы определим так, как это делалось

в гл. I, но в несколько более общем виде, включая в рассмотрение и формулы со свободными индивидными переменными. Формула исчисления предикатов называется общезначимой, если при любой подстановке логических функций вместо формульных переменных и элементов индивидной области вместо свободных индивидных переменных (если эти последние в формуле имеются) она принимает значение «истина»; формула называется выполнимой, если она принимает значение «истина» при подходящем выборе подстановок.

Общезначимость и выполнимость двойственны по отношению друг к другу; именно формула общезначима тогда и только тогда, когда ее отрицание невыполнимо; отсюда в предположении, что для предикатов верен «tertium non datur», получается, что формула выполнима тогда и только тогда, когда ее отрицание не общезначимо.

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

А теперь возникает вопрос о том, верно ли обращение этой теоремы, т. е. является ли выводимой всякая общезначимая формула исчисления предикатов. Тем самым мы возвращаемся к прежней теме, которая и привела нас к рассмотрению теоретико-множественной логики предикатов. Вопрос этот получил свое решение благодаря следующей доказанной К. Гёделем теореме о полноте. Назовем формулу опровержимой, если выводимо ее отрицание; тогда имеет место следующая альтернатива: всякая формула исчисления предикатов лпбо опровержима, либо выполнима, и притом в индивидной области целых чисел.

Отсюда в качестве следствия получается, что каждая общезначимая формула выводима. Действительно, если общезначимая формула, то ее отрицание во всяком случае является невыполнимым; поэтому на основании упомянутой альтернативы формула опровержима и, следовательно, выводима; а из может быть выведена и сама формула

Конечно, гёделевская теорема о полноте в рассмотренном нами виде не может быть перенесена в финитную теорию доказательств, поскольку она существенным образом опирается пусть не на самые сильные нефинитные вспомогательные средства, но все же, например, на «tertium non datur» в применении к целым числам. Однако из гёделевского доказательства можно извлечь некоторую финитную теорему о полноте, которая выражает тот факт, что для любой неопровержимой формулы в рамках формализованной (с включением принципа «tertium non datur») арифметики всегда имеется некоторая формальная модель, а также (на что здесь мы пока только намекнем) некий тип аппроксимативных моделей, состоящих из сколь угодно далеко продолжаемых конечных последовательностей систем предикатов, которые определены в конечных индивидных областях и каждая из которых представляет собой продолжение предыдущей. И обратно, согласно одной теореме, доказанной Эрбраном, из существования такой аппроксимативной модели для данной формулы будет вытекать ее неопровержимость. Далее, тот факт, что формула, выполнимая в рамках формализованной арифметики является неопровержимой, следует из непротиворечивости арифметики, которая еще должна быть доказана.

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

Напротив, попытка проследить другую, лежащую в сходном направлении аналогию, а именно аналогию с проблемой разрешимости, к цели не привела. Эта проблема, о которой мы уже говорили в гл. I, заключается в том, чтобы попытаться

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

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

С точки зрения теории доказательств место проблемы распознавания общезначимости формул занимает проблема распознавания их выводимости. Как общезначимости формул соответствует их выводимость, так выполнимости формул соответствует их неопровержимость.

Исследование вопроса о неопровержимости формул теснейшим образом связано с проблемой непротиворечивости систем аксиом. Именно, имеет место следующая

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

если вместо каждого из предикатных символов подставить некоторую новую формульную переменную с тем же самым числом аргументов, а на место индивидных символов подставить различные свободные индивидные переменные.

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

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

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

Мы подробно поговорили о подходе к проблеме разрешимости и о ее значении. Теперь, что касается полученных результатов, то к хгастоящему времени удалось найти распознающие процедуры только для одноместного исчисления предикатов, а также для нескольких других частных случаев, которые в дальнейшем еще будут указаны более подробно Эти случаи изучались главным образом с позиций распознавания общезначимости или соответственно выполнимости формул. Разработанные здесь распознающие процедуры затем удавалось оформить — частью прямым способом, частью с помощью упомянутой теоремы Эрбрана — как методы распознавания выводимости формул или соответственно их опровержимости. Эти решения частных случаев проблемы разрешимости носят, однако, весьма специальный характер; предлагаемые в них методы распознавания существенным образом связаны с особым характером рассматриваемых случаев.