Closure ordinal of immediate derivability operator of infinitary action logic

T. G. Pshenitsyn

Matematičeskie zametki, Tome 116 (2024) no. 4, pp. 559-577

Résumé

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$.

Détail

Keywords: closure ordinal, action logic, substructural logic, cut rule.

Bibliographie

[1] E. Palka, “An infinitary sequent system for the equational theory of $*$-continuous action lattices”, Fund. Inform., 78:2 (2007), 295–309 | MR

[2] S. L. Kuznetsov, S. O. Speranski, “Infinitary action logic with multiplexing”, Studia Logica, 111:2 (2023), 251–280 | DOI | MR

[3] S. L. Kuznetsov, S. O. Speranski, “Infinitary action logic with exponentiation”, Ann. Pure Appl. Logic, 173:2 (2022), 103057 | DOI | MR

[4] S. L. Kuznetsov, “Commutative action logic”, J. Logic Comput., 33:6 (2022), 1437–1462 | DOI | MR