Математическая логика и теория алгоритмов
|
1.3 Исчисление высказываний (ИВ) |
назад | оглавление | вперёд |
       
Одним из важных примеров аксиоматической теории может служить исчисление высказываний (один из возможных способов формализации логики высказываний). Исчисление – основанный на четких правилах формальный аппарат оперирования со знаниями определенного вида, позволяющий дать точное описание некоторого класса задач, а для отдельных подклассов этого класса и алгоритм решения.
       
Логическое исчисление строится на базе некоторого формализованного языка. Задается набор исходных символов, из которых с помощью четко определенных правил строятся формулы рассматриваемого исчисления. Некоторые из этих формул выбираются в качестве аксиом, из которых с помощью правил преобразования получают новые формулы, называемые теоремами. После того как к исчислению добавляется интерпретация, придающая значение ее исходным символам и формулам, исчисление превращается в язык, описывающий некоторую предметную область.
        Определим исчисление высказываний (ИВ) как формальную аксиоматическую теорию L следующим образом :
       Выводимость формул в теории L доказывается путем предъявления конкретного вывода, т.е. последовательности формул, удовлетворяющих определению. Для удобства формулы последовательности вывода располагаются друг под другом в столбик, а справа указывается на каком основании формула включена в вывод. В качестве примера приведем доказательства двух теорем.
1 | A | гипотеза |
2 |
![]() |
A 1 |
3 |
![]() |
MP 1,2 |
       Всякую доказанную выводимость можно
использовать как новое (производное) правило вывода. Последняя доказанная теорема (Теорема 2) называется правилом введения импликации: .