Сечение в теории доказательств — правило вывода , позволяющее удалить («высечь») промежуточное высказывание ${\displaystyle A}$ :

${\displaystyle {\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \Lambda }}}$ .

Поскольку правило сечения не обладает (требующим, чтобы посылки состояли из подформул заключения), особую значимость (в том числе для возможности конструктивного доказательства их непротиворечивости ) приобретают логические исчисления с устранимостью сечений , то есть такие, в которых всякую выводимую секвенцию можно вывести без сечения. Для классического и интуиционистского исчислений секвенций свойство доказано Генценом , в дальнейшем оно установлено для большой серии классических и неклассических теорий высших порядков.

Литература

• Г. Такеути. Теория доказательств. — М. : Мир, 1978. — 412 с.
• Подформульности свойство — статья из Математической энциклопедии . С. Ю. Маслов