Исчисление высказываний — различия между версиями
м |
м |
||
| Строка 41: | Строка 41: | ||
'''Ǝ''' –– квантор существования. | '''Ǝ''' –– квантор существования. | ||
== Определения == | == Определения == | ||
| − | '''Секвенцией''' называется выражение вида '''Γ├ Δ''', где '''Γ''' и '''Δ''' — конечные последовательности логических формул. | + | '''Секвенцией''' называется выражение вида '''Γ├ Δ''', где '''Γ''' и '''Δ''' — конечные последовательности логических формул. |
| + | |||
| + | Формула антецедента '''Γ={A<sub>1</sub>, A<sub>2</sub>,..., A<sub>n</sub>}''', формула сукцедента '''Δ={B<sub>1</sub>, B<sub>2</sub>,..., B<sub>m</sub>}'''. | ||
Интуитивный смысл, закладываемый в секвенцию '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>n</sub>├ B<sub>1</sub>, B<sub>2</sub>,..., B<sub>m</sub>''' — если выполнена конъюнкция формул антецедента '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>n</sub>''', то имеет место (выводится) дизъюнкция формул сукцедента '''B<sub>1</sub>, B<sub>2</sub>,..., B<sub>m</sub>'''. | Интуитивный смысл, закладываемый в секвенцию '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>n</sub>├ B<sub>1</sub>, B<sub>2</sub>,..., B<sub>m</sub>''' — если выполнена конъюнкция формул антецедента '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>n</sub>''', то имеет место (выводится) дизъюнкция формул сукцедента '''B<sub>1</sub>, B<sub>2</sub>,..., B<sub>m</sub>'''. | ||
Версия 09:02, 2 апреля 2025
Исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций). В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.
Содержание
Обозначения
A, B, C — одиночные формулы;
Γ, Г1, Г2 — списки формул антецедента, возможно пустые;
Δ, Δ1, Δ2 — списки формул сукцедента, возможно пустые;
A1, A2, …, An — формулы списка антецедента;
B1, B2, …, Bm — формулы списка сукцедента;
F(x) — формула со свободной переменной;
F(t) — формула со значением терма вместо свободной переменной;
Ø — пустое множество формул;
├ — знак вывода;
L –– изменения слева –– изменения в антецеденте;
R –– изменения справа –– изменения в сукцеденте ;
W –– ослабление;
C –– сокращение;
P –– перестановка;
˄ –– конъюнкция;
˅ –– дизъюнкция;
¬ –– отрицание;
→ –– импликация;
Ɐ –– квантор всеобщности;
Ǝ –– квантор существования.
Определения
Секвенцией называется выражение вида Γ├ Δ, где Γ и Δ — конечные последовательности логических формул.
Формула антецедента Γ={A1, A2,..., An}, формула сукцедента Δ={B1, B2,..., Bm}.
Интуитивный смысл, закладываемый в секвенцию A1, A2,..., An├ B1, B2,..., Bm — если выполнена конъюнкция формул антецедента A1, A2,..., An, то имеет место (выводится) дизъюнкция формул сукцедента B1, B2,..., Bm.
˄Ø — конъюнкция формул пустого множества — тождественно истинное высказывание;
˅Ø — дизъюнкция формул пустого множества — тождественно ложное высказывание;
Γ├ — секвенция с противоречивым антецедентом, которая имеет смысл Γ├ ˅Ø;
├ Δ — секвенция подразумевает выполнимый сукцедент, которая имеет смысл ˄Ø├ Δ;
├ — секвенция с противоречивым выводом, которая имеет смысл ˄Ø├ ˅Ø;
Система LK
Система LK –– это классическое генценовское исчисление секвенций (построенное Генценом в 1934 году). В системе LK одна аксиома и 21 правило вывода, которые делятся на структурные, логические и кванторные. Структурные правила (7) –– это правила WL, WR, CL, CR, C, PL, PR. Логические правила (10) –– это правила ¬L, ¬R, ˄L1, ˄L2, ˄R, ˅L, ˅R1, ˅R2, →L, →R. Кванторные правила (4) –– это правила ⱯL, ⱯR, ƎL, ƎR.
Аксиома
~ аксиома
Основные правила
- Основные правила включают в себя структурные и логические.
- Основные правила легко преобразуются в аналогичные с помощью перестановки и наоборот.
Кванторные правила
- Кванторные правила используют кванторы и формулы со свободной переменной или с термами.
- Кванторные правила для удобства применения представлены в двух вариантах.
Пример вывода
- Приведён вывод закона исключённого третьего в системе LK.
