累积归纳构造的谓词演算 (pCuIC) 的一致性

为避免与自指定义相关的众所周知悖论，高阶依赖类型论使用可数无穷的宇宙（亦称排序）层级对理论进行分层，Type$_0$ : Type$_1$ : $\cdots$。若对任意类型 $A$，有 $A$ : Type$_{i}$ 蕴含 $A$ : Type$_{i+1}$，则称此类类型系统为累积的。构成 Coq 证明助手基础的归纳构造谓词演算 (pCIC) 正是这样一个系统。本文提出并确立了累积归纳构造谓词演算 (pCuIC) 的可靠性，该系统将累积性关系扩展到了归纳类型。