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

В математике о том , гипотеза Такеути — это гипотеза Гаиси Такеути что секвентивная формализация логики второго порядка имеет исключение разреза (Takeuti 1953). Решение было принято положительно:

• Автор Тейт , использующий семантическую технику доказательства исключения отсечения, основанную на работе Шютте (Tait 1966);
• Независимо Правица (Prawitz 1968) и Такахаши (Takahashi 1967) по аналогичной методике (Takahashi 1967), хотя доказательства Правица и Такахаши не ограничиваются логикой второго порядка, а касаются логики высшего порядка в целом;
• Это следствие , предложенного Жаном-Ивом Жираром синтаксического доказательства сильной нормализации системы F .

Гипотеза Такеути эквивалентна 1-непротиворечивости арифметики второго порядка в том смысле, что каждое из утверждений может быть выведено друг из друга в слабой системе примитивно-рекурсивной арифметики (PRA) . Это также эквивалентно сильной нормализации Жирара/Рейнольда системы F .

См. также

• Вторая проблема Гильберта

Ссылки

• Даг Правиц , 1968. Hauptsatz логики высшего порядка. Журнал символической логики , 33:452–457, 1968.
• Уильям В. Тейт , 1966. Неконструктивное доказательство хауптзаца Генцена для логики предикатов второго порядка. В Бюллетене Американского математического общества , 72:980–983.
• Гаиси Такеути , 1953. Об обобщенном логическом исчислении. В Японском математическом журнале , 23:39–96. Опечатки к этой статье были опубликованы в том же журнале, 24:149–156, 1954 г.
• Мото-о Такахаши, 1967. Доказательство исключения разреза в простой теории типов. В Японском математическом обществе , 10:44–45.