We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal $α$ for fixed points. Our main result is that provability in the system for some computable ordinal $α$ is complete for the $ω^{α^ω}$ level of the hyperarithmetical hierarchy. To this end we first develop proof theoretic foundations, namely cut elimination and focussing results, to control both the upper and lower bound analysis. Our arguments employ a carefully calibrated notion of formula rank, calculating a tight bound on the height of the (cut-free) proof search space.

翻译：我们研究了带不动点的线性逻辑的无穷良基系统，其具有由不动点的某个闭序数$α$索引的超限分支规则。我们的主要结果表明，对于某个可计算序数$α$，该系统中的可证性对于超算术层级中$ω^{α^ω}$层级是完全的。为此，我们首先发展了证明论基础，即消去切割和聚焦结果，以控制上界和下界分析。我们的论证采用了一种精心校准的公式秩概念，计算了（无切割）证明搜索空间高度的紧致上界。