Секвенции

Материал из Мегапедии
Перейти к: навигация, поиск

Секвенции (латинское 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