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

нормальная форма представления формул предикатов исчисления, имеющая (в общем случае) вид: где Q? (0 ? ? ? n) – квантор общности (?) или существования (?); (...) - формула, не содержащая кванторов и находящаяся в области действия каждого Q?; а x1, х2, ..., хn - попарно различные переменные, каждая из к-рых по крайней мере один раз входит в (...) свободно [при этом (...), наз. матрицей, может содержать и др. свободные переменные]. Выражение Q1x1Q2x2 ... Qnxn, стоящее перед (...), наз. приставкой, или префиксом. В классич. исчислении предикатов доказывается след. метатеорема: "Для каждой формулы А исчисления предикатов существует (может быть найдена средствами этого исчисления) формула В формы (*) (являющаяся, т.о., П. ф. формулы А) такая, что АПРЕДВАРЁННАЯ ФОРМАВ". Доказательство этой метатеоремы вытекает непосредственно из способа построения П. ф., к-рый основан на использовании нек-рых выводимых в исчислении предикатов эквивалентностей, в частности (для классич. случая): к-рые позволяют отрицание всякой формулы переносить в ее подкванторную часть; эквивалентностей: в к-рых А не содержит свободных вхождений переменной х; а также (или правил переименования связанных переменных) и дистрибутивности законов для ? и ?. Возможность представления каждой формулы исчисления предикатов в П. ф. существенно облегчает рассмотрение вопросов, связанных с его разрешения проблемой. Особенно полезным в этом отношении является результат Сколема, позволяющий свести рассмотрение вопроса о выполнимости [общезначимости] произвольной формулы исчисления предикатов к рассмотрению только такой ее П. ф., к-рая имеет вид: