Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной Гаиси Такеути (яп. 竹内外史; 1926—2017) в 1953 году[1]. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам корректности, непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом для классического и интуиционистского исчислений предикатов первого порядка, установленного Генценом в 1934 году.
Первым шагом к подтверждению гипотезы стало доказательство Тэйтом (англ. William W. Tait; род. 1929) устранимости сечений в логике второго порядка в 1966 году[2]. В 1967 году результат был обобщён в работах Такахаси[3] и Правица (швед. Dag Prawitz; род. 1936), тем самым, гипотеза полностью подтверждена.
Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, Драгалин установил устранимость сечений для серии неклассических логик высших порядков, а Жирар[fr] — для системы F.
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .