Computation by infinite descent made explicit

TL;DR

This paper presents a non-wellfounded proof system for intuitionistic logic with inductive and co-inductive definitions, establishing computability, normalization, and categorical models with explicit fixpoint annotations.

Contribution

It introduces a novel proof system with explicit ordinal annotations, demonstrating its computational content, normalization, and categorical semantics.

Findings

Every valid proof in the system is computable.

Proofs of certain sequents correspond to unique functions on natural numbers.

A categorical model links fixpoint formulas to initial algebras and final coalgebras.

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.