Гипотеза Такеути: различия между версиями
Перейти к навигации
Перейти к поиску
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
MagnusFit (обсуждение | вклад) Нет описания правки |
Спасено источников — 1, отмечено мёртвыми — 0. Сообщить об ошибке. См. FAQ.) #IABot (v2.0.9.2 |
||
| Строка 1: | Строка 1: | ||
'''Гипотеза Такеути''' — утверждение об [[Устранимость сечений|устранимости сечений]] в [[Исчисление секвенций|исчислении секвенций]] для простой теории типов, построенной {{нп2|Такеути, Гаиси|Гаиси Такеути|ja|竹内外史|text=1926—2017}} в 1953 году{{sfn|Такеути|1978|с=188—195}}. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам [[корректность (логика)|корректности]], [[Непротиворечивость|непротиворечивости]] и [[Полная теория|полноты]] для широкого класса [[Логика высшего порядка|логик высших порядков]], по аналогии с результатом [[Генцен, Герхард|Генцена]] 1934 года для классического и интуиционистского [[Исчисление предикатов|исчислений предикатов]] [[Логика первого порядка|первого порядка]]. |
'''Гипотеза Такеути''' — утверждение об [[Устранимость сечений|устранимости сечений]] в [[Исчисление секвенций|исчислении секвенций]] для простой теории типов, построенной {{нп2|Такеути, Гаиси|Гаиси Такеути|ja|竹内外史|text=1926—2017}} в 1953 году{{sfn|Такеути|1978|с=188—195}}. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам [[корректность (логика)|корректности]], [[Непротиворечивость|непротиворечивости]] и [[Полная теория|полноты]] для широкого класса [[Логика высшего порядка|логик высших порядков]], по аналогии с результатом [[Генцен, Герхард|Генцена]] 1934 года для классического и интуиционистского [[Исчисление предикатов|исчислений предикатов]] [[Логика первого порядка|первого порядка]]. |
||
Первым шагом к подтверждению гипотезы стало доказательство {{нп2|Тэйт, Уильям|Тэйтом|en|William W. Tait|text=род. 1929}} устранимости сечений в [[Логика второго порядка|логике второго порядка]] в [[1966 год в науке|1966 году]]<ref>{{статья | автор = Tait W. W. | заглавие = A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic | издание = Bulletin of the American Mathematical Society | том = 72 | год = 1966 | страницы =980—983 | язык = en }}</ref>. В [[1967 год в науке|1967 году]] результат был обобщён в работах [[Такахаси, Мотоо|Такахаси]]<ref>{{статья | автор = Takahashi M. | заглавие = |
Первым шагом к подтверждению гипотезы стало доказательство {{нп2|Тэйт, Уильям|Тэйтом|en|William W. Tait|text=род. 1929}} устранимости сечений в [[Логика второго порядка|логике второго порядка]] в [[1966 год в науке|1966 году]]<ref>{{статья | автор = Tait W. W. | заглавие = A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic | издание = Bulletin of the American Mathematical Society | том = 72 | год = 1966 | страницы =980—983 | язык = en }}</ref>. В [[1967 год в науке|1967 году]] результат был обобщён в работах [[Такахаси, Мотоо|Такахаси]]<ref>{{статья | автор = Takahashi M. | заглавие = A proof of cut-elimination theorem in simple type-theory | издание = Journal of Japanese Mathematical Society | том = 19 | номер = 4 | год = 1967 | страницы = 399—410 | ссылка = https://projecteuclid.org/euclid.jmsj/1260478312 | doi = 10.2969/jmsj/01940399 | archivedate = 2019-01-21 | archiveurl = https://web.archive.org/web/20190121064307/https://projecteuclid.org/euclid.jmsj/1260478312 }}</ref> и {{нп2|Правиц, Даг|Правица|sv|Dag Prawitz|text=род. 1936}}, тем самым, гипотеза полностью подтверждена. |
||
Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, [[Драгалин, Альберт Григорьевич|Драгалин]] установил устранимость сечений для серии неклассических логик высших порядков, а {{нп2|Жирар, Жан-Ив|Жирар|fr|Jean-Yves Girard}} — для [[Система F|системы F]]. |
Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, [[Драгалин, Альберт Григорьевич|Драгалин]] установил устранимость сечений для серии неклассических логик высших порядков, а {{нп2|Жирар, Жан-Ив|Жирар|fr|Jean-Yves Girard}} — для [[Система F|системы F]]. |
||
Текущая версия от 11:39, 17 декабря 2022
Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной Гаиси Такеути (яп. 竹内外史; 1926—2017) в 1953 году[1]. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам корректности, непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка.
Первым шагом к подтверждению гипотезы стало доказательство Тэйтом (англ. William W. Tait; род. 1929) устранимости сечений в логике второго порядка в 1966 году[2]. В 1967 году результат был обобщён в работах Такахаси[3] и Правица (швед. Dag Prawitz; род. 1936), тем самым, гипотеза полностью подтверждена.
Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, Драгалин установил устранимость сечений для серии неклассических логик высших порядков, а Жирар (фр. Jean-Yves Girard) — для системы F.
Примечания
[править | править код]- ↑ Такеути, 1978, с. 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. 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. Архивировано 21 января 2019 года.
Литература
[править | править код]- Takeuti G. On a generalized logic calculus (англ.) // Japanese Journal of Mathematics. — Vol. 23. — P. 39—96.
- Такеути Г. Теория доказательств. — М.: Мир, 1978. — 412 с.