为什么证明助手使用从属类型理论而不是集合理论？

\\ begingroup $在演讲中，凯文·巴扎德（Kevin Buzzard）博士指出，精益是唯一适用于形式化所有数学的现有证明助手。在演讲的“问答环节”（1:00:00）中，他提出以下理由：

我的问题是关于第一个问题的：为什么集合论（与从属类型论相比）很难实现自动化？

$ \ endgroup $

$ \ begingroup $也很想问一句句子的准确性，它是现有的唯一这样的证明助手，它表明其他证明助手（例如Coq）“不适合将所有数学形式化”。 $ \ endgroup $ – YCor

$ \ begingroup $我希望Buzzard参与讨论。但是我发现奇怪的是，这一次提到了Voevodsky周围的“小伙子”，除了对环和模块进行形式化之外，他们对Coq并没有做任何事情。我没听错吗？听起来确实令人误解。显然，有很多由Coq正规化的数学库；例如，Gonthier等人将奇数定理形式化（可解决奇数有限组）。是一种这样的巡回演出，尽管不一定是“ Voevodsky小伙子”开发的。 $ \ endgroup $ – Todd Trimble♦

$ \ begingroup $ @TimothyChow谢谢；我再次听了，你是对的。不过，我不确定如何接受“无所作为”的主张。 $ \ endgroup $ – Todd Trimble♦

$ \ begingroup $让我再说一次，我对Coq口臭的事感到非常遗憾，我不知道会不会对Coq造成严重影响。 $ \ endgroup $ –凯文·巴扎德

$ \ begingroup $是的，这很好地概括了它！现在，我已经就此问题进行了20多次演讲，并且有一些录音被记录在案，但是不知何故，这一演讲变得疯狂了，我完全无意间使一堆Coq用户不安。对于Coq生态系统的优缺点，我确实有很强的看法，但是在演讲中总结它们时我做得很糟糕。我在其他地方（例如在Coq Zulip上）发表了更多经过深思熟虑的评论，但没有任何内容可以吸引此演讲。 $ \ endgroup $ –凯文·巴扎德

$ \ begingroup $我写了一个冗长的答案表示歉意，但是我感到关于形式化数学基础的讨论通常由于缺乏信息而受阻。

我已经使用了一段时间的证明助手，并且还进行了他们的设计和实现。尽管我会很快讲一些关于集合论的笑话，但我非常痛苦地意识到类型论的缺点，很可能比典型的集合论者更是如此。 （哈，哈，“典型的集合论者”！）如果有人可以向我展示如何用集合论来改进证明助手，那么我绝对会感到无所适从！但是仅仅拥有一个好的想法是不够的–您需要在大型项目中进行实践测试，因为与形式化数学相关的许多现象只有在达到一定程度的复杂性后才会出现。

现代证明助手的体系结构是数十年实验，开发和实践经验的结果。证明助手不包含一个，而是包含多个正式系统。

证明助手的核心组件是内核，它可验证每个推理步骤并确保证明正确。它是通过实现一个正式的系统$ F $（基础）来实现的，该系统的表现力足以允许大量数学的形式化，但又足够简单以允许高效且正确的实现。

内核中实现的基础系统太基本，无法直接用于复杂的数学。取而代之的是，用户使用一种更具表现力的形式化语言$ V $（白话）来编写他们的输入，这种语言被设计成实用且有用的。通常$ V $非常复杂，因此可以容纳各种符号约定和其他可接受的数学表达形式。证明助手的第二个组成部分，细化器，将$ V $转换为$ F $，并将转换结果传递给内核进行验证。

证明助手可以合并第三种正式语言$ M $（元语言），该语言用于实现证明搜索，决策程序和其他自动化技术。因为$ M $的目的是实现算法，所以它通常类似于编程语言。 $ M $和$ V $之间的区别可能不是很明显，有时它们被合并为一个形式主义。从数学角度来看，$ M $比$ F $和$ V $有趣，因此我们将忽略它。

整个系统的正确性取决于内核的正确性。内核中的错误允许接受无效的证明，而任何其他组件中的错误仅是一个烦人。因此，基础$ F $应该很简单，以便我们可以可靠地实现它。它不应太过奇特，以至于逻辑学家无法说出它与公认的数学基础之间的关系。计算机速度很快，因此从$ V $到$ F $的转换是否产生冗长的语句并不重要（太多）。同样，$ F $不必直接由人类使用。

