Andrews 类型论中的未定义性

${\cal Q}_0$ 是由 Peter B. Andrews 提出并广泛研究的 Church 类型论的一个优雅版本。与其他传统逻辑一样，${\cal Q}_0$ 不容许未定义项。数学实践中处理未定义性的“传统方法”是将未定义项视为合法的、无指称的项，它们可以构成有意义陈述的组成部分。${\cal Q}^{\rm u}_{0}$ 是对 Andrews 类型论 ${\cal Q}_0$ 的一种修正，它直接形式化了这种处理未定义性的传统方法。本文提出了 ${\cal Q}^{\rm u}_{0}$，并证明了 ${\cal Q}^{\rm u}_{0}$ 的证明系统相对于其基于 Henkin 式广义模型的语义是可靠且完备的。本文对 ${\cal Q}^{\rm u}_{0}$ 的构建紧密遵循 Andrews 对 ${\cal Q}_0$ 的构建，以清晰 delineate 两个系统之间的差异。