Closure Ordinal of Immediate Derivability Operator of Infinitary Action Logic

We prove that the closure ordinal of the immediate derivability operator of infinitary action logic equals $$\omega^\omega$$ . We thus answer an open question from the article (Kuznetsov, Speranski 2022), which is to find the exact value of this proof-theoretic characteristic. We also prove that the closure ordinal of commutative infinitary action logic equals $$\omega^\omega$$ . Both results are established by constructing a series of sequents whose ranks tend to $$\omega^\omega$$ . To prove the results, we develop methods to analyze sequent derivations in infinitary action logic. In the case of commutative action logic, we use a zero-test techinque similar to that from (Kuznetsov, 2022). We show that ranks of the sequents constructed for infinitary axtion logic significantly decrease in presence of the cut rule so their supremum is not greater than $$\omega^2$$ .