形式证明 · aiwiki.page

形式证明是用精确定义的语言表述的数学证明，其中每一步推理都有明确规则作为依据。它确立的是：在某个形式系统中，结论可由给定假设推出，而不是依赖读者补足未明说的推理。形式证明在逻辑学和数学基础研究中居于核心地位，也是借助计算机验证数学成果、软件和硬件的基础。其本质特征是依据明确规则为推理提供论证，而不一定是使用计算机。(leanprover.github.io)

结构与简单示例

形式系统规定了其语言的符号和构成规则、公理以及允许使用的推理规则。证明可以表示为有限的公式序列或公式树。每一步都必须是公理、规则允许引入的假设，或依据某条明确规则从先前步骤推出的结果。涉及临时假设的规则还会规定何时可以消去这些假设。定理是能够在系统中推导出的陈述；从额外前提进行的推导，则确立了以这些前提为条件的推论。(builds.openlogicproject.org)

例如，在命题逻辑中，肯定前件式允许从 $P$ 和 $P\rightarrow Q$ 推出 $Q$ ：

$P$ ——前提。
$P\rightarrow Q$ ——前提。
$Q$ ——对第 1 步和第 2 步应用肯定前件式。

记号 $\Gamma\vdash Q$ 表示可以从 $\Gamma$ 中的假设推导出 $Q$ 。这一推导并不独立证明其前提成立，而是表明：一旦接受这些前提，结论便随之成立。在具有适当蕴含引入规则的系统中，消去这些假设即可得到定理 $P\rightarrow((P\rightarrow Q)\rightarrow Q)$ 。(builds.openlogicproject.org)

因此，形式化不只是把日常用语替换成符号。定义、量化的论域、假设和依赖关系都必须足够精确，使选定的规则能够适用。先前已经证明的结果可以作为可复用的组成部分，前提是这些结果的陈述及其证明推导在形式框架内可用。(leanprover.github.io)

证明系统与通常的数学写作

不同证明系统以不同方式组织演绎推理。希尔伯特式系统通常采用公理模式和相对较少的推理规则。自然演绎使用逻辑联结词的引入规则和消去规则，往往包含嵌套的子证明。相继式演算则明确列出假设集合和结论集合。证明论研究这些系统及其推导的结构性质。(openlogicproject.org)

所采用的底层逻辑也很重要。经典推理允许使用一些在直觉主义逻辑中通常不成立的原则，例如不受限制的双重否定消去。因此，将经典的反证法转化为构造性框架中的证明时，可能需要引入额外原则。“形式”并不指某一种特定的逻辑或基础体系。(docs.lean-lang.org)

通常的数学证明结合了文字、符号、图示，并省略一些常规步骤。这类证明即使没有完全形式化，也可以是严谨的：其目标读者会补足背景定义，并识别标准论证。相比之下，形式推导会将所需的依赖关系交代得足够明确，以便按照规则进行检查。它可能揭示缺失的假设，却不会自动解释某个论证为何富有启发性，或哪些思想促成了它的发现。(leanprover.github.io)

可推导性、真与局限

形式可推导性关注的是按照规则对表达式进行操作。语义学关注的是表达式的解释。在一阶逻辑中， $\Gamma\models\varphi$ 表示每一种满足前提 $\Gamma$ 的解释也都满足 $\varphi$ 。这种语义后承关系不同于句法关系 $\Gamma\vdash\varphi$ 。(builds.openlogicproject.org)

如果可推导性保证语义后承关系成立，演绎系统就是可靠的；如果每个语义后承都可以推导出来，系统就是完备的。标准的经典一阶演算同时具有这两种性质。这里的完备性意味着能够涵盖前提在所有解释下的后承，而不是能够证明某个预期数学结构中为真的每一个陈述。(builds.openlogicproject.org)

哥德尔不完备定理揭示了另一种局限。一个一致、可有效公理化且足以表达初等算术的理论，无法判定其语言中的每一个语句：有些语句在该理论内既不能被证明，也不能被否证。这与一阶逻辑的完备性并不矛盾，因为演算的完备性与特定公理化理论的完备性是不同的性质。(builds.openlogicproject.org)

计算机检查与证明助手

证明助手支持形式推导的构建与检查。例如，在 Lean 中，命题表示为类型，证明则表示为属于这些类型的项。在这种与类型论相关的“命题即类型”解释下，检查证明就成为一种类型检查。蕴含对应于一个函数，它将前提的证据转换为结论的证据。(docs.lean-lang.org)

用户不必手动写出每一个基本步骤。证明策略可以化简表达式、引入假设，或搜索中间论证。在 Lean 通常采用的证明项工作流程中，策略的输出由一个小型内核检查，这一检查独立于生成输出的策略。尽管如此，可信性仍取决于内核以及所使用的任何附加机制；依赖原生求值的证明可能引入更广泛的实现依赖。此外，还必须将显式公理和未完成证明的占位符与已经证明的结果区分开来。(lean-lang.org)

应用与验证范围

在形式验证中，软件或硬件的行为用数学方式表示，再通过证明确立这一表示满足某项规约。可以证明某个算法返回的结果符合其规定的条件。这保证了在模型假设成立时，相应的形式性质成立；至于模型、规约与实际系统之间是否相符，仍是一个需要另行考察的问题。(leanprover.github.io)

大型数学形式化项目也展示了这一方法所能达到的规模。Flyspeck 项目使用 HOL Light 和 Isabelle 完成了开普勒猜想的形式证明；介绍这一成果的论文于 2017 年发表。其验证既涵盖数学论证，也涵盖大量计算部分。审查这样的形式化成果，需要考察形式陈述、相关定义、所用假设以及检查推导的机制，而不能仅仅看证明脚本是否成功运行。(cambridge.org)