Приглашаем посетить сайт
ПРЕДВАШННАЯ ФОРМА
ПРЕДВАШННАЯ ФОРМА - нормальная форма представления формул предикатов исчисления, имеющая (в общем случае) вид:
где Qι (0 ≤ ι ≤ n) - квантор общности (∀) или существования (∃); (...) - формула, не содержащая кванторов и находящаяся в области действия каждого Qι; а x1, х2, ..., хn - попарно различные переменные, каждая из к-рых по крайней мере один раз входит в (...) свободно [при этом (...), наз. матрицей, может содержать и др. свободные переменные]. Выражение Q1x1Q2x2 ... Qnxn, стоящее перед (...), наз. приставкой, или префиксом. В классич. исчислении предикатов доказывается след. метатеорема: "Для каждой формулы А исчисления предикатов существует (может быть найдена средствами этого исчисления) формула В формы (*) (являющаяся, т.о., П. ф. формулы А) такая, что АПРЕДВАШННАЯ ФОРМАВ". Доказательство этой метатеоремы вытекает непосредственно из способа построения П. ф., к-рый основан на использовании нек-рых выводимых в исчислении предикатов эквивалентностей, в частности (для классич. случая):
к-рые позволяют отрицание всякой формулы переносить в ее подкванторную часть; эквивалентностей:
в к-рых А не содержит свободных вхождений переменной х; а также
[соответственно:
где n - число всех ∃, а m - число всех ∃ входящих в эту формулу (т.н. П. ф. Сколема). Этот результат стимулировал метатеоретич. исследования (см. Метатеория) в направлении поиска т.н. редукционных теорем (теорем о сведении), позволяющих выяснить возможные частные, - обусловленные как раз видом приставок П. ф., - случаи решения проблемы разрешения для логики предикатов (об этом см. J. Suranyi, Reduktionstheorie des Entscheidungsproblems im Prδdikatenkalkόl der ersten Stufe, Bdpst, 1959).
Лит.: Гильберт Д. и Аккерман В., Основы теоретич. логики, пер. с нем., М., 1947, с.112-17; Клини С. К., Введение в метаматематику, пер. с англ., М., 1957, с. 152-53; Новиков П. С., Элементы математич. логики, М., 1959, гл. 3, § 9; Чёрч Α., Введение в математическую логику - пер. с англ., М., 1960, § 39.
М. Новоселов. Москва.