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.

翻译：我们引入了一种基于非良基证明系统的直觉主义逻辑扩展，该系统支持归纳定义与余归纳定义，其语法中固定点公式通过显式的序数变量进行标注。我们探索了该系统的计算内容，特别地定义了一种可计算性概念，并证明每个有效证明都是可计算的。由此，我们获得了针对所谓"有限公式"证明的规范化结果。该结果的特例表明：任何适当形式序列的证明都唯一对应一个自然数函数。最后，我们从该证明系统推导出一个范畴模型，并证明最小与最大固定点公式分别对应于初始代数与终余代数。