直觉主义类型论 (2024)

# 直觉类型论 来源：https://plato.stanford.edu/entries/type-theory-intuitionistic/ ## 1. 概述 我们首先鸟瞰直觉类型论的一些重要方面。不熟悉该理论的读者在首次阅读时可能选择跳过。直觉类型论的起源是布劳威尔的直觉主义和罗素的类型论。它与 Church 的经典简单类型论（https://plato.stanford.edu/entries/type-theory-church/）类似，都基于带类型的 lambda 演算，但不同之处在于它采用了 Curry（1958）在命题逻辑中发现、并由 Howard（1980）和 de Bruijn（1970）扩展到谓词逻辑的**命题即类型**原则。这一扩展之所以可能，是因为引入了带索引的类型族（依赖类型）来表示谓词逻辑中的谓词。这样，所有逻辑联结词和量词都可以通过类型形成子来解释。 在直觉类型论中，还添加了其他类型，例如自然数类型、小类型类型（宇宙）和良基树类型。由此产生的理论包含了直觉数论（Heyting 算术）以及更多内容。该理论以自然演绎形式化，每个类型形成子的规则分为构造、引入、消去和等式规则。这些规则在引入和消去规则之间呈现出某种对称性，遵循 Gentzen 和 Prawitz 对自然演绎的处理，正如证明论语义（https://plato.stanford.edu/entries/proof-theoret-semantics/）条目中所解释的那样。 当命题被解释为类型时，其元素称为**证明对象**。当证明对象被添加到自然演绎演算中时，它就成为一个带有依赖类型的类型化 lambda 演算，扩展了 Church 原始的类型化 lambda 演算。等式规则是该演算项的计算规则。理论中定义的每个函数都是全函数且可计算的。因此，直觉类型论是一种类型化函数式编程语言，具有所有程序都终止的特殊性质。 直觉类型论不仅是一个形式逻辑系统，还为直觉主义提供了一个全面的哲学框架。它是一种**解释型语言**，其中**判断的展示**与**命题的证明**之间的区别起着根本作用（Sundholm 2012）。直觉类型论的判断意义是通过类型和项的规范形式计算来解释的。这些非正式的、直观的意义解释是“前数学的”，应与在标准数学框架（如集合论）内开发的形式数学模型区分开来。这种意义理论也证明了各种归纳、递归和归纳递归定义的合理性。 尽管某些证明论上的强概念（如某些大基数的类比）可以被证明是合理的，但该系统被认为是**可预测的**。高阶逻辑、直觉集合论和拓扑理论中出现的那种非可预测定义并非该理论的一部分。Markov 原理也不包含在内，因此该理论与俄罗斯构造主义不同。另一种用于可预测构造数学的形式逻辑系统是 Myhill 和 Aczel 的**构造性 Zermelo-Fraenkel 集合论**（https://plato.stanford.edu/entries/set-theory-constructive/）（CZF）。该理论基于直觉一阶谓词逻辑，并削弱了经典 Zermelo-Fraenkel 集合论的一些公理，在直觉类型论中有自然的解释。因此，Martin-Löf 的意义解释也间接构成了 CZF 的基础。 直觉类型论的变体支撑了几个广泛使用的证明助手，包括 NuPRL、Coq 和 Agda。这些证明助手是计算机系统，已被用于形式化大型和复杂的数学定理证明，如图论中的四色定理和有限群论中的 Feit-Thompson 定理。它们还被用于证明一个现实的 C 编译器（Leroy 2009）和其他计算机软件的正确性。 从哲学和实践角度看，直觉类型论是一个基础框架，其中构造性数学和计算机编程在深层意义上是相同的。Gonthier（2008）在描述其四色定理证明的论文中强调了这一点： > 对此证明成功的方法是将几乎每个数学概念转化为 Coq 系统中的数据结构或程序，从而将整个事业转化为程序验证。 ## 2. 命题即类型 ### 2.1 直觉类型论：看待逻辑的新方式？ 直觉类型论通过引入显式证明对象提供了一种分析逻辑的新方式。这为逻辑提供了直接的计算解释，因为证明对象具有计算规则。就表达能力而言，直觉类型论可以被视为一阶逻辑的扩展，就像高阶逻辑一样，但是可预测的。 #### 2.1.1 一种类型论 罗素为了回应他在朴素集合论中发现的悖论而发展了**类型论**（https://plato.stanford.edu/entries/type-theory/）。在他的分支类型论中，数学对象根据其**类型**进行分类：命题类型、对象类型、对象属性类型等。当 Church 在类型化 lambda 演算的基础上发展他的**简单类型论**（https://plato.stanford.edu/entries/type-theory-church/）时，他添加了一条规则：理论中任何两个类型之间都存在一个函数类型。 直觉类型论进一步用依赖类型（即带索引的类型族）扩展了简单类型化 lambda 演算。一个例子是按 \(n\) 索引的 \(n\) 元组类型族。类型在编程中已经被广泛使用了很长时间。早期的高级编程语言引入了整数和浮点数类型。现代编程语言通常具有丰富的类型系统，包含许多用于形成新类型的构造。 直觉类型论是一种函数式编程语言，其类型系统如此丰富，以至于几乎任何可想象的程序属性都可以表示为类型。因此，类型可以用作程序任务的规范。 #### 2.1.2 带证明对象的直觉逻辑 布劳威尔对逻辑的分析使他得出了一种直觉逻辑，它拒绝排中律和双重否定律。这些定律在直觉类型论中无效。因此，它不包含经典（Peano）算术，而只包含直觉（Heyting）算术。（Peano 算术可以通过双重否定解释在 Heyting 算术中被解释，这是另一回事，参见直觉逻辑条目（https://plato.stanford.edu/entries/logic-intuitionistic/）。） 考虑直觉算术的一个定理，例如除法定理： \[ \forall m, n. m > 0 \supset \exists q, r. mq + r = n \wedge m > r \] 该定理的形式证明（通常意义下）是一个公式序列（或树），其中最后一个（根）公式是定理，序列中的每个公式要么是公理（一个叶节点），要么是对某些更早（更高）公式应用推理规则的结果。当在直觉类型论中证明除法定理时，我们不仅构建了通常意义下的形式证明，还构建了一个**构造**（或**证明对象**）“\(\divi\)”，它见证了该定理的真理性。 我们写成： \[ \divi : \forall m, n {:} \mathbb{N}.\, m > 0 \supset \exists q, r {:} \mathbb{N}.\, mq + r = n \wedge m > r \] 以表达 \(\divi\) 是除法定理的证明对象，即代表除法定理类型的元素。 当命题表示为类型时，\(\forall\) 量词被识别为依赖函数空间形成子（或广义笛卡尔积）\(\Pi\)，\(\exists\) 量词被识别为依赖对类型形成子（或广义不相交和）\(\Sigma\)，合取 \(\wedge\) 被识别为笛卡尔积 \(\times\)，恒等关系 = 被识别为恒等证明对象的类型形成子 \(\mathsf{I}\)，大于关系 > 被识别为大于陈述证明对象的类型形成子 \(\mathsf{GT}\)。 使用“类型表示法”，我们写成： \[ \divi : \Pi m, n {:} \mathbb{N}.\, \mathsf{GT}(m,0) \rightarrow \Sigma q, r {:} \mathbb{N}.\, \mathsf{I}(\mathbb{N}, mq + r, n) \times \mathsf{GT}(m, r) \] 以表达证明对象“\(\divi\)”是一个函数，它映射两个数字 \(m\) 和 \(n\) 以及一个见证 \(m > 0\) 的证明对象 \(p\) 到一个四元组 \((q, (r, (s, t)))\)，其中 \(q\) 是商，\(r\) 是用 \(m\) 除 \(n\) 得到的余数。第三个组件 \(s\) 是一个见证 \(mq + r = n\) 的证明对象，第四个组件 \(t\) 是一个见证 \(m > r\) 的证明对象。 关键的是，\(\divi\) 不仅在经典意义上是一个函数；它在直觉意义上也是一个函数，即一个程序，当给定输入 \(m\)、\(n\)、\(p\) 时，它计算输出 \((q, (r, (s, t)))\)。这个程序是 lambda 演算中带有特殊常量的项，即函数式编程语言中的程序。 #### 2.1.3 一阶谓词逻辑的扩展 直觉类型论可以被视为一阶逻辑的扩展，就像高阶逻辑是的一阶逻辑的扩展一样。在高阶逻辑中，我们发现一些个体域可以被解释为我们喜欢的任何集合。如果签名中有关系常量，它们可以被解释为解释个体域集合之间的任何关系。在此基础上，我们可以对关系进行量化，对关系的关系进行量化，等等。 我们可以将高阶逻辑视为配备了一种引入新量化域方式的一阶逻辑：如果 \(S_1, \ldots, S_n\) 是量化域，那么 \((S_1, \ldots, S_n)\) 是一个新的量化域，由域 \(S_1, \ldots, S_n\) 之间的所有 n 元关系组成。高阶逻辑有一个直接的集合论解释，其中 \((S_1, \ldots, S_n)\) 被解释为幂集 \(P(A_1 \times \cdots \times A_n)\)，其中 \(A_i\) 是 \(S_i\) 的解释，对于 \(i=1, \ldots, n\)。这就是 Ramsey、Church 等人引入的那种高阶逻辑或简单类型论。 直觉类型论也可以类似地看待，只是这里引入量化域的可能性更丰富，可以使用 \(\Sigma, \Pi, +, \mathsf{I}\) 从旧域构造新域。（第 3.1 节（https://plato.stanford.edu/entries/type-theory-intuitionistic/#Judg）；Martin-Löf 1998 [1972]）。 直觉类型论也有一个直接的集合论解释，其中 \(\Sigma\)、\(\Pi\) 等被解释为相应的集合论构造；见下文。我们可以像在 HOL 中一样向直觉类型论添加未指定的个体域。这些被解释为集合，就像在 HOL 中一样。 现在我们展示与 HOL 的一个区别：在直觉类型论中，我们可以引入未指定的族符号。我们可以将 \(T\) 引入为个体域 \(S\) 上的一个类型族： \[ T(x) \;\mathsf{type}\; (x{:}S). \] 如果 \(S\) 被解释为 \(A\)，那么 \(T\) 可以被解释为由 \(A\) 索引的任何集合族。作为一个非数学例子，我们可以将一个个体域*人*成员之间的二元关系*爱*表示如下。在域 People 上引入二元族 Loves： \[ \mathsf{Loves}(x,y) \;\mathsf{type}\; (x{:}\mathsf{People}, y{:}\mathsf{People}). \] 解释可以是任何集合族 \(B_{x,y}\)（\(x{:}A\)，\(y{:}A\)）。 这如何涵盖关系的标准概念？假设我们在熟悉的集合论意义下有一个二元关系 \(R\) 在 \(A\) 上。我们可以如下构造一个对应的二元族： \[ B_{x,y} = \begin{cases} \{0\} &\text{如果 } R(x,y) \text{ 成立} \\ \varnothing &\text{如果 } R(x,y) \text{ 为假。} \end{cases} \] 现在显然 \(B_{x,y}\) 非空当且仅当 \(R(x,y)\) 成立。（我们可以选择集合论宇宙中的任何其他元素而不是 0 来表示真。）因此，从任何关系出发，我们都可以构造一个族，其中 \(x,y\) 的真等价于 \(B_{x,y}\) 非空。 注意，这种解释并不关心 \(R(x,y)\) 的证明是什么，只关心它成立。回忆一下，直觉类型论将命题解释为类型，所以 \(p{:} \mathsf{Loves}(\mathsf{John}, \mathsf{Mary})\) 意味着 \(\mathsf{Loves}(\mathsf{John}, \mathsf{Mary})\) 为真。将关系解释为族允许跟踪 \(R(x,y)\) 成立的证明或证据，但我们也可以选择忽略它。 在蒙太古语义学（https://plato.stanford.edu/entries/montague-semantics/）中，高阶逻辑用于给出自然语言（以及上述例子）的语义。Ranta（1994）引入了使用直觉类型论借助依赖类型更好地捕捉句子结构的思想。 相比之下，数学关系 \(\gt\) 在直觉类型论中将如何处理？首先我们需要一个数字类型 \(\mathbb{N}\)。原则上我们可以引入一个未指定的个体域 \(\mathbb{N}\)，然后添加公理，就像我们在一阶逻辑中设置 Peano 算术的公理系统时所做的那样。然而，这不会给我们期望的计算解释。因此，如下所述，我们为在 \(\mathbb{N}\) 中构造新自然数制定引入规则，并为定义 \(\mathbb{N}\) 上的函数（通过递归）制定消去和计算规则。 标准顺序关系 \(\gt\) 应满足： \[ x \gt y \text{ 当且仅当存在 } z{:}\mathbb{N} \text{ 使得 } y+z+1 = x. \] 在直觉类型论中，右边被表示为 \(\Sigma z{:}\mathbb{N}.\, \mathsf{I}(\mathbb{N}, y+z+1, x)\)，我们将其作为关系 \(\gt\) 的定义。（\(+\) 是通过递归方程定义的，\(\mathsf{I}\) 是恒等类型构造。）现在，\(\gt\) 的所有性质都由上述提到的 \(\mathbb{N}\) 的引入、消去和计算规则确定。 #### 2.1.4 具有多种判断形式的逻辑 直觉类型论的类型系统非常具有表达力。结果是，一个类型是否良构不再是一个简单的解析问题，而是需要证明的事情。类型的良构性是直觉类型论的一种**判断**形式。项相对于类型的良类型是另一种。此外，还有类型和项的等式判断。这是直觉类型论区别于只关注表达命题真假的单一判断的普通一阶逻辑的又一种方式。 #### 2.1.5 语义学 虽然一阶逻辑的标准介绍会遵循 Tarski 定义模型的概念，但直觉类型论的语义学……（内容中断）