Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm

TL;DR

This paper advances the understanding of cut elimination in ill-founded proof systems by applying reducibility candidates to ensure the preservation of progressivity in infinitary logic with fixed-points.

Contribution

It introduces two cut elimination methods for ill-founded $$ logic using reducibility candidates, addressing a key challenge in non-wellfounded proof theory.

Findings

Both methods preserve progressivity during cut elimination.

The second method employs a topological notion of internally closed sets.

The techniques are based on the reducibility candidates framework of Tait and Girard.

Abstract

Ill-founded (or non-wellfounded) proof systems have emerged as a natural framework for inductive and coinductive reasoning. In such systems, soundness relies on global correctness criteria, such as the progressivity condition. Ensuring that these criteria are preserved under infinitary cut elimination remains a central technical challenge in ill-founded proof theory. In this paper, we present two cut elimination arguments for ill-founded $\mu \mathsf{MALL}$ - a fragment of linear logic extended with fixed-points - based on the reducibility candidates technique of Tait and Girard. In both arguments, preservation of progressivity follows directly from the defining properties of the reducibility candidates. In particular, the second argument is derived from the topological notion of internally closed set developed in previous work by Afshari and Leigh.