集合论或类型论的合适变体符合这些标准。实际上，Mizar是基于集合论的，而HOL，Lean，Coq和Agda则在内核中使用类型论。由于集合论和类型论在数学上都非常了解，并且或多或少地具有同等的表现力，因此选择将取决于技术标准，例如证明检查算法的可用性和效率。

为了使本地语言有用，它必须尽可能地反映数学实践。它应该允许以熟悉的术语直接表达数学思想和概念，而没有不必要的形式主义麻烦。另一方面，$ V $应该是一种正式的语言，以便制作者可以将其翻译为基础$ F $。

要了解有关使$ V $变得更好的原因的更多信息，我们需要仔细观察数学家如何实际编写数学。它们产生定义，定理和构造的复杂网络，因此$ V $应该支持对大量正规数学的管理。在这方面，通过查看程序员如何组织软件，我们可以学到很多东西。例如，说一个数学主体是“只是一系列定义，定理和证明”，这是一种幼稚的理想化，它在某些情况下有效，但在数学的实际形式化中肯定不是。

数学家在他们的著作中省略了大量信息，并且非常愿意为了简洁而牺牲形式上的正确性。希望读者填写缺少的细节，并纠正不正确之处。证明助手将执行相同的操作。为了说明这一点，请考虑以下数学文本片段：

假设$ U $和$ V $为向量空间，$ f：U \至V $为线性映射。那么对于所有$ x $和$ y $，$ f（2 \ cdot x + y）= 2 \ cdot f（x）+ f（y）$。

你听懂了吗当然。但是，您可能会惊讶地发现大脑进行了多少猜测和纠正：

标量字段未指定，但这不会阻止您理解文本。您仅假设存在标量$ K $的一些基础字段。您可能会在随后的文本中找到有关$ K $的更多信息。 （$ K $是一个存在变量。）

严格来说“ $ f：U \ to V $”没有意义，因为$ U $和$ V $没有设置，而是结构$ U =（| U |，0_U，{+} _ U，{-} _ U， {\ cdot} _U）$和$ V =（| V |，0_V，{+} _ V，{-} _ V，{\ cdot} _V）$。当然，您正确地推测$ f $是运营商之间的映射，即$ f：| U |。 \至| V | $。 （您从向量空间向其载体插入了隐式强制。）

$ x $和$ y $的范围是多少？为了使$ f（x）$和$ f（y）$有意义，必须是$ x \ in | U | $和$ y \ in | U | $。 （您推断出$ x $和$ y $的域。）

在等式中，左侧的$ + $表示$ + _ {U} $，右侧的$ + $是$ {+} _ V $，对于标量乘法也类似。 （您重构了$ + $的隐式参数。）

每个孩子都知道，符号$ 2 $是一个自然数，但显然它的意思是表示标量$ 1_K + _K 1_K $。 （您再次从$ \ mathbb {N} $插入到$ K $的隐式强制，将$ n $映射为$ 1 $ K $的$ n $倍数。）

本地的$ V $必须支持这些技术，以及更多其他技术，以便可以在详细说明中实现它们。它不能像具有一阶逻辑和定义扩展的ZFC或单纯的Martin-Löf类型理论那样简单。您可能会认为$ V $的开发超出了数学和逻辑的范围，但是当计算机科学家按照他们的技术塑造它时，不要抱怨。

我从未见过针对基于集合论的本地语言的任何严肃建议。或者换句话说，一旦我们开始扩展和转换集合论以适应$ V $的要求，我们最终得到的东西看起来很像类型论。 （您可以考虑如何用集合论来检测$ f：U \ to V $才有意义，除非我们插入强制–因为如果一切都是集合，那么$ U $和$ V $也是如此。 ，在这种情况下，$ f：U \ to V $确实有意义。）

基础适用性的一个重要方面是其发现错误的能力。当然，它的目的是防止逻辑错误，但是错误不仅限于违反逻辑。有形式上有意义的陈述，很可能是错误。请考虑以下代码片段，并仔细阅读：

定义：当每个$ x \ in X $中存在一个bryllyg $ U \ subseteq X $和一个乏味的$ K \ subseteq X $使得$ x \ in U $和$ U \ in时，集合$ X $是jaberwocky K $。

即使您从未阅读过Lewis Carroll的作品，您也应该对“ $ U \ in K $”感到好奇。看起来“ $ U \ subseteq K $”更有意义，因为$ U $和$ K $都是$ X $的子集。尽管如此，其基础$ F $基于ZFC的证明助手将接受上述定义为有效，即使人类不太可能使用它。

