ПРЕДВАРЁННАЯ ФОРМА

ПРЕДВАРЁННАЯ ФОРМА

нормальная форма представления формул предикатов исчисления, имеющая (в общем случае) вид:

ФОРМА">

где 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.

М. Новоселов. Москва.