Исчисление предикатов

Исчисление предикатов – это формальная теория P, в которой определены следующие компоненты:

1.Алфавит:

– основные связки;

– дополнительные связки;

(,) – служебные символы (открывающая и закрывающая скобки, а также запятая);

- кванторы всеобщности и существования;

- предметные константы;

– предметные переменные;

- предикаты;

- функциональные символы (функторы). С каждым предикатом и функтором связано некоторое натуральное число называемое кратностью или местностью.

Все выражения исчисления предикатов строятся из выше перечисленных символов алфавита. Среди таких выражений различают термы.

Термы – это выражения, которые являются аналогами имен объектов теории и соответствующих именных форм. По индуктивному определению терм - это:

предметные переменные и константы;

если - n –местный функциональный символ и - термы, то - терм;

других термов, кроме построенных по пп. 1) и 2) нет.

Из термов с помощью предикатных символов (имен конкретных предикатов) строятся атомы. Атомом (атомарной формулой, элементарной формулой) называется любая пропозициональная переменная (0-местная предикатная переменная), а также выражение вида , где: - n –местный предикатный символ, а - термы.

2. Формулы.

атом есть формула;

если А и В – формулы, то выражения считаются формулами;

если А – формула, а x предметная переменная, то выражения , считаются формулами.

3. Аксиомы исчисления предикатов P включают в себя все аксиомы исчисления высказываний L, плюс

: ,

: .

Здесь: t – терм свободный для переменной x в формуле A

4. Правила вывода:

,

-правило,

-правило.

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

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

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

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

Установлено что интерпретация исчисления высказываний в логику предикатов адекватно.

Можно доказать что исчисление предикатов не противоречиво.

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

2.9. АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

2.9.1. Постановка задачи

Алгоритм, который проверяет отношение для формулы S, множества функций Г, в формально теории Т называется алгоритмом автоматического доказательства теорем.

В общем случае такой алгоритм невозможен т.к. не существует правила по которому для любых S, Г и Т выдавался бы ответ “да” если верно, что и ответ “нет” если не верно, что . Более того, известно также, что нельзя построить автоматического доказательства теорем для большинства конкретных достаточно сложных формальных теорий. В некоторых случаях удается построить алгоритм автоматического доказательства теорем, который применим не ко всем формулам теории (частичный алгоритм).

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

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

Классический алгоритм автоматического доказательства теорем называется методом резолюций. Для любого приклад­ного исчисления предикатов первого порядка Т, любой формулы S и множества формул Г теории Т метод резолюций выдает от­вет «да» если и выдает ответ «нет», или не выдает ника­кого ответа, (т.е. зацикливается) если неверно, что .

В ос­нове метода резолюции лежит идея доказательства «от противного».

Теорема: Если , где F – любое противоречие (тождественно ложная формула), то .

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