Исчисле́ние выска́зываний — это формальная теория, в которой осуществляется попытка формализации понятий логического закона и логического следования.
Высказывание относится к одному из неопределяемых понятий и задаётся аксиоматически: это утверждение,
которое может быть либо истинно, либо ложно. В ИВ высказывания рассматриваются как переменные (так называемые высказывательные, или пропозициональные переменные), которые могут принимать одно из двух значений: 1 (истина) либо 0 (ложь).
Кроме пропозициональных переменных, в ИВ используются так называемые логические связки.
Если - высказывание, то через будем обозначать отрицание этого высказывания. Зададим его таблицей:
Значение двуместных логических связок (импликация), (дизъюнкция)
и (конъюнкция) определются так:
Формулы
пропозициональные переменные являются формулами;
если — формулы, то , и — формулы.
если - формула, то - формула.
Тавтологии
Формула является тавтолгией, если она истинна при любых значениях входящих в нее переменных. Вот несколько широко известных
примеров тавтолгий логики высказываний:
Теорема корректности ИВ утверждает, что все перечисленные выше аксиомы являются тавтологиями, а с помощью правила modus ponens из истинных высказываний можно получить только истинные. Доказательство этой теоремы тривиально и сводится к непосредственной проверке. Куда более интересен тот факт, что все остальные тавтологии можно получить из аксиом с помощью правила вывода - это так называемая теорема полноты логики высказываний.