Устранимость сечений

Устранимость сечений (теорема Генцена, элиминационная теорема) — свойство логических исчислений, согласно которому всякую секвенцию, выводимую в данном исчислении, можно вывести без применения правила сечений^[1]. Играет фундаментальную роль в теории доказательств и важную методологическую роль в математической логике в целом в связи с тем, что предоставляет конструктивный метод доказательства непротиворечивости, в частности, для классической и интуиционистской логик первого порядка^[2].

Для классического и интуиционистского исчислений секвенций свойство доказано Генценом в 1934 году. В 1953 году высказана гипотеза Такеути, согласно которой устранимость сечений имеет место для простой теории типов и соответствующих ей логик высших порядков, впоследствии она нашла подтверждение — для классической логики второго порядка устранимость сечений доказал Тейт^[англ.], для простой теории типов — Такахаси и Правица^[швед.], вскоре найдены доказательства для серии неклассических теорий высших порядков (Драгалин) и развитых теорий типов (Жирар^[англ.] для системы F).

Символическая формулировка: пусть ${\displaystyle \Gamma \vdash \Theta ,\Phi }$ и ${\displaystyle \Phi ,\Lambda \vdash \Delta }$ — доказуемые секвенции исчисления ${\displaystyle G}$; если ${\displaystyle \Gamma ,\Lambda \vdash \Delta ,\Theta }$ — секвенция исчисления ${\displaystyle G}$, то она доказуема^[3].