Гипотеза Такейтиса - Википедия - Takeutis conjecture

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

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

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

Смотрите также

Рекомендации

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