Предваренная нормальная форма формул логики предикатов

В алгебре логики было введено понятие нормальной дизъюнктивной и конъюнктивной форм функции. В логике предикатов, сохраняя преемственность, используют аналогичное понятие для формул логики предикатов,отличающееся тем, что оно, кроме операций дизъюнкции, конъюнкции

и отрицания, распространяется и на кванторные операции и определяется следующим образом.

Определение. Нормальной формой формулы логики предикатов является такая формула, которая содержит только операции конъюнкции. дизъюнкции и кванторные операции, а операция отрицания применяется только к элементарным формулам. Под элементарной формулой понимается один отдельно взятый предикат.

Замечание. Иногда вместо термина нормальная, форма используется термин приведенная форма. Однако, по мнению автора, второй термин является неудачным, так как он не сохраняет преемственности между логикой предикатов и алгеброй логики. И если использовать этот термин, то окажется, что в логике предикатов и в алгебре логики очень похожие понятия называются разными словами, что делает саму логику не логичной. Приведем пример приведения формулы к нормальному виду. Для этого будем использовать равносильные преобразования.

Кванторные операции обусловливают появление новых форм формул (новых относительно алгебры логики). Такой формой является так называемая предваренная нормальная форма (ПНФ).

Определение. Под ПНФ понимается такая форма, в которой кванторные операции либо полностью отсутствуют, либо они предшествуют всем формулам логики предикатов. Иначе говоря, ПНФ имеет вид

где под символами (δx) понимается один из кванторов а формула В кванторов не содержит.

Примерами формул, записанных в ПНФ, являются формулы 1.1). 4). 6); 2.1), 2), 3), 4), 8) из упражнений к подразд. 3.5. А примерами формул. записанных не в ПНФ, являются формулы 1.3), 5); 2.5), 6), 7) из тех же упражнений.

Приведем без доказательства теорему, которая утверждает следующее.

Теорема. Всякая формула логики предикатов может быть приведена к ПНФ.

Пример приведения формулы логики предикатов к ПНФ.