Введение

Хорошо квази-порядок конечных деревьев
В математике теорема Крускала о деревьях утверждает, что множество конечных деревьев над хорошо квазиупорядоченным множеством меток само по себе хорошо квазиупорядочено относительно гомеоморфного вложения.

История

Теорема была сформулирована Эндрю Вазони и доказана ; короткое доказательство было предложено в . С тех пор она стала известным примером в обратной математике как утверждение, которое нельзя доказать в ATR0 (арифметическая теория второго порядка с формой арифметической трансфинитной рекурсии). В 2004 году результат был обобщен с деревьев на графы в теорему Робертсона — Сеймура, которая также оказалась важной в обратной математике и приводит к еще более быстрорастущей функции SSCG, значительно превосходящей A. Конечное применение теоремы гарантирует существование быстрорастущей функции TREE.

Работа Фридмана

Для счётного множества меток X, теорему Крускаля о деревьях можно сформулировать и доказать с помощью арифметики второго порядка. Однако, подобно теореме Гудштейна или теореме Пари-Харрингтона, некоторые частные случаи и варианты этой теоремы могут быть выражены в подсистемах арифметики второго порядка, значительно более слабых, чем те, в которых они могут быть доказаны. Это было впервые отмечено Харви Фридманом в начале 1980-х годов, что стало одним из первых успехов тогда только зарождающейся области обратной математики. В случае, когда рассматриваемые деревья немаркированы (то есть, когда множество X имеет размер один), Фридман показал, что результат недоказуем в ATR0, предоставив тем самым первый пример предикативного утверждения с доказуемо непредсказуемым доказательством. Этот частный случай теоремы всё ещё доказуем в Π CA0, но, добавив "условие разрыва" к определению порядка на деревьях, он нашёл естественную вариацию теоремы, которая недоказуема в этой системе. Значительно позже теорема Робертсона — Сеймура предоставила ещё одну теорему, недоказуемую в Π CA0. Ординальный анализ подтверждает силу теоремы Крускаля, теоретический ординал которой равен малому ординалу Веблена (иногда путают с меньшим ординалом Аккермана).

Функция TREE

Включая метки, Фридман определил гораздо более быстрорастущую функцию. Для положительного целого числа *n*, обозначим через *TREE(n)* наибольшее целое число *m*, такое что выполняется следующее:

Существует последовательность T1, T2, ..., Tm корневых деревьев, помеченных из набора из *n* меток, где каждое Ti имеет не более *i* вершин, причем условие *TREE(n-1)* не выполняется для любого *i*.

Последовательность TREE начинается с 1, 2, затем внезапно "взрывается" до значения, настолько огромного, что многие другие "большие" комбинаторные константы, такие как число Фридмана, число Кона и число Грэма, оказываются чрезвычайно малыми по сравнению с ним. Нижняя граница для *TREE(n)*, а следовательно, и крайне слабая нижняя граница для *TREE(n+1)*, – это число Грэма, например, которое намного меньше нижней границы *TREE(TREE(…(TREE(4)))* (где количество TREE равно 64), которая приблизительно равна G(G(…(G(4)))), где G – функция Грэма.