Computation by infinite descent made explicit
Abstract
We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the computational content of this system, in particular we introduce a notion of computability and show that every valid proof is computable. As a consequence, we obtain a normalization result for proofs of what we call finitary formulas. A special case of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.
Cite
@article{arxiv.2506.22206,
title = {Computation by infinite descent made explicit},
author = {Sebastian Enqvist},
journal= {arXiv preprint arXiv:2506.22206},
year = {2026}
}