Устранение сечений: теорема Гентцена и подформульное свойство

В 1934 году Герхард Гентцен доказал, что любое математическое доказательство можно переписать так, что оно никогда не 'изобретает' новые понятия - все используемые формулы содержатся в доказываемом утверждении. Это Hauptsatz ('главная теорема'). Из неё следует непротиворечивость арифметики Пеано.

• Proof assistants Coq и Lean используют соответствие Карри-Говарда: устранение сечений = нормализация программ. Microsoft Research использует Lean 4 для верификации математики и промышленного кода - и за этим стоит теорема Гентцена 1934 года.

Секвенциальное исчисление LK

Герхард Гентцен в 1934 году ввёл секвенциальное исчисление LK и доказал теорему Hauptsatz (устранение сечений). LK строит доказательства секвенций Gamma => Delta (если все формулы в Gamma истинны, то хотя бы одна в Delta истинна). Правило сечения (cut) вводит 'леммы', но делает анализ доказательств нетривиальным. Устранение сечений восстанавливает аналитичность: все формулы в доказательстве являются подформулами доказываемой.

Следствия устранения сечений

Из теоремы Гентцена следуют: непротиворечивость PA (через ординальный анализ с epsilon_0), теорема интерполяции Крейга (1957), теорема о консерватизме расширений. В компьютерной науке Cut elimination обеспечивает нормализацию в просто типизированном лямбда-исчислении (соответствие Карри-Говарда).

Ключевые результаты

• LK = секвенциальное исчисление. Правило Cut вводит 'леммы'.
• Hauptsatz Гентцена: cut-free доказательство существует для любой теоремы LK.
• Подформульное свойство: cut-free доказательство аналитично.
• Curry-Howard: Cut = бета-редекс, cut elimination = нормализация лямбда-термов.