Б) Обоснование правил вывода.

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

Рассмотрим для примера правило транзитивности импликации, его семантическое и синтаксическое обоснование.

Сначала остановимся на семантическом обосновании.

(А É В), (В É С) и (А É С) существует отношение логического следования, поэтому невозможно, чтобы посылки (А É В) и (В É С) были истинными, а заключение (А É С) – ложным.

Допустим, что это не так (то есть, что А É В и В É С – истинные, а

А É С – ложно). Но А É С – ложно, когда А – истинно, а С – ложно. А в посылках: если А – истинно, а С – ложно, то при любом значении В конъюнкция посылок не может быть истинной, что противоречит исходному допущению. Таким образом, посылки в нашем правиле не могут быть истинными, а заключение – ложным, что свидетельствует о корректности правила и гарантирует правильность соответствующих его структуре конкретных рассуждений.

Схематически подобная проверка корректности данного правила вывода выглядит следующим образом:

(И)А É (И/Л) В

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

Доказательство осуществляется следующим образом: