Языки и исчисления




Исчисление высказываний (ИВ) - часть 4


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

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

Другие аксиомы описывают свойства логических связок. Аксиомы

и говорят, какие следствия можно вывести из конъюнкции ( и ). Напротив, аксиома 5 говорит, как можно вывести конъюнкцию. Из нее легко следует такое правило: если и , то (применяем эту аксиому и дважды правило MP). Часто подобные правила записывают так:

(над чертой пишут "посылки" правила, а снизу — его "заключение", вытекающее из посылок).

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

Аксиомы 6-7 позволяют утверждать, что и . Аксиома 8 обеспечивает такое правило:

Оно соответствует такой схеме рассуждения: "Пусть выполнено . Разберем два случая. Если выполнено , то и потому . Если выполнено , то и потому . В обоих случаях верно . Значит, влечет ."

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

24. Докажите, что следующие формулы, а также обратные к ним (меняем местами посылку и заключение) являются теоремами исчисления высказываний:

У нас остались еще три аксиомы, касающиеся отрицания. Аксиома 9 гарантирует, что из противоречивого набора посылок можно вывести что угодно: если и , то для любого . Аксиома 10, напротив, объясняет, как можно вывести отрицание некоторой формулы : надо допустить и вывести два противоположных заключения и . Точнее говоря, имеет место такое правило:

(в самом деле, дважды применяем лемму о дедукции, а затем правило MP с аксиомой 10).

Аксиомы 9 и 10 позволяют вывести некоторые логические законы, связанные с отрицанием.


Содержание  Назад  Вперед