Проблема разрешимости в логике предикатов

Многие математические задачи являются частным случаем некоторой общей схемы и поэтому могут быть решены посредством применения обобщенной процедуры к конкретной задаче. Например, можно ответить на вопрос: делится ли полином f(x) на полином g(x) с помощью алгоритма деления. Если остаток от деления будет равен нулю, ответом на вопрос будет «да». Иначе – «нет».

Метод, позволяющий ответить «да» на произвольный частный случай общего запроса, называется разрешающей процедурой. Задача нахождения такого метода для некоторого общего запроса называется проблемой разрешимости этого запроса.

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

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

Проблема разрешимости в логике высказываний имеет положительное решение.

Проблема разрешимости в логике предикатов не так проста. Формула j языка логики предикатов выводима тогда и только тогда, когда j общезначима, т.е. истинна во всех интерпретациях. Однако, число интерпретаций языка логики предикатов может оказаться бесконечным, и мы не в состоянии их все проверить. Хотя проблема разрешимости логики предикатов не может быть решена в общем виде, для некоторых частных случаев существуют решения [4].

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

или нет.

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

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