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

Материал из Мегапедии
Перейти к: навигация, поиск
м
м
Строка 69: Строка 69:
 
[[файл:СЕК30о.JPG]]
 
[[файл:СЕК30о.JPG]]
 
[[файл:СИВ31.png]]
 
[[файл:СИВ31.png]]
=== '''Правило_п''' ===
+
=== '''Пример_п''' ===
 
[[файл:СЕК30п.JPG]]
 
[[файл:СЕК30п.JPG]]
 
[[файл:СИВ32.png]]
 
[[файл:СИВ32.png]]

Версия 11:55, 4 апреля 2025

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

Обозначения

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

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

A1, A2, …, An — формулы списка антецедента;

B1, B2, …, Bm — формулы списка антецедента;

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

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

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

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

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

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

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

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

Определения

Секвенции (латинское sequentia — последовательность, следствие) — это выражения вида A1, A2,..., Am |- B1, B2,..., Bn, где |- — знак выводимости, A1, A2,..., Am и B2,..., Bn — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).

Аксиома

ИВ00.png ~ аксиома

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

СИВ01.png

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

СИВ02.png

Примеры

СЕК13.JPG

СЕК14.JPG

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

Пример_в

СИВ21.png

Пример_д

СИВ22.png

Пример_е

СИВ23.png

Пример_ж

СЕК30ж.JPG СИВ24.png

Пример_з

СЕК30з.JPG

Пример_и

СЕК30и.JPG

Пример_к

СЕК30к.JPG

Пример_л

СЕК30л.JPG

Пример_м

СЕК30м.JPG

Пример_н

СЕК30н.JPG

Пример_о

СЕК30о.JPG СИВ31.png

Пример_п

СЕК30п.JPG СИВ32.png

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

Ссылки

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