Теорема 2.1

Определение

Предваренной (или пренексной) формулой называется формула вида , где Qi суть кванторы, а формула A (называемая матрицей предваренной формулы) уже кванторов не содержит.

Если и B – предваренная формула, то B называют предваренной (нормальной) формой (ПНФ) формулы A.

В частности, не исключается и случай n = 0, т.е. бескванторная формула также считается предваренной.

Для всякой формулы существует ПНФ.

Доказательство. С помощью основных логических законов устраняем в формуле все знаки логических операций, кроме (если таковые имеются).

К полученной формуле последовательно применяем в произвольном возможном порядке преобразования двух типов: А и В.

Преобразование типа А. Находим в формуле некоторую часть (подформулу) Ф, имеющую вид , или , или , или , где F, G(x) – какие-то формулы и G(x) содержит свободную переменную x. Пусть для определенности (в остальных случаях все делается точно так же).

Преобразуем Ф следующим образом: проверяем, содержит ли F переменную x, и если нет, то замещаем Ф на (соотношение (III.1)), если да, то заменяем все вхождения x в вхождениями какой-либо новой переменной, скажем, t, не встречающейся в нашей «боль-шой» формуле (соотношение (IV.1)), и затем заменяем на . Таким же образом поступаем с подформулами остальных трех видов (это возможно ввиду коммутативности конъюнкции и дизъюнкции).

Преобразование типа В. Находим в формуле некоторую подформулу, имеющую вид (или ), где G(x) – формула со свободной переменной x, и заменяем ее на (соответственно на ) по соотношениям (II.1), (II.2).

Применяя преобразования типов А и В, мы шаг за шагом «вытаскиваем наружу» все кванторы и, в конце концов, приходим к формуле, в которой ни один квантор не стоит внутри конъюнкции или дизъюнкции, или вслед за отрицанием. Но в такой формуле квантор может стоять только либо вслед за другим квантором, либо в самом начале формулы, т.е. получена ПНФ для исходной формулы.

Дата добавления: 2014-01-06