Computation by infinite descent made explicit
This work provides a foundational framework for computational content in non-wellfounded proofs, relevant to logicians and computer scientists studying proof theory and categorical semantics.
The authors introduce a non-wellfounded proof system for intuitionistic logic with inductive and co-inductive definitions, using ordinal-annotated fixpoint formulas. They prove that every valid proof is computable, yielding normalization for finitary formulas and a unique function representation for proofs of certain sequents.
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.