Исчисление высказываний
Исчисление высказываний – это аксиоматическая логическая система, интерпретацией которой является алгебра высказываний.
Описание
всякого исчисления включает в себя описание символов этого исчисления
(алфавита); формул, являющихся конечными конфигурациями символов и определение
выводимых формул.
Алфавит исчисления
высказываний состоит из символов трех категорий:
1)
Символы первой категории: x, y, z,…,x1, x2,…, которые
называются переменными высказывания;
2)
Символы второй категории: 
, которые называются логическими связками.
– дизъюнкция
(логическое сложение), 
– конъюнкция
(логическое умножение), → – импликация (логическое следование), ¯ –
отрицание;
3)
Символы третьей категории: скобки.
Других
символов исчисление высказываний не имеет.
Формулы исчисления
высказываний представляют собой последовательности символов алфавита исчисления
высказываний. Для обозначения формул будем пользоваться заглавными буквами
латинского алфавита. Эти буквы не являются символами исчисления. Они
представляют собой условные обозначения формул.
Определение формулы исчисления
высказываний.
1.
Всякая переменная x, y, z,… является
формулой.
2.
Если A
и B – формулы,
то слова 
– формулы.
3.
Никакая другая строчка символов не является формулой.
Переменные
высказывания называются элементарными
формулами.
Определение подформулы.
1.
Подформулой
элементарной формулы является только она сама.
2.
Если формула имеет вид 
, то ее подформулами являются: она
сама, формула 
и все подформулы формулы .
3.
Если формула имеет вид 
(под символом 
понимается
любая из трех связок 
), то ее подформулами являются: она
сама, формулы и 
, все подформулы формул и .
Замечание. Скобки в записи
формул можно опускать по тем же правилам, что и в алгебре высказываний.
Система аксиом исчисления
высказываний:
I группа. I1 x→(y→x); I2
(x→(y→z))→((x→y)→(x→z)).
II группа. II1 
; II2 
; II3 
.
III группа. III1 
; III2 
; III3 
.
IV группа. IV1 
; IV2 
; IV3 
.