Гипотеза Такеути

Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной Гаиси Такеути в 1953 году^[1]. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам корректности, непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка.

Первым шагом к подтверждению гипотезы стало доказательство Тэйтом устранимости сечений в логике второго порядка в 1966 году^[2]. В 1967 году результат был обобщён в работах Такахаси^[3] и Правица, тем самым, гипотеза полностью подтверждена.

Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, Драгалин установил устранимость сечений для серии неклассических логик высших порядков, а Жирар — для системы F.