基于类型理论的证明助手会通过声明“ $ U \ in K $”是类型错误来拒绝该定义。

因此，假设我们使用集合理论基础$ F $，该基础接受任何语法公式均有效。在这样的系统中，写“ $ U \ in K $”是有意义的，因此内核将接受上述定义。如果我们希望证明助手真正地帮助人类，它就必须包含一个附加机制，即使内核对此感到满意，该机制仍会将“ $ U \ in K $”标记为可疑对象。但是，如果不仅仅是基于类型理论的第二个内核，那么这种额外的机制又是什么呢？

我并不是说不可能基于集合论来设计证明助手。毕竟，所有这些中最受尊敬的Mizar都是以这种方式精确设计的-集合论在顶部具有类型理论机制的层。但是我不禁要问：为什么要烦恼需要集合类型理论的围栏的集合论内核，以使用户免受集合论的意料之外的限制？

$ \ endgroup $

$ \ begingroup $非常有用的答案！但是我不明白“基于ZFC的基础$ F $的证明助手将接受上述定义为有效的说法”。它是否被接受取决于白话而不是基础，不是吗？是什么阻止某人在集合论基础上构建类似于类型理论的白话语言？如果我们希望能够根据集合论公理来校准逻辑强度，但又希望在人机界面中使用类型论的优势，那似乎是很自然的事情。 $ \ endgroup $ –蒂莫西·周

$ \ begingroup $ Andrej，非常感谢您的出色回答！ （超级未成年人nitpick：让我们看看元语言$ M $对数学家来说是否不重要。事实证明，重要的是，数学家/用户可以轻松地编写少量的元代码来整理特定于子字段的证明方法例如：在我最近与Rob Lewis进行Witt向量环的形式化的项目中，我们为所谓的“重影计算”（即Witt向量的通用方法）编写了战术（元代码），这使我们得以写出2许多身份的在线证明，模仿非正式证明。）$ \ endgroup $ – jmc

$ \ begingroup $ @TimothyChow Metamath在设计时就考虑了这种用例；该工具报告任何特定定理所依赖的公理，并且有许多专门的冗余公理，以便您可以用其所具有的最小公理强度来证明一个定理；由于整个库都是以这种方式编写的，因此您既可以找出给定的证明是否在ZF替换中，也可以在该子集中找到不平凡的定理。 $ \ endgroup $ – Mario Carneiro

$ \ begingroup $这是一个非常了不起的答案，MathOverflow处于最佳状态。但是，有两个问题/异议：（1）“内核中的错误允许接受无效的证明，而其他任何组件中的错误仅是一个烦人”：细化器中的错误如何处理？那不是灾难性的吗？ （2）在“让$ U $和$ V $为向量空间，而$ f：U \ to V $为线性映射”中，我看不到任何隐式强制。作为分类理论家，我相信你的话。 $ f $是向量空间之间的线性映射，仅此而已。这是$ \ mathbf {Vect} $中的箭头。简而言之，这里没有提及集吧？ $ \ endgroup $ –汤姆·伦斯特

$ \ begingroup $ @TomLeinster但是，在这种解释下（我也希望这样做），然后您必须隐式将线性映射强制转换为集合函数，以便编写$ f（x）$。 （-：$ \ endgroup $ –́ Mike Shulman

$ \ begingroup $我个人认为Kevin Buzzard所做的工作非常出色；同时，他对尚未普遍使用的证明助手有很强的见解，因此您应该一丁点儿接受这些见解。

在2018年，约翰·哈里森（John Harrison）进行了题为``让集合理论再次变得伟大！''的演讲。 IMO，Harrison演讲的幻灯片比Buzzard更加平衡地讨论了使用集合论的利弊。

关于精益，几年前，汤姆·海尔斯（Tom Hales）对精益定理证明者进行了回顾，阐明了当时所见的利弊。他所说的某些内容在今天可能已不再适用，但事实是，即使精益爱好者也同意，他们承诺将在精益版本4中修复一些缺陷（不幸的是，该缺陷将与精益3不兼容，或我听到）。

$ \ endgroup $

$ \ begingroup $ John Harrison的幻灯片是一组很好的建议，但是从对定理证明者有好的想法到实施并尝试它们还有很长的路要走。哈里森是否已经研究过这些想法？ $ \ endgroup $ –安德烈·鲍尔（Andrej Bauer）

