2. Приведение формул к предваренному виду; примеры; описание разрешимых случаев проблемы разрешимости с помощью предваренной нормальной формы.

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

Всякую формулу, имеющую такой вид, мы будем называть предваренной формулой.

Процедуру перевода любой формулы в предваренную мы изложим на примере формулы

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

Согласно правилу

мы можем перевести в

далее по правилу

мы можем преобразовать в

следовательно, по правилу

может быть преобразовано в

так что в целом мы получим

Теперь применим к члену

этой дизъюнкции правило переименования, переименовав х и у виши; так мы получим формулу

а ее по правилу можно перевести в предваренную формулу

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

и

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

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

мы во втором члене дизъюнкции переименовываем только переменную при этом получается

Применение правила сначала приведет нас к формуле

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

которая является предваренной и у которой кванторная приставка состоит только из трех кванторов.

Метод приведения произвольной формулы к предваренному виду мы хотели бы применить еще и к упоминавшейся ранее формуле которая получается в результате конъюнктивного связывания следующих трех формул:

Если здесь в третьем члене конъюнкции предварительно переименовать , то получится

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

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

Кроме того, выражение, стоящее после кванторов, можно, преобразовав второй член конъюнкции [по правилу ], перевести в конъюнктивную нормальную форму; таким образом, мы получим

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

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

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

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

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

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

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

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

1. Кванторы, входящие в приставку, суть либо только кванторы всеобщности, либо только кванторы существования; либо же все кванторы всеобщности предшествуют всем кванторам существования.

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

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

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

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

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

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

и

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

Теперь, что касается решения упомянутых трех случаев проблемы разрешимости, то первый из них может быть разрешен относительно легко; мы будем говорить о нем в гл. Для второго случая проблема разрешимости была, независимо друг от друга, решена Гёделем, Кальмаром и Шютте. Все они рассмотрели

соответствующий класс с разрешимой проблемой выполнимости и нашли для формул этого класса условие, необходимое для их неопровержимости. Для тех формул, которые удовлетворяют этому условию, Гёдель и Кальмар доказали, что они выполнимы при помощи некоторой модели в финитной арифметике; Шютте доказал, кроме того, их выполнимость в некоторой конечной индивидной области (с числом индивидов, оцениваемым при помощи рассматриваемой формулы). Разрешающую процедуру для третьего случая нашел Эрбран непосредственным применением своей уже упоминавшейся общей теоремы.