На этом шаге мы рассмотрим предваренную нормальную форму.
Формула находится в предваренной нормальной форме тогда и только тогда, когда она состоит из цепочки кванторов, называемой префиксом, и следующей за ней бескванторной формулы, называемой матрицей:
(Q1x1)( Q2x2) … (Qnxn)M,
где Qi - квантор всеобщности " или квантор
существования $, то есть (Qixi)
обозначает ("xi) или
($xi), i=1, 2, ..., n;
(Q1x1)( Q2x2) ... (Qnxn) - префикс формулы; M - матрица.
Например, следующие формулы находятся в предваренной нормальной форме:
("x)("y)(A(x,y)
ÙB(y));
("x)("y)( $z)(A(x,y)ÚB(y,z)ÚC(z)).
Для записи формул в предваренной нормальной форме можно использовать приведенные ниже эквивалентные формулы, в которых кванторы всеобщности " и существования $ обозначены буквой Q:
(Qx)A(x)ÚB=(Qx)(A(x)ÚB);
(Qx)A(x)ÙB=(Qx)(A(x)ÙB);
~(("x)A(x))=($x)(~A(x));
~(($x)A(x))=("x)(~A(x));
("x)A(x)Ù("x)B(x)= ("x)(A(x)ÙB(x));
($x)A(x)Ú ($x)B(x)= ($x)(A(x)ÚB(x));
(Q1x)A(x)Ú(Q2x)B(x)= (Q1x)(Q2y)(A(x)ÚB(y));
(Q3x)A(x)Ù(Q4x)B(x) =(Q3x)(Q4y)(A(x)ÙB(y)).
Здесь A(x) - форма, содержащая наряду с другими переменными и свободную переменную x; B - формула, содержащая любые переменные, кроме x.
На следующем шаге мы рассмотрим проверку общезначимости формул.
