Специальное исчисление высказываний — различия между версиями

Версия 09:05, 4 апреля 2025

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

Обозначения

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

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

A, B, C — формулs сукцедента, возможно пустые;

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

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

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

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

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

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

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

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

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

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

Определения

Секвенции (латинское sequentia — последовательность, следствие) — это выражения вида A₁, A₂,..., A_m |- B₁, B₂,..., B_n, где |- — знак выводимости, A₁, A₂,..., A_m и B₂,..., B_n — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).

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

Дополнительные правила

Примеры

Доказательства секвенций

Доказательства некоторых дополнительных правил:

Правило_в

Правило_д

Правило_е

Правило_ж

Правило_з

Правило_и

Правило_к

Правило_л

Правило_м

Правило_н

Правило_о

Правило_п

Другие понятия:

Ссылки

Генцен Г. Исследования логических выводов. В кн. Математическая теория логического вывода, М, 1967, с. 9—74.
Участник:Logic-samara

@@ Строка 1: / Строка 1: @@
 '''Специальное исчисление высказываний (секвенций)''' — построение логической последовательности условных суждений (секвенций) по определённым правилам. В секвенциальном подходе используется аксиома и правила вывода, а доказательство ведётся в форме дерева вывода. Исчисления секвенций относятся к генценовскому типу.
+== Обозначения ==
+'''A, B, C''' — одиночные формулы;
+'''Γ, Г<sub>1</sub>, Г<sub>2</sub>''' — списки формул антецедента, возможно пустые;
+'''A, B, C''' — формулs сукцедента, возможно пустые;
+'''A<sub>1</sub>, A<sub>2</sub>, …, A<sub>n</sub>''' — формулы списка антецедента;
+'''B<sub>1</sub>, B<sub>2</sub>, …, B<sub>m</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>''' — произвольные формулы; первые — образующие '''антецедент''' секвенции, вторые — её '''сукцедент'''.
@@ Строка 5: / Строка 32: @@
 == Основные правила ==
 [[файл:СЕК12.JPG]]
+[[файл:СИВ01.png]]
 == Дополнительные правила ==
 [[файл:СЕК13.JPG]]
+[[файл:СИВ02.png]]
+== Примеры ==
 [[файл:СЕК14.JPG]]
 == Доказательства секвенций ==