$ \ begingroup $我从未坚持过一种方法总比另一种方法更好。无论如何，我都会在一个单独的答案中更仔细地解释我的立场。 $ \ endgroup $ –安德烈·鲍尔（Andrej Bauer）

$ \ begingroup $进行计数时，我喜欢自然数从0开始（因为某些集合为空）。当我做质数和因式分解时，我喜欢它们从1开始（否则，我必须不断写“如果n不为零，则...”）。我对集合和类型的感觉是相同的-不同的基础系统使不同的事情变得更容易/更简单。 $ \ endgroup $ –凯文·巴扎德

$ \ begingroup $我仍然感到非常惊讶，我所进行的这种随机交谈吸引了如此多的关注，特别是因为并非我所说的一切都经过深思熟虑。我非常乐意与人们进行讨论，讨论我所说的话以及我所说的某些话是否不了解情况。

但是，在我对您的问题的回答上：尽管我一般不是专家证明专家（我已经成为一名专家的知识渊博，并且对其他人的经验有限），但是根据我的经验观察，像精益钻戒这样的高级策略策略，它将立即证明$（x + 2y）^ 3 = x ^ 3 + 6x ^ 2y + 12xy ^ 2 + 8y ^ 3 $这样的结果-在Coq和Isabelle / HOL中也有类似的策略，另外两种类型理论系统-似乎不存在于两个主要的集合理论形式证明系统中，即Metamath和Mizar。我真的不知道为什么，但是这些都是事实。请注意，从环的公理来证明这一点非常长且令人不舒服，因为您需要多次应用加法和乘法的关联性和可交换性-数学家所做的事情几乎没有考虑。

$ \ endgroup $

$ \ begingroup $因此，在回应游戏中，安德烈（Andrej）提出了一个评论-并问“理论上可以做什么？”，在这个游戏中，一个同样重要的问题是“实践中可以做什么？” Mario Carneiro是Metamath和Lean的专家，据我所知，他在短短几天内就写下了Lean的铃声策略，但Metamath仍然没有铃声策略。 $ \ endgroup $ –凯文·巴扎德

$ \ begingroup $我没有为Metamath写戒指的部分原因是因为没有太多的例子无法用更好的证据手动完成。在元数学中，创建丑陋证明的策略很难出售，因为证明的每一行都暴露给所有人阅读。数字评估器（又名lean的norm_num）是用metamath编写的，并且包含与环战术相同的技术。 $ \ endgroup $ – Mario Carneiro

$ \ begingroup $ ...我正在使用的当前证明助手Metamath Zero是基于peano算术，甚至没有集合论，并且环法与lean一样容易编写。这更多地与语言框架有关，而不是与形式系统有关（用Andrej的话说：$ M $对于编写自动化来说很重要，而不是$ F $），而Metamath的问题在于$ M $根本没有编码在“可交付成果”中，因此每个作者都必须亲自发现它。 $ \ endgroup $ – Mario Carneiro

$ \ begingroup $我将只回答自动化问题，因为其他答案给出了很好的概括，但似乎没有集中在这个狭窄的问题上。我自己的直接自动化经验是使用ACL2，精益和基于SMT的求解器。

严格来讲，我不知道为什么精益理论中的集合论比基于类型论的方法好还是坏，有什么基础论点。

从我的角度来看，Lean的优势在于：表达力强的显式类型系统，用于表示术语的相对简单的核心语言，以及对术语如何有效操纵表示的关注。

关于类型化的核心逻辑，定理证明中的大多数自动化都是针对数学中广泛使用的特定通用理论量身定制的。在编写这种自动化程序时，重要的是要知道所涉及的类型和操作。例如，在用无类型语言编写线性算术的决策程序时，即使表达式不表示数字，也需要仔细检查是否所有转换仍然有意义。通过使用经过类型验证和类型检查的表达式语言，可以从定理证明者本身获得知识，而不必支付额外的运行时和复杂性成本。

精益的第二个优势是确保核心语言既简单又具有表达力，因此可以紧凑地表示证明。当使用诸如SMT求解器之类的自动化工具时，作为证据生成的“证明条款”可能非常庞大，并且需要设计核心证明语言以紧凑地表示证明，同时仍然要进行有效的检查。我不确定Lean本身是否对Coq或其他求解器有优势，但这是否是Lean设计的一个因素。

精益的第三项优势是写作的语言

......