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

Версия 14:47, 4 апреля 2025

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

Обозначения

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

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

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

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

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

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

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

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

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

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

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

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

Определения

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

Аксиома

~ аксиома

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

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

Примеры секвенций

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

Пример_в

Пример_д

Пример_е

Пример_ж

Пример_з

Пример_и

Файл:СИВ26.png

Пример_к

Пример_л

Пример_м

Файл:СИВ29.png

Пример_н

Файл:СИВ30.png

Пример_о

Пример_п

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

Ссылки

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

@@ Строка 5: / Строка 5: @@
 '''Γ, Г<sub>1</sub>, Г<sub>2</sub>''' — списки формул антецедента, возможно пустые;
-'''A<sub>1</sub>, A<sub>2</sub>, …, A<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>m</sub>''' — формулы списка антецедента;
+'''B<sub>1</sub>, B<sub>2</sub>, …, B<sub>n</sub>''' — формулы списка антецедента;
 '''Ø''' — пустое множество формул;