Исчисление высказываний — различия между версиями
(начало) |
м |
||
| (не показано 5 промежуточных версий этого же участника) | |||
| Строка 7: | Строка 7: | ||
'''Δ, Δ<sub>1</sub>, Δ<sub>2</sub>''' — списки формул сукцедента, возможно пустые; | '''Δ, Δ<sub>1</sub>, Δ<sub>2</sub>''' — списки формул сукцедента, возможно пустые; | ||
| − | '''A<sub>1</sub>, A<sub>2</sub>, …, A<sub> | + | '''A<sub>1</sub>, A<sub>2</sub>, …, A<sub>m</sub>''' — формулы списка антецедента; |
| − | '''B<sub>1</sub>, B<sub>2</sub>, …, B<sub> | + | '''B<sub>1</sub>, B<sub>2</sub>, …, B<sub>n</sub>''' — формулы списка сукцедента; |
'''F(x)''' — формула со свободной переменной; | '''F(x)''' — формула со свободной переменной; | ||
| Строка 41: | Строка 41: | ||
'''Ǝ''' –– квантор существования. | '''Ǝ''' –– квантор существования. | ||
== Определения == | == Определения == | ||
| − | '''Секвенцией''' называется выражение вида '''Γ├ Δ''', где '''Γ''' и '''Δ''' — конечные последовательности логических формул. | + | '''Секвенцией''' называется выражение вида '''Γ├ Δ''', где '''Γ''' и '''Δ''' — конечные последовательности логических формул. |
| − | Интуитивный смысл, закладываемый в секвенцию '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub> | + | Формула антецедента '''Γ={A<sub>1</sub>, A<sub>2</sub>,..., A<sub>m</sub>}''', формула сукцедента '''Δ={B<sub>1</sub>, B<sub>2</sub>,..., B<sub>n</sub>}'''. |
| + | |||
| + | Интуитивный смысл, закладываемый в секвенцию '''Γ├ Δ''' или '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>m</sub>├ B<sub>1</sub>, B<sub>2</sub>,..., B<sub>n</sub>''' — если выполнена конъюнкция формул антецедента '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>m</sub>''', то имеет место (выводится) дизъюнкция формул сукцедента '''B<sub>1</sub>, B<sub>2</sub>,..., B<sub>n</sub>'''. | ||
'''˄Ø''' — конъюнкция формул пустого множества — тождественно истинное высказывание; | '''˄Ø''' — конъюнкция формул пустого множества — тождественно истинное высказывание; | ||
| Строка 55: | Строка 57: | ||
'''├ ''' — секвенция с противоречивым выводом, которая имеет смысл '''˄Ø├ ˅Ø'''; | '''├ ''' — секвенция с противоречивым выводом, которая имеет смысл '''˄Ø├ ˅Ø'''; | ||
== Система LK == | == Система LK == | ||
| − | Система LK –– это классическое генценовское исчисление секвенций ( | + | Система LK –– это классическое генценовское исчисление секвенций (построенное Генценом в 1934 году). В системе LK одна аксиома и 21 правило вывода, которые делятся на структурные, логические и кванторные. |
Структурные правила (7) –– это правила '''WL, WR, CL, CR, C, PL, PR'''. | Структурные правила (7) –– это правила '''WL, WR, CL, CR, C, PL, PR'''. | ||
Логические правила (10) –– это правила '''¬L, ¬R, ˄L<sub>1</sub>, ˄L<sub>2</sub>, ˄R, ˅L, ˅R<sub>1</sub>, ˅R<sub>2</sub>, →L, →R'''. | Логические правила (10) –– это правила '''¬L, ¬R, ˄L<sub>1</sub>, ˄L<sub>2</sub>, ˄R, ˅L, ˅R<sub>1</sub>, ˅R<sub>2</sub>, →L, →R'''. | ||
| Строка 64: | Строка 66: | ||
[[файл: ИВ01.png]] | [[файл: ИВ01.png]] | ||
*Основные правила включают в себя структурные и логические. | *Основные правила включают в себя структурные и логические. | ||
| − | *Основные правила легко преобразуются в аналогичные с помощью перестановки | + | *Основные правила легко преобразуются в аналогичные (и наоборот) с помощью перестановки. |
=== Кванторные правила === | === Кванторные правила === | ||
[[файл: ИВ02.png]] | [[файл: ИВ02.png]] | ||
*Кванторные правила используют кванторы и формулы со свободной переменной или с термами. | *Кванторные правила используют кванторы и формулы со свободной переменной или с термами. | ||
*Кванторные правила для удобства применения представлены в двух вариантах. | *Кванторные правила для удобства применения представлены в двух вариантах. | ||
| − | === Пример | + | === Пример 1 === |
[[файл: ИВ10.png]] | [[файл: ИВ10.png]] | ||
*Приведён вывод закона исключённого третьего в системе LK. | *Приведён вывод закона исключённого третьего в системе LK. | ||
| + | === Пример 2 === | ||
| + | [[файл: ИВ20.png]] | ||
| + | *Приведён вывод с использованием кванторных правил в системе LK. | ||
== [[Логические понятия|Другие понятия:]] == | == [[Логические понятия|Другие понятия:]] == | ||
| − | {{Список | + | {{Список ЛП}} |
== Ссылки == | == Ссылки == | ||
*https://en.wikipedia.org/wiki/Sequent_calculus | *https://en.wikipedia.org/wiki/Sequent_calculus | ||
[[Категория:Математика]][[Категория:Дискретная математика]][[Категория:Логика]] | [[Категория:Математика]][[Категория:Дискретная математика]][[Категория:Логика]] | ||
Текущая версия на 08:03, 6 апреля 2025
Исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций). В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.
Содержание
Обозначения
A, B, C — одиночные формулы;
Γ, Г1, Г2 — списки формул антецедента, возможно пустые;
Δ, Δ1, Δ2 — списки формул сукцедента, возможно пустые;
A1, A2, …, Am — формулы списка антецедента;
B1, B2, …, Bn — формулы списка сукцедента;
F(x) — формула со свободной переменной;
F(t) — формула со значением терма вместо свободной переменной;
Ø — пустое множество формул;
├ — знак вывода;
L –– изменения слева –– изменения в антецеденте;
R –– изменения справа –– изменения в сукцеденте ;
W –– ослабление;
C –– сокращение;
P –– перестановка;
˄ –– конъюнкция;
˅ –– дизъюнкция;
¬ –– отрицание;
→ –– импликация;
Ɐ –– квантор всеобщности;
Ǝ –– квантор существования.
Определения
Секвенцией называется выражение вида Γ├ Δ, где Γ и Δ — конечные последовательности логических формул.
Формула антецедента Γ={A1, A2,..., Am}, формула сукцедента Δ={B1, B2,..., Bn}.
Интуитивный смысл, закладываемый в секвенцию Γ├ Δ или A1, A2,..., Am├ B1, B2,..., Bn — если выполнена конъюнкция формул антецедента A1, A2,..., Am, то имеет место (выводится) дизъюнкция формул сукцедента B1, B2,..., Bn.
˄Ø — конъюнкция формул пустого множества — тождественно истинное высказывание;
˅Ø — дизъюнкция формул пустого множества — тождественно ложное высказывание;
Γ├ — секвенция с противоречивым антецедентом, которая имеет смысл Γ├ ˅Ø;
├ Δ — секвенция подразумевает выполнимый сукцедент, которая имеет смысл ˄Ø├ Δ;
├ — секвенция с противоречивым выводом, которая имеет смысл ˄Ø├ ˅Ø;
Система 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.
Аксиома
~ аксиома
Основные правила
- Основные правила включают в себя структурные и логические.
- Основные правила легко преобразуются в аналогичные (и наоборот) с помощью перестановки.
Кванторные правила
- Кванторные правила используют кванторы и формулы со свободной переменной или с термами.
- Кванторные правила для удобства применения представлены в двух вариантах.
Пример 1
- Приведён вывод закона исключённого третьего в системе LK.
Пример 2
- Приведён вывод с использованием кванторных правил в системе LK.
