Linear logic with approximations of fixed-point operators

Fixed points can be incorporated into linear logic in several ways, leading to proof systems with explicit (co)induction rules, cyclic or non-well-founded proofs, or infinitely branching inference rules. The setting of linear logic allows to compare these methodologies in a robust way, largely free from artefacts of, say, classical or intuitionistic logic, or first-order theories, such as arithmetic. The least fixed point of a monotone operator $F\colon S \to S$ in a complete lattice can be obtained by transfinitely iterating $F$ starting with the least element of the lattice. This gives rise to the notion of the $\alpha$-th approximation of the least fixed point of $F$. Such approximations can be axiomatized using infinitary rules. We study an extension of multiplicative-additive linear logic with $\alpha$-th approximations of fixed points and determine the exact complexity of its provability problem in the hyperarithmetical hierarchy, showing its $\Sigma^0_{\omega^{\alpha^\omega}}$-completeness. To establish this result, we develop the corresponding proof-theoretic machinery, including cut-elimination, focusing, and a theory of formula ranks. The talk is based on the joint work with Anupam Das.