2.3. Исчисление высказываний

Логическим исчислением, ил и просто исчислением, называют совокупность, которая включает в себя: алфавит (совокупность используемых символов); синтаксические правила построения формул в алфавите; аксиомы (общезначимые исходные формулы); правила вывода по аксиомам производных формул или теорем.

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

2.3.1. Классическое исчисление высказываний

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

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

Классическое исчисление высказываний использует два правила вывода.

Модус поненс. Из истинности условия импликации и истинности самой импликации следует истинность следствия импликации:

Правило подстановки. Из формулы выводима формула а получающаяся подстановкой в формулу вместо каждого вхождения переменной формулы Р:

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

Исключение конъюнкта. Из истинности конъюнкции следует истинность любого ее конъюнкта:

Введение конъюнкции. Из списка истинных формул следует истинность их конъюнкции:

Введение дизъюнкции. Из истинности формулы следует истинность ее дизъюнкции с любыми другими формулами:

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

Простая резолюция (удаление дизъюнкта). Из истинности дизъюнкции и отрицания одного из ее дизъюнктов следует истинность формулы, получающейся из дизъюнкции удалением этого дизъюнкта:

Резолюция. Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая — его отрицание, следует формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания: