Связь между общезначимостью и выполнимостью формул логики предикатов.

Теорема 1. Для того, чтобы формула    F   была общезначимой, необходимо и достаточно, чтобы её отрицание было не выполнимо.

Теорема 2. Для того, чтобы формула    F    была выполнима, необходимо и достаточно, чтобы формула была не общезначима.

Проблема разрешения для общезначимости и выполнимости формул.

Постановка проблемы и её неразрешимость в общем виде: в алгебре высказываний было установлено, что существует четкий алгоритм, позволяющий для любой формулы алгебры высказываний ответить на вопрос, будет ли данная формула выполнима, тождественно истинна или тождественно ложна. Для этого нужно составить ТИ (таблица истинности) формулы и посмотреть на распределение нулей и единиц в её последнем столбце. Аналогичная проблема возникает и для формул логики предикатов: существует ли единый алгоритм, позволяющий для любой формулы логики предикатов определить, будет ли она выполнимой или общезначимой? Ответ отрицательный: общего такого алгоритма не существует. Это было доказано в 1936 г. Американским ученым А. Черчем.

Для некоторых частных видов формул данная проблема допускает решение.

Решение проблемы для формул на конечных множествах.

Пусть формула логики предикатов рассматривается на конечном множестве. Вместо её предикатных переменных подставляем конкретные предикаты, определенные на этом конечном множестве. Т.к. операции квантификации сводятся к конъюнкции и к дизъюнкции

,

то задача о выполнимости и общезначимости формулы логики предикатов на конечном множестве сводится к задаче о выполнимости или общезначимости некоторой формулы алгебры высказываний. А эта задача разрешима.

Продемонстрируем идею действия этого алгоритма на конкретном примере. Рассмотрим формулу логики предикатов

и выясним, будет ли она выполнима или общезначима на двухэлементном множестве .

Алгоритм распознавания общезначимости формул в частных случаях

1. Проблема разрешимости в случае конечных областей.

Очевидно, что проблема разрешимости в случае конкретных областей разрешима. В этом случае кванторные операции можно заменить операциями & и и тем самым свести формулулогики предикатов к формуле алгебры логики, для которой проблема разрешимости разрешима.

Пример 1. Формула в области, состоящий из двух элементов, приводится к виду:

2. Проблема разрешимости для формул, содержащих в предваренной нормальной форме кванторы одного типа.

Определение 1. Формула логики предикатов называется замкнутой, если она не содержит свободных предикатных переменных.

Определение 2. Если формула логики предикатов   F   содержит свободные переменные , то формула называется замыканием общности формулы    F,

формула называется замыканием существования формулы    F.

Теорема 1

Если формула логики предикатов, содержащая только одноместные предикатные переменные, выполнима, то она выполнима на конечном множестве, содержащем не более элементов, гдеn-число различных предикатных переменных, входящих в рассматриваемую формулу.

Следствие

Если замкнутая формула , в которую входят только одноместные предикатные переменные , тождественно истинна на множестве из элементов, то она общезначима.

Решение проблемы для -формул и-формул.

Проблема разрешимости общезначимости для двух типов формул ЛП – --формул и-формул: => и в этих случаях она сводится к тождественной истинности формул на конечных множествах.

Определение. Под -формулой понимается формула

, (*)

у которой в предваренной нормальной форме кванторная часть содержит только кванторы общности.

Определение. Под -формулой понимается формула

, (**)

у которой в предваренной нормальной форме кванторная часть содержит только кванторы существования, причем ,, т.е. формулы (*) и (**)

(*)-замыкание общности формулы F

(**)-замыкание существования формулы F

Теорема 2. -формула общезначима тогда и только тогда, когда она тождественно истинна на n-элементном множестве.

Теорема 3. -формула общезначима тогда и только тогда, когда она тождественно истинна на одноэлементном множестве.