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

ПРЕДВАРЁННАЯ ФОРМА
нормальная форма представления формул предикатов исчисления, имеющая (в общем случае) вид:

где 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.
М. Новоселов. Москва.

Философская Энциклопедия. В 5-х т. — М.: Советская энциклопедия. Под редакцией Ф. В. Константинова. 1960—1970.