Замыкающий ординал оператора непосредственной выводимости в инфинитарной логике действий

В работе доказывается, что замыкающий ординал оператора непосредственной выводимости в инфинитарной логике действий равен $\omega^\omega$; тем самым дан ответ на открытый вопрос из статьи (С. Л. Кузнецов, С. О. Сперанский, 2022) о нахождении точного значения этой теоретико-доказательственной характеристики. Также в работе доказывается, что замыкающий ординал для коммутативной инфинитарной логики действий равен $\omega^\omega$. Оба результата устанавливаются путем предъявления семейства секвенций, ранги которых стремятся к $\omega^\omega$. Для доказательства результатов разрабатываются техники анализа выводов секвенций в инфинитарной логике действий. В случае коммутативной инфинитарной логики действий используется техника проверки на нуль, аналогичная примененной в статье (С. Л. Кузнецов, 2022). Показано, что в присутствии правила сечения ранги секвенций, построенных для инфинитарной логики действий, значительно уменьшаются, так что их супремум не превосходит $\omega^2$.
Библиография: 4 названия.