Математическая логика и теория алгоритмов

1.3 Исчисление высказываний (ИВ)

назад | оглавление | вперёд

 

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

        Определим исчисление высказываний (ИВ) как формальную аксиоматическую теорию L следующим образом :

  1. Алфавит ИВ образуют буквы A, B, C,... и т . д . ( возможно с индексами ), которые называются пропозициональными переменными , логические символы ( связки, ¬ , → ),а также вспомогательные символы скобок (, ).
  2. Множество формул ИВ определяется индуктивно :
  3. Аксиомы ИВ (классическое определение):
        
  4. Единственным правилом вывода в ИВ является правило отделения (modus ponens): если A и – выводимые формулы , то B – также выводимая формула . Символическая запись :
       Здесь А, В – любые формулы. Таким образом, множество аксиом теории L бесконечно, хотя задано тремя схемами аксиом. Множество правил вывода также бесконечно, хотя оно задано только одной схемой.
       Договоримся далее опускать внешние скобки у формул. Другие логические связки вводятся определениями: . Любая формула, содержащая эти связки, рассматривается как синтаксическое сокращение собственной формулы теории L .

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


Теорема 1. .
Доказательство:
1. A 1:B ← (A→A)
2. A 2: B ← (A→A);C ← A
3. MP 1,2
4. A 1: B ← A
5. MP 4,3
       Теорема доказана.

Теорема 2. .
Доказательство:
1 A гипотеза
2 A 1
3 MP 1,2
       Теорема доказана.

       Всякую доказанную выводимость можно использовать как новое (производное) правило вывода. Последняя доказанная теорема (Теорема 2) называется правилом введения импликации: .


назад | оглавление | вперёд