This thesis focuses on non-wellfounded proof theory. While these logics emerged more
recently than their wellfounded counterparts, they possess a rich theory and have numer-
ous applications in areas such as programming language theory and program verification.
This thesis contributes to the development of tools for the syntactic study of these log-
ics, with particular emphasis on cut-elimination. We provide a comprehensive study of
syntactic cut-elimination for non-wellfounded proof theory in linear logic and apply it to
complex logical systems.
We begin by reviewing, in a background chapter, basic notions of proof theory (both
wellfounded and non-wellfounded versions). We also provide brief introductions to lin-
ear logic and modal logic. Additionally, we present concepts from Gale-Stewart games
and Martin’s determinacy theorem, which we adapt to Gale-Stewart games over formula
occurrences in multiplicative and additive linear logic.
In the first part of this thesis, we show how to extend existing cut-elimination results
to linear logic with super exponentials, a system inspired by Nigam and Miller’s subex-
ponentials. We employ a simple translation into non-wellfounded linear logic, yielding a
modular approach that is readily adaptable to potential future extensions of these logics.
We apply this result to a linear version of the modal µ-calculus and derive a syntactic
cut-elimination result for Kozen’s non-wellfounded modal µ-calculus.
In the second part, we prove a convergence property for cut-reduction sequences in
the sliced system of multiplicative and additive linear logic, using a novel proof technique
that combines a proof-theoretic study of formula sequences in proofs, called threads, with
Martin’s determinacy theorem. This enables us to derive a simple characterization of
sequences converging to cut-free valid proofs. Finally, we demonstrate how to extend
these results to full linear logic and establish a new proof of strong normalization for
wellfounded linear logic.