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

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

Версия 11:54, 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