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

Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной Гаиси Такеути (яп. 竹内外史; 1926—2017) в 1953 году[1]. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам корректности, непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка.

Первым шагом к подтверждению гипотезы стало доказательство Тэйтом (англ. William W. Tait; род. 1929) устранимости сечений в логике второго порядка в 1966 году[2]. В 1967 году результат был обобщён в работах Такахаси[3] и Правица (швед. Dag Prawitz; род. 1936), тем самым, гипотеза полностью подтверждена.

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

Примечания
  1. Такеути, 1978, с. 188—195.
  2. Tait W. W. A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic (англ.) // Bulletin of the American Mathematical Society. — 1966. — Vol. 72. — P. 980—983.
  3. Takahashi M. A proof of cut-elimination theorem in simple type-theory // Journal of Japanese Mathematical Society. — 1967. — Т. 19, № 4. — С. 399—410. — doi:10.2969/jmsj/01940399.

Литература
  • Takeuti G. On a generalized logic calculus (англ.) // Japanese Journal of Mathematics. — Vol. 23. — P. 39—96.
  • Такеути Г. Теория доказательств. — М.: Мир, 1978. — 412 с.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.