Специальное исчисление высказываний — различия между версиями
м |
|||
| (не показаны 23 промежуточные версии этого же участника) | |||
| Строка 1: | Строка 1: | ||
| + | '''Специальное исчисление высказываний (секвенций)''' — построение логической последовательности условных суждений (секвенций) по определённым правилам. В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу. | ||
| + | == Обозначения == | ||
| + | '''A, B, C''' — одиночные формулы; | ||
| + | |||
| + | '''Γ, Г<sub>1</sub>, Г<sub>2</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>''' — формулы списка антецедента; | ||
| + | |||
| + | '''Ø''' — пустое множество формул; | ||
| + | |||
| + | '''├''' — знак вывода; | ||
| + | |||
| + | '''W''' –– ослабление; | ||
| + | |||
| + | '''P''' –– перестановка; | ||
| + | |||
| + | '''˄''' –– конъюнкция; | ||
| + | |||
| + | '''˅''' –– дизъюнкция; | ||
| + | |||
| + | '''¬''' –– отрицание; | ||
| + | |||
| + | '''→''' –– импликация. | ||
| + | == Определения == | ||
'''Секвенции''' (латинское sequentia — последовательность, следствие) — это выражения вида '''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>2</sub>,..., B<sub>n</sub>''' — произвольные формулы; первые — образующие '''антецедент''' секвенции, вторые — её '''сукцедент'''. | '''Секвенции''' (латинское sequentia — последовательность, следствие) — это выражения вида '''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>2</sub>,..., B<sub>n</sub>''' — произвольные формулы; первые — образующие '''антецедент''' секвенции, вторые — её '''сукцедент'''. | ||
Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать). | Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать). | ||
| + | == Аксиома == | ||
| + | [[файл:ИВ00.png]] ~ аксиома | ||
== Основные правила == | == Основные правила == | ||
| − | [[файл:СЕК12.JPG]] | + | <!--[[файл:СЕК12.JPG]]--> |
| + | [[файл:СИВ01.png]] | ||
== Дополнительные правила == | == Дополнительные правила == | ||
| − | [[файл:СЕК13.JPG]] | + | [[файл:СИВ02.png]] |
| − | [[файл:СЕК14.JPG]] | + | == Примеры секвенций == |
| + | <!--[[файл:СЕК13.JPG]][[файл:СЕК14.JPG]]--> | ||
| + | [[файл:СИВ10.png]] | ||
== Доказательства секвенций == | == Доказательства секвенций == | ||
| − | + | === '''Пример_в''' === | |
| − | === ''' | + | <!--[[файл:СЕК30в.JPG]]--> |
| − | [[файл:СЕК30в.JPG]] | + | [[файл:СИВ21.png]] |
| − | === ''' | + | === '''Пример_д''' === |
| − | [[файл:СЕК30д.JPG]] | + | <!--[[файл:СЕК30д.JPG]]--> |
| − | === ''' | + | [[файл:СИВ22.png]] |
| − | [[файл:СЕК30е.JPG]] | + | === '''Пример_е''' === |
| − | === ''' | + | <!--[[файл:СЕК30е.JPG]]--> |
| + | [[файл:СИВ23.png]] | ||
| + | <!--=== '''Пример_ж''' === | ||
[[файл:СЕК30ж.JPG]] | [[файл:СЕК30ж.JPG]] | ||
| − | === ''' | + | [[файл:СИВ24.png]]--> |
| − | [[файл:СЕК30з.JPG]] | + | === '''Пример_з''' === |
| − | === ''' | + | <!--[[файл:СЕК30з.JPG]]--> |
| + | [[файл:СИВ25.png]] | ||
| + | <!--=== '''Пример_и''' === | ||
[[файл:СЕК30и.JPG]] | [[файл:СЕК30и.JPG]] | ||
| − | === ''' | + | [[файл:СИВ26.png]]--> |
| − | [[файл:СЕК30к.JPG]] | + | === '''Пример_к''' === |
| − | === ''' | + | <!--[[файл:СЕК30к.JPG]]--> |
| − | [[файл:СЕК30л.JPG]] | + | [[файл:СИВ27.png]] |
| − | === ''' | + | === '''Пример_л''' === |
| + | <!--[[файл:СЕК30л.JPG]]--> | ||
| + | [[файл:СИВ28.png]] | ||
| + | <!--=== '''Пример_м''' === | ||
[[файл:СЕК30м.JPG]] | [[файл:СЕК30м.JPG]] | ||
| − | === ''' | + | [[файл:СИВ29.png]]--> |
| + | <!--=== '''Пример_н''' === | ||
[[файл:СЕК30н.JPG]] | [[файл:СЕК30н.JPG]] | ||
| − | === ''' | + | [[файл:СИВ30.png]]--> |
| − | [[файл:СЕК30о.JPG]] | + | === '''Пример_о''' === |
| − | === ''' | + | <!--[[файл:СЕК30о.JPG]]--> |
| − | [[файл:СЕК30п.JPG]] | + | [[файл:СИВ31.png]] |
| + | === '''Пример_п''' === | ||
| + | <!--[[файл:СЕК30п.JPG]]--> | ||
| + | [[файл:СИВ32.png]] | ||
== [[Логические понятия|Другие понятия:]] == | == [[Логические понятия|Другие понятия:]] == | ||
{{Список ЛП}} | {{Список ЛП}} | ||
Текущая версия на 16:44, 5 апреля 2025
Специальное исчисление высказываний (секвенций) — построение логической последовательности условных суждений (секвенций) по определённым правилам. В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.
Содержание
Обозначения[править]
A, B, C — одиночные формулы;
Γ, Г1, Г2 — списки формул антецедента, возможно пустые;
A1, A2, …, Am — формулы списка антецедента;
B1, B2, …, Bn — формулы списка антецедента;
Ø — пустое множество формул;
├ — знак вывода;
W –– ослабление;
P –– перестановка;
˄ –– конъюнкция;
˅ –– дизъюнкция;
¬ –– отрицание;
→ –– импликация.
Определения[править]
Секвенции (латинское sequentia — последовательность, следствие) — это выражения вида A1, A2,..., Am |- B1, B2,..., Bn, где |- — знак выводимости, A1, A2,..., Am и B2,..., Bn — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).
Аксиома[править]
~ аксиома
Основные правила[править]
Дополнительные правила[править]
Примеры секвенций[править]
Доказательства секвенций[править]
Пример_в[править]
Пример_д[править]
Пример_е[править]
Пример_з[править]
Пример_к[править]
Пример_л[править]
Пример_о[править]
Пример_п[править]
Другие понятия:[править]
Ссылки[править]
- Генцен Г. Исследования логических выводов. В кн. Математическая теория логического вывода, М, 1967, с. 9—74.
- Участник:Logic-samara
