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

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

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

где кванторов не содержит.

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

1. Элементарные формулы (формульные переменные с аргументом или без него).

2. Формулы вида

3. Формулы вида

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

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

Рассмотрим теперь какой-нибудь из членов полученной таким образом конъюнктивной нормальной формы. Он имеет вид

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

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

а затем переименованием связанных переменных и применением правила в формулу

и, значит, в формулу вида

где нет никаких кванторов, кроме указанных. Тем самым требуемое преобразование выполнено.

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

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

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

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

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

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

1. Вполне определенных истинностных значений («истина» или «ложь»), приписываемых формульным переменным без аргументов.

2. Вполне определенных логических функций от одного аргумента

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

3. Собственных имен индивидов из которые подставляются вместо свободных индивидных переменных.

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

совпадает с последовательностью значений

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

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

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

1. Вместо индивидной области мы возьмем -элементную область

2. Вместо функций

возьмем функции

3. Вместо собственного имени для индивида из некоторый знак для целого класса индивидов.

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

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

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

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

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

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

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

Обозначим эту формулу символом Пусть означает формулу, которая получится из если

а

пусть, кроме того, означает формулу, которая получится из если

Наше предположение, что формула является 2-тождественной, а тем самым и 1-тождественной, означает, что формулы

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

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

Как легко убедиться, обе формулы

выводимы. Первая из них в сочетании с дает

из второй в сочетании с мы получаем

Используя выводимые формулы

и

мы из формулы

по правилу силлогизма получим формулы

и

Далее, из формулы

мы с помощью выводимой формулы

получим формулу

из нее, выполнив соответствующие преобразования, получим

а отсюда двукратным применением схемы и путем элементарных преобразований получим

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

и

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

В этом выводе идея предыдущего содержательного доказательства находит свое отражение в применении формулы

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

При вместо этой формулы будет фигурировать формула

Здесь вместо двух переменных нас будут четыре переменные Аналогично, в общем случае приходится ввести свободных индивидных переменных.

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

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