一句话：提出显式标注序数变量的非良基证明系统，证明有效证明可计算，并导出规范化与范畴模型。
本文研究带归纳与余归纳定义的直觉主义逻辑的计算内容。作者提出一种非良基证明系统，其语法用显式序数变量标注不动点公式，并给出可计算性概念，证明所有有效证明都是可计算的。由此得到有限公式证明的规范化结果；特别地，特定形式序列的每个证明都表示自然数上的唯一函数。最后，作者从证明系统导出范畴模型，并说明最小与最大不动点公式分别对应初代数与终余代数。
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.