И.А. Пушкарев логика

делать, если бинарное отношение S подразумевается симметричным?

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

QED

Замечания. (1) Напомним, что свойство образца быть тавтологией алгоритмически разрешимо, поэтому теорема 13.1 даёт алгоритм проверки общезначимости (и, следовательно – доказуемости) бескванторных формул.

(2) При всей тривиальности теоремы 13.1, из неё вытекает важный факт:

если в теории выполнима элиминация кванторов, то она разрешима.

(3) Проверка общезначимости формул класса П1 тривиально сводится к теореме 13.1. Действительно, общезначимость формулы

122

Ax1 Ax2 ...Axn p(x1, x2 , ..., xn ) равносильна общезначимости бескванторной

формулы с параметрами p(x1, x2 , ..., xn ).

«представительный набор термов», применявшийся в элиминации кванторов. В

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

делающего истинной формулу с параметрами p(x1, x2 , ..., xn ), и, следовательно,

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

Нетривиально, что такой набор обязательно (конеченаприори

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

Пример. Формула Ex(S (c, x)® S(x, d )), где с и d – константы,

общезначима: если S (c, d )= 0 , то в качестве х, обращающего в истину формулу

S (c, x)® S(x, d ) подойдёт d, иначе – подойдёт с («из лжи следует всё что угодно», «истина следует из чего угодно»). Заметим, что тем самым предъявлен тот самый конечный набор из двух подстановок, о существование которого и утверждается в теореме Эрбрана J.

Доказательство теоремы 13.2 достаточно провести(в соответствии со сделанным выше замечанием) только в одну сторону. Не умаляя общности,

считаем, то формула Ex1Ex2 ...Exn p(x1, x2 , ..., xn ) замкнута (в противном случае заменим свободные переменные «свежими» константами). Рассмотрим, вообще

123

говоря – бесконечный, набор формул вида Øp(t1 x1 , t2 x2 , ..., tn xn ), где t1, t2 , ..., tn

пробегает все возможные упорядоченные наборы замкнутых термов.

Если этот набор противоречив, то в выводе из него формулыО участвует

Øp1 Ù Øp2 Ù ... Ù Øpk ® O общезначима. Вспомнив, что формулы Øp и p ® O

доказуемо эквивалентны, можно заключить, что общезначимы и(доказуемо

модель, построенная в доказательстве теоремы Гёделя о полноте исчисления предикатов, и в этой модели, в которой носитель совпадает с множеством

меньшей мере – один, что S (x, y)=1. Выберем один такой y, и обозначим его

y = f (x) (между прочим, здесь мы в явном виде использовали аксиому выбора

d = d (e ), имея в виду, что для каждого e d может быть своя собственная? Это соображение даёт моральное право написать вместо AxEyS (x, y) более простую по виду формулу AxS(x, f (x)), которая выполнима одновременно с исходной.

Аналогично, для неатомарной формулы p(x, y), одновременно с формулой

124

AxEy p(x, y) будет выполнима формула Ax p(x, f (x) y), где f – некоторый новый функциональный символ (правда, следует проследить, чтобы подстановка была

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

Нет никакого препятствия тому, чтобы применить этот приём и к более

сложным . случаям Например, формула

Aa Ae Ed El Em Ab Eg p(a, b ,g ,d ,e, l, m) выполнима одновременно с формулой

существования, навешенным на соответствующую этой функции переменную g , находятся все три квантора всеобщности.

По существу, нами доказана следующая теорема.

Теорема 13.3. Для любой замкнутой формулы p сигнатуры s существует

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

справедлива следующая теорема.

AxAyEzEt (F (x, y, z)Ù G(x, y, t )Ù ((F (x, y, z)Ù G(x, y, t ))® p(x, y, z, t ))). Далее,

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

Теорема 13.5. (о сколемовской нормальной форме)

Для любой замкнутой формулыp сигнатуры s существует формула p¢

класса Σ2 над сигнатуройs ¢, полученной добавлением кs нескольких

«свежих» символов отношений, общезначимая одновременно с р.

QED

126

Замечание. Эта теорема означает, что для решения вопроса об общезначимости формул логики предикатов достаточно решить более простой

вопрос об общезначимости формул классаΣ . Позднее мы увидим, что

2

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

127

§14. Исчисление секвенций для языка предикатов 1. Первый формализм

Естественно попробовать построить исчисление секвенций для языка

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

описываются так же точно(пересечение правого и левого семейств формул

P, r(x)a Q

(Е–) ,

P, Eu r(u )a Q

P a r(x), Q (Е+) P a Eu r(u ), Q .

Действительно, вспоминая идеологию «поиска контрпримеров», можно заметить, что свойство подстановки быть контрпримером не меняется, если убрать квантор, «развязав» ещё одну переменную: в случае квантора существования такой контрпример тоже существует, а в случае квантора всеобщности любое распространение оценки на новую свободную переменную будет контрпримером. При этом правило (А+) есть вариант (ПБ1), а правило

(Е–) – вариант (ПБ2). Это напоминает о присущих правилам Бернайса ограничениях: переменная x не должна свободно входить в случае правила (А+)

формулу P , а в случае правила(Е–) – в формулу Q (иначе, напомним,

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

128

Вопрос. Почему с двумя другими правилами таких проблем не возникает?

Пример. Докажем секвенцию AxEyr (x, y)a AxEyEz(r(x, y )Ù r(y, z)), где r

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

следует не прямолинейно к этой секвенции, а к более сложной по виду, хотя и

дважды вытекает из того обстоятельства, что количество символов отношений,

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

2. Второй формализм

Правило (N+) позволяет перенести формулу из левой части секвенции в правую, навесив на неё отрицание. Применяя его систематически, можно добиться того, чтобы все рассматриваемые секвенции приобрели видÆ a P ,

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

Как и раньше, в двух правилах предполагается одно ограничение(не забыли – какое в каких? J). Аксиомами в этом случае окажутся(после аналогичного преобразования) множества формул, содержащие одновременно формулы р и Ø p для некоторой формулы р.

Далее заметим, что правило (N+) стало, откровенно говоря, просто смешным, и его можно безболезненно из списка правил удалить.

Кроме того, нам будет удобно заменить правила(А–) и (Е–) двумя другими правилами:

Эта замена не уменьшит множества теорем теории, так как применение правила (А–) можно заменить на применение двух правил(Е+) и (А*–)

(правило (Е–), соответственно, на (А+) и (Е*–)):

130

И наоборот, эта замена не увеличит множество теорем теории, так как применение новых правил требует, чтобы в секвенции содержалась бы формула вида EuØr(u) (соответственно, AuØr(u )), которая в новых условиях может появиться только вследствие применения правил(Е+) (соответственно (А+)),

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

Наконец, удалим для простоты(и без того сложного) рассмотрения из исчисления знак импликации и правила(I+) и (I–). По завершении рассмотрения их можно будет(при необходимости) вернуть обратно, добавив правила

3. Третий формализм. Теорема адекватности для исчисления

секвенций

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