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.

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