Общезначимость и выполнимость формул

Определение 4.14. Формула А логики предикатов называется выполнимой в области М, если существуют значения переменных, входящих в эту формулу и отнесенных к области М, при которых формула А принимает истинные значения.

Определение 4.15. Формула А называется выполнимой, если существует область, на которой эта формула выполнима.

Из определения 4.15 следует, что, если формула выполнима, то это еще не означает, что она выполнима в любой области.

Определение 4.16. Формула А называется тождественно истинной в области М, если она принимает истинные значения для всех значений переменных, входящих в эту формулу и отнесенных к этой области.

Определение 4.17. Формула А называется общезначимой, если она тождественно истинная на всякой области.

Определение 4.18. Формула А называется тождественно ложной в области М, если она принимает ложные значения для всех значений переменных, входящих в эту формулу и отнесенных к этой области.

Из приведенных определений следует:

1) если формула А общезначима, то она и выполнима на всякой области;

2) если формула А тождественно истинная в области М, то она и выполнима в этой области;

3) если формула А тождественно ложная в области М, то она не выполнима в этой области;

4) если формула А не выполнима, то она тождественно ложна на всякой области.

В связи с данными определениями естественно выделить два класса формул логики предикатов: выполнимых и не выполнимых формул.

Отметим, что общезначимую формулу называют логическим законом.

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

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

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

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

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

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

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

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

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

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

Определение 4.19. Если формула логики предикатов С содержит свободные переменные х₁, х₂,..., х_п, то формула

А = х₁ х₂ ... х_п С(х₁, х₂, ..., х_п)

называется замыканием общности формулы С, а формула

В = $х₁ $х₂ ... $х_п С(х₁, х₂, ..., х_п)

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

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

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