Исчисление высказываний

Исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций). В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.

Обозначения

A, B, C — одиночные формулы;

Γ, Г₁, Г₂ — списки формул антецедента, возможно пустые;

Δ, Δ₁, Δ₂ — списки формул сукцедента, возможно пустые;

A₁, A₂, …, A_n — формулы списка антецедента;

B₁, B₂, …, B_m — формулы списка сукцедента;

F(x) — формула со свободной переменной;

F(t) — формула со значением терма вместо свободной переменной;

Ø — пустое множество формул;

├ — знак вывода;

L –– изменения слева –– изменения в антецеденте;

R –– изменения справа –– изменения в сукцеденте ;

W –– ослабление;

C –– сокращение;

P –– перестановка;

˄ –– конъюнкция;

˅ –– дизъюнкция;

¬ –– отрицание;

→ –– импликация;

Ɐ –– квантор всеобщности;

Ǝ –– квантор существования.

Определения

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

Интуитивный смысл, закладываемый в секвенцию A₁, A₂,..., A_n├ B₁, B₂,..., B_m — если выполнена конъюнкция формул антецедента A₁, A₂,..., A_n, то имеет место (выводится) дизъюнкция формул сукцедента B₁, B₂,..., B_m.

˄Ø — конъюнкция формул пустого множества — тождественно истинное высказывание;

˅Ø — дизъюнкция формул пустого множества — тождественно ложное высказывание;

Γ├ — секвенция с противоречивым антецедентом, которая имеет смысл Γ├ ˅Ø;

├ Δ — секвенция подразумевает выполнимый сукцедент, которая имеет смысл ˄Ø├ Δ;

├ — секвенция с противоречивым выводом, которая имеет смысл ˄Ø├ ˅Ø;

Система LK

Система LK –– это классическое генценовское исчисление секвенций (построенная Генценом в 1934 году). В системе LK одна аксиома и 21 правило вывода, которые делятся на структурные, логические и кванторные. Структурные правила (7) –– это правила WL, WR, CL, CR, C, PL, PR. Логические правила (10) –– это правила ¬L, ¬R, ˄L₁, ˄L₂, ˄R, ˅L, ˅R₁, ˅R₂, →L, →R. Кванторные правила (4) –– это правила ⱯL, ⱯR, ƎL, ƎR.

Аксиома

~ аксиома

Основные правила

• Основные правила включают в себя структурные и логические.
• Основные правила легко преобразуются в аналогичные с помощью перестановки и наоборот.

Кванторные правила

• Кванторные правила используют кванторы и формулы со свободной переменной или с термами.
• Кванторные правила для удобства применения представлены в двух вариантах.

Пример вывода

• Приведён вывод закона исключённого третьего в системе LK.

Ссылки

• https://en.wikipedia.org/wiki/Sequent_calculus