Алгебраические системы - Мальцев А.И.
Скачать (прямая ссылка):
Итак, бесконечная система формул @ невыполнима. Отсюда, согласно принципу локализации (см. примеры и дополнения к § б, доп. 4), вытекает, что невыполнима некоторая ее конечная подсистема - %, 1Я(ГШ ..., Tim, Уі,..., уп), ...
П«(Гм..... * him Уі, . ¦ ¦, Уп),
т. е. невыполнима формула % &H 1 (Гц, .. ., Tim, Iji, ..., уп) &.. .
... & н St (Tki, ..., Tkm, Уі, ..., Уп) и, значит, тождественно истинна формула
St^11,..., ¦L Int» У и • • .. Уп)У ...
...\J%(Thi, ...,Tkm, Уі, ...,уп). Обратная импликация
Ш(Тп, ...,Tim, Уі, ..., Уп)У ...
...у%(Тк „ ..., Tkm, уи ...,уп) S
также тождественно истинна, так как, если стоящая слева от знака импликации формула истинна в какой-то алгебраической системе SJi для некоторых уи ..., уп, то какая-то формула St (Tiu . .., Tim, ..., уп) истинна в 5Ш. Поэтому формула 21 (Xi, ..., xm, уи .. ., уп) истинна для Xi = Tii, ..., Xm = Tim, и потому $ также истинна. Итак, % эквивалентна бескванторной формуле
SI (Tii,..., 1 im, У и . ..,ЫV•••
... V Sl (Tni, ..., Tkm, yi7 ..., Уп), (5)
что и требовалось.
Изложенное доказательство теоремы 2 не конструктивно, т. е. в нем не указывается алгоритм для построения формулы (5). Однако такой алгоритм существует. Пользуясь алгоритмом Гильберта (см. примеры и дополнения к § 6, доп. 3), строим все тождественно истинные формулы вида g fjj, % -*- gf3, ... Одновременно строим 168
ЯЗЫКИ ПЕРВОЙ II ВТОРОЙ СТУПЕНИ
[Гл. III
цепочки всех тождественно истинных формул вида %і —>-
Sn» Si %і2-> • - - и продолжаем этот процесс до тех пор, пока не получатся формулы % -у- і З1 і S1 > ГДе gfj — бескванторная формула. Теорема 2 гарантирует, что такая формула найдется.
Рассматривая отрицание V-формулы, получаем из теоремы 2 непосредственное
Следствие. Если Ч-формула устойчива относительно перехода к надсистемам, то она эквивалентна -некоторой бескванторной формуле.
Поставим следующий вопрос: существует ли алгоритм, позволяющий по записи произвольной формулы ^ ПИП узнать, эквивалентна эта формула или нет какой-нибудь V-формуле?
Теорема 3. Не существует алгоритма, позволяющего по записи произвольной замкнутой формулы % ПИП узнать, эквивалентна или нет формула gf какой-нибудь 3-формуле {у-формуле).
Согласно теореме Чёрча (см. Клини [22], стр. 382, теорема 54) не существует алгоритма, позволяющего по записи формул УИП распознавать их тождественную истинность. Покажем, что если бы у нас был алгоритм Jk, позволяющий узнать, эквивалентна или нет произвольная формула какой-нибудь 3-формуле, то с помощью Jk мы могли бы распознавать тождественно истинные формулы и вступили бы в противоречие с теоремой Чёрча.
Итак, пусть упомянутый алгоритм Л нам известен, и пусть % — произвольная формула УИП. Смотрим, эквивалентна или нет формула § какой-нибудь 3-формуле. Если нет, то % не может быть тождественно истинной, так как каждая тождественно истинная формула эквивалентна 3-формуле (Зж) х = х. Пусть ответ «да». Тогда при помощи процесса Гильберта строим последовательно все формулы, эквивалентные формуле и выбираем среди них первую 3-формулу ^1. Остается узнать, будет ли тождественно истинной, т. е. будет или нет формула выполнимой. Формула H^1 обычным путем приводится к универсальному виду. Следовательно, вопрос о ее выполнимости в силу теоремы 1 равносилен вопросу о выполнимости Hyj на какой-нибудь одноэлементной системе и потому может быть решен эффективно. КЛАССИФИКАЦИЯ ФОРМУЛ
169
Аналогично доказывается утверждение теоремы 3 и для V-формул.
В заключение сделаем несколько замечаний по поводу теоремы 2. Формулы вида
P (її) • • • і їт)і F (її, • ¦ • і Zn) — Ъп + П
где Ii — предметные переменные, P — предикатный, F ~~ функциональный сигнатурные символы, называются атомарными формулами. Формулы, построенные из атомарных формул и знаков &, \j, —>• (т. е. без кванторов), называются абсолютно бескванторными. Формулы вида
[Q1Xli . .. х1Т) .. . (Qixli . .. Xu)
где — абсолютно бескванторная формула, a Q1, . . . . . ., Qi— чередующиеся кванторы, называются абсолютными Q1 .. . Qi-формулами.
Если сигнатура не содержит функциональных символов, то, очевидно, понятия Q1 . . . (?гформулы и абсолютной Q1 . . . (?гформулы совпадают. Для произвольной сигнатуры указанные понятия не совпадают, однако в этом случае имеет место следующее утверждение.
Теорема 4. Каждая Q1 ... Q гформула (I 1) эквивалентна подходящей абсолютной Q1 .. . Qi-формуле.
Для доказательства достаточно показать, что формула вида f = g, где /, g — термы, эквивалентна и подходящей абсолютной 3-формуле вида
(3 xi...xp)(B1& ...&Bq), (6)
и подходящей абсолютной V-формуле вида
(Ужі . . . xr) (C1 & . .. &CS—>C0), (7)
где Bi, Cj— атомарные формулы.
Доказательство ведем индукцией по числу v функциональных знаков, участвующих в записи формулы / = g. При v I формула / = g атомарная и доказывать нечего. Пусть у> 1, тогда формула / — g имеет вид Fi (/1,- • -і /m) ~ h и потому эквивалентна формуле
(3xt . . . XmJrl) (X1 = Z1 & . . .
, .. &. хт = fm & XmJrl = Fi (X1, . .., хт) & жт+1 = h), (8) 170 ЯЗЫКИ ПЕРВОЙ II ВТОРОЙ СТУПЕНИ [Гл. III
