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

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

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

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

Литература

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