Изменения
'''Секвенции''' (латинское sequentia — последовательность, следствие) — это выражения вида '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>m</sub> |- B<sub>1</sub>, B<sub>2</sub>,..., B<sub>n</sub>''', где '''|-''' — знак выводимости, '''A<sub>1</sub>, A<sub>2</sub>,..., A<sub>m</sub>''' и '''B<sub>2</sub>,..., B<sub>n</sub>''' — произвольные формулы; первые — образующие '''антецедент''' секвенции, вторые — её '''сукцедент'''.
Такого рода выражения изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать).
== Основные правила ==
[[файл:СЕК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]] [[Категория:Математика]][[Категория:Дискретная математика]][[Категория:Логика]]
