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

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

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

Примечания

Литература

• G. Gentzen. Untersuchungen über das logische Schließen (нем.) // Mathematische Zeitschrift. — 1934–1935. — Bd. 39 . — S. 405–431 . — doi : .
• Такеути Г. Теория доказательств. — М. : Мир, 1978. — 412 с.
• Ершов Ю. Л. , Палютин Е. А. Математическая логика. — М. : Наука, 1987. — 336 с.