Элементы математической логики Лекция 6. Исчисление высказываний (ив)

1. Аксиомы.

2. Формальное доказательство и формальный вывод.

3. Свойства отношения выводимости

4. Некоторые вспомогательные правила вывода.

5. Полнота, непротиворечивость и независимость аксиом исчисления высказываний.

Чтобы формализовать процесс человеческого мышления и попытаться создать искусственный интеллект, строятся формальные системы. В их основе лежит алфавит, т.е. не пустое множество, конечное, элементы его называются символами. Любая упорядоченная последовательность символов называется словом. Построение формальной системы начинается с того, что отбираются исходные слова в той или иной предметной области. Эти начальные слова называются аксиомами. Потом формулируют правила, с помощью которых из аксиом получаются слова, которые называют теоремами. Процесс получения теорем из аксиом с помощью правил вывода можно записать в виде последовательности. Она называется доказательством теоремы. Исчисление высказываний - пример формальной аксиоматической теории.

В алгебре высказываний рассматривался класс общезначимых формул, выражающих законы логики, на основе понятия истинностного значения. В исчислении высказываний законы логики — множество доказуемых формул — рассматривается по-другому. Принимаются некоторые формулы в качестве «аксиом», а для получения новых формул вводят некоторое «правило вывода».

Алфавит исчисления высказываний состоит из логических переменных, которые будем обозначать большими буквами латинского алфавита (возможно с индексами), из логических связок ¬ и круглых скобок. Понятие формулы исчисления высказывания дается так же, как и в алгебре высказываний.

6.1 Аксиомы

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

а) импликации и отрицания,

б) импликации и дизъюнкции,

в) импликации, отрицания, конъюнкции и дизъюнкции

можно использовать в процессе дедуктивного вывода любую из указанных систем.

Определение. Аксиомами теории L назовем всякие формулы, которые порождают нижеследующие формульные схемы при любом выборе формул А, В, С:

Каждая из схем (1) — (13) порождает счетное множество аксиом, если символы А, В, С заменять конкретными формулами. Поэтому записи (1) — (13) будем называть аксиомными схемами (АС).

АС (1) и АС (2) представляют собой аксиомы для оператора ,

АС (3) вводит оператор /\, а АС (4) и АС (5) его удаляют.

АС (6) и АС (7) вводят оператор V, АС (8) его удаляет,

АС (9) служит для введения оператора ¬, АС (10) удаляет оператор ¬,

АС (11) вводит оператор , АС (12) и АС (13) этот оператор удаляют.

Определение. Правилом вывода теории L называют процедуру перехода от двух формул вида А и АВ к одной формуле вида В для любых А и В.

Это правило называют modus ponens, МР. Правило МР позволяет удалять оператор , поэтому его называют также правилом удаления импликации и обозначают УИ. В случае применения правила МР формулы А и АВ называют посылками, a В — заключением этого правила: