Interested Article - Гипотеза Такеути
melania
- 2020-06-21
- 1
Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной ( яп. ; 1926—2017) в 1953 году . Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам , непротиворечивости и полноты для широкого класса логик высших порядков , по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка .
Первым шагом к подтверждению гипотезы стало доказательство ( англ. ; род. 1929) устранимости сечений в логике второго порядка в 1966 году . В 1967 году результат был обобщён в работах и ( швед. ; род. 1936), тем самым, гипотеза полностью подтверждена.
Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, Драгалин установил устранимость сечений для серии неклассических логик высших порядков, а ( фр. ) — для системы F .
Примечания
- , с. 188—195.
- 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 .
- Takahashi M. // Journal of Japanese Mathematical Society. — 1967. — Т. 19 , № 4 . — С. 399—410 . — doi : . 21 января 2019 года.
Литература
- Takeuti G. On a generalized logic calculus (англ.) // Japanese Journal of Mathematics. — Vol. 23 . — P. 39—96 .
- Такеути Г. Теория доказательств. — М. : Мир, 1978. — 412 с.
melania
- 2020-06-21
- 1
