Секвенции

Материал из ALL
Версия от 15:05, 15 ноября 2015; Ws (обсуждение | вклад) (Восстановление статей Logic-samara)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Определение

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

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

СЕК12.JPG

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

СЕК13.JPG СЕК14.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

Ссылки

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