Infinitary proof theory : the multiplicative additive case

Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediatedevices between semantics and traditional finitary proof systems, they are commonly found incompleteness arguments, automated deduction, verification, etc. However, their proof theoryis surprisingly underdeveloped. In particular, very little is known about the computationalbehavior of such proofs through cut elimination. Taking such aspects into account has unlockedrich developments at the intersection of proof theory and programming language theory. Onewould hope that extending this to infinitary calculi would lead, e.g., to a better understanding ofrecursion and corecursion in programming languages. Structural proof theory is notably basedon two fundamental properties of a proof system: cut elimination and focalization. The firstone is only known to hold for restricted (purely additive) infinitary calculi, thanks to the workof Santocanale and Fortier; the second one has never been studied in infinitary systems. Inthis paper, we consider the infinitary proof system μMALL ∞ for multiplicative and additivelinear logic extended with least and greatest fixed points, and prove these two key results. Wethus establish μMALL ∞ as a satisfying computational proof system in itself, rather than just anintermediate device in the study of finitary proof systems