1 基本概念
1.1 定义
形式证明是指在给定形式系统中，依据明确规定的公理和推理规则，对命题进行逐步演绎并最终得到结论的过程。它要求每一个推导环节都能被严格检查，从而使结论在该系统内部具有明确的逻辑有效性。与日常语言中的论证不同，形式证明不依赖直觉性的说服，而依赖符号化表示和规则化操作。
1.2 与非形式论证的区别
非形式论证通常以自然语言展开，强调表达的可理解性与说服力，允许省略部分中间环节，并依赖语境、经验和常识进行补足。形式证明则将论证拆解为可验证的符号步骤，任何一步若不符合规则，都可能导致整个证明失效。前者更重说明与辩护，后者更重严格性与可检验性。
1.3 形式证明的核心特征
形式证明的核心在于其可机械检查的结构。它不仅关注结论是否成立，还关注结论如何从前提出发被逐步导出。
1.3.1 严格的语法约束
形式证明只能使用系统允许的符号、公式和推导格式。命题如何书写、变量如何出现、量词如何绑定，都受到严格限制。这样的约束使得证明过程具有统一的形式，避免歧义。
1.3.2 可验证的推导步骤
每一步推导都必须能根据既定规则独立验证。无论是引入假设、使用公理，还是进行代入，都需要明确说明依据。正因为步骤可检验，形式证明才适合交由计算机处理。
1.3.3 结论相对于系统的有效性
形式证明所得到的结论，并非绝对意义上的“真”，而是相对于某个系统成立。若前提、公理和规则改变，结论的可证明性也可能随之变化。因此，形式证明强调的是“在该系统内可导出”。
2 形式系统
2.1 语言与符号
形式系统首先需要一套精确定义的语言，用于描述对象、关系和推理过程。语言的设计决定了能够表达哪些命题，也决定了证明的基本形态。
2.1.1 命题符号
命题逻辑中，命题符号通常表示最基本的陈述单元，如 P、Q、R 等。它们本身不再拆分为更细的结构，而是作为真假值的载体参与推理。通过联结词可以将这些基本符号组合成更复杂的公式。
2.1.2 谓词与量词
在谓词逻辑中，谓词用于刻画对象的性质或对象之间的关系，量词则用于表达“对所有”或“存在”这样的范围限定。它们使形式系统能够处理比命题逻辑更丰富的内容，特别适合表达数学中关于元素、集合和函数的陈述。
2.1.3 公式的构造规则
公式并不是任意拼接而成，而是按照构造规则逐层生成。变量、常项、函数符号、谓词符号和逻辑联结词需要按语法要求组合，才能形成合法公式。构造规则保证了表达式的唯一解释基础。
2.2 公理
公理是系统中无需证明即可直接采用的基本陈述。它们提供推理起点，并限定系统允许讨论的范围。
2.2.1 逻辑公理
逻辑公理体现纯粹逻辑结构，例如某些蕴含、否定和全称量化的基本模式。它们通常不依赖具体学科内容，而是描述推理本身的通用规律。
2.2.2 非逻辑公理
非逻辑公理与具体理论相关，例如几何、算术或集合论中的基本假设。不同领域的非逻辑公理不同，因此相同的逻辑框架可以承载不同的数学理论。
2.3 推理规则
推理规则规定如何由已知公式推出新公式，是形式证明最关键的操作机制之一。
2.3.1 直接推理规则
直接推理规则允许从前提中直接导出结论，例如由合取式推出其中一个分量，或由蕴含式和前件推出后件。此类规则通常简单明确，便于逐步执行。
2.3.2 结构性规则
结构性规则涉及假设的引入、消去和组织方式，决定了证明中前提如何被使用。例如某些系统允许重复使用前提，某些系统则对前提管理更为严格。
2.3.3 替换与代入
替换与代入是在保持公式结构合法的前提下，用具体项替换变量或用等价表达替换某部分内容。此类操作在数学证明中极为常见，尤其是在处理等式、函数和量词时。
3 证明的构造
3.1 证明步骤
证明通常不是一次完成，而是由多个可追踪步骤组成。每一步都应当清楚说明其来源和作用。
3.1.1 假设引入
许多证明会先暂时引入某些假设，以便在局部范围内展开推导。假设引入后，后续步骤必须说明哪些结论依赖于该假设。
3.1.2 中间结论推导
在证明过程中，往往需要先得到若干中间结论，再将其组合成最终目标。中间结论既是逻辑链条中的支点，也便于将复杂证明分解为小步骤。
3.1.3 结论推出
当所有必要条件都已建立后，证明便进入结论推出阶段。此时需要显示最终命题如何由前面的推导自然得出，并确认没有遗漏关键前提。
3.2 常见证明方法
不同类型的命题适合不同的证明策略。常见方法往往不是彼此排斥，而是可以组合使用。
3.2.1 直接证明
直接证明从命题前提出发，按照规则逐步推出结论。这种方法结构清晰，适用于命题之间存在明显推导链的情况。
3.2.2 反证法
反证法通过假设结论不成立，进而推出矛盾，从而间接确立原命题。它在处理否定性命题、存在性命题或难以直接构造的结论时十分常见。
3.2.3 数学归纳法
数学归纳法适用于具有递推结构的命题。通常先证明起始情形，再说明若某一步成立，则下一步也成立，由此推广到整体范围。
3.2.4 分情况讨论
当命题依赖于若干互斥条件时，分情况讨论是一种有效方法。证明者分别在各个可能情形下验证结论，再综合得到总命题成立。
3.3 证明结构
证明不仅有内容上的步骤，也有组织上的形式。不同结构会影响证明的表达方式和检查方式。
3.3.1 线性证明
线性证明按照单一顺序展开，从前提逐渐走向结论。它便于阅读和书写，是最常见的证明呈现方式之一。
3.3.2 树形证明
树形证明将推导分支化展示，特别适合包含多种分情况或多重前提的情形。证明的每个分支对应一条局部推理路径，最后在结点处汇合。
3.3.3 证明对象的层级组织
复杂证明常包含定理、引理、命题和推论等多个层次。通过层级组织，可以将大型证明拆分成若干相互支撑的局部结果，提高可读性与可管理性。
4 证明系统
4.1 自然演绎
自然演绎强调尽量贴近人类推理习惯，采用引入与消去规则处理联结词和量词。它常以局部假设为基础，适合展示命题如何由直观步骤逐渐构成。由于结构清楚，自然演绎在教学和形式化表达中都很常见。
4.2 希尔伯特系统
希尔伯特系统以少量公理模式和极简推理规则为基础，通常以蕴含推导和少数基本规则为核心。它的特点是形式紧凑，但单个证明可能较长，因而更适合理论分析而非日常书写。
4.3 序列演算
序列演算将证明表示为关于“前提推出结论”的序列，并通过对序列的规则变换进行推导。该体系便于研究逻辑结构、证明规范化以及元理论性质，在理论逻辑中具有重要地位。
4.4 类型论中的证明
类型论将证明与程序、命题与类型联系起来，使证明具有构造性和计算意义。它在现代计算机辅助证明中占有重要位置。
4.4.1 命题即类型
命题即类型的思想认为，一个命题若可证明，则对应类型非空；其证明则可看作该类型的一个项。这种对应关系使逻辑与编程之间出现深层联系。
4.4.2 证明项
证明项是证明在类型论中的具体表示，类似于程序中的表达式。它不仅说明命题成立，还记录了成立的构造方式。
4.4.3 构造性证明
构造性证明要求给出对象或算法，而不仅是排除其不存在的可能性。此类证明常强调可执行性，因此与计算过程结合紧密。
5 元理论性质
5.1 一致性
一致性是指系统中不能同时推出某命题及其否定。若系统不一致，则几乎任何命题都可能被推出，系统将失去区分真假陈述的能力。因此，一致性是形式系统最基本的要求之一。
5.2 完备性
完备性通常表示系统在某种意义下足够强大，使所有语义上成立的命题都能在系统中被证明。不同逻辑框架对完备性的定义略有差别，但其核心都在于“真”与“可证”之间的覆盖关系。
5.3 可判定性
可判定性关注的是：是否存在一个算法，能在有限时间内判断某类命题是否可证明。并非所有形式系统都具备这一性质，复杂性较高的理论往往在可判定性上面临限制。
5.4 可证明性
可证明性研究命题是否能够在指定系统中被导出，以及这种导出需要多大代价。它既是逻辑问题，也与计算复杂度密切相关。
5.4.1 证明与真理的关系
在理想化模型中，证明与真理可能高度一致，但在具体系统里二者并不总是完全重合。一个命题可能在语义上为真，却由于系统限制而暂时无法证明。
5.4.2 证明长度与复杂度
证明不仅有“能不能证明”的问题，还有“要多长才能证明”的问题。证明长度直接影响人工检查和机器验证的成本，也是证明复杂性研究的重要内容。
5.4.3 证明压缩
证明压缩关注如何用更短的形式表达原本较长的推导。通过引入引理、抽象共通结构或重用已有结果，可以减少冗余步骤，提高证明效率。
6 计算机辅助证明
6.1 证明助手
证明助手是一类帮助用户构造和检查形式证明的软件系统。它们通常要求输入严格形式化的命题和步骤，并能自动验证每一步是否合法。
6.1.1 交互式证明
交互式证明中，用户负责给出高层思路，系统负责检查细节并提示可行的下一步。此类方式兼顾灵活性与严格性，适合复杂定理的形式化。
6.1.2 自动化验证
自动化验证则侧重由系统自动完成更多推导工作，用户只需提供目标、策略或关键提示。它能显著减轻机械性工作，但对搜索能力和启发式策略要求较高。
6.2 自动定理证明
自动定理证明试图让计算机在较少人工介入下完成证明搜索、规则应用和结果确认。它常用于逻辑推理、程序分析和数学问题求解。
6.2.1 搜索策略
由于证明空间往往很大，自动系统需要借助搜索策略来决定优先探索哪些路径。常见策略包括启发式搜索、目标导向搜索和基于约束的筛选。
6.2.2 归结与重写
归结是一种典型的自动推理方法，适用于命题和一阶逻辑中的子句处理；重写则通过等式或规则将表达式化简为标准形式。二者常被结合使用，以提高自动证明效率。
6.3 形式化数学库
形式化数学库是将大量已证明定理、定义和引理系统整理后的知识集合。它们为后续证明提供可复用资源，也推动了大型数学形式化的发展。
6.3.1 定理库组织
定理库通常按照学科领域、理论层次或依赖关系组织，以便查找和维护。良好的结构能减少重复证明，并使库的扩展更有秩序。
6.3.2 证明复用
证明复用指在新证明中调用已有结果，而不是从头推导全部细节。它能显著提升效率，也是大型形式化工程得以持续扩展的重要原因。
6.3.3 机器可读文档
机器可读文档将数学内容写成可由程序解析的格式，使定义、命题和证明能够直接进入验证流程。这种表达方式有助于实现自动检查与长期维护。
7 应用领域
7.1 数学基础
形式证明在数学基础中用于刻画公理系统、分析推理边界，并研究定理可导出的条件。它使数学从单纯的经验性陈述转向可精确审查的演绎结构。
7.2 程序验证
在程序验证中，形式证明可用于说明程序是否满足规格说明，例如是否终止、是否保持不变量、是否输出正确结果。通过证明，程序行为可从经验测试提升为理论保证。
7.3 密码学中的正确性证明
密码学中的形式证明常用于说明协议或算法在特定假设下的正确性与安全性。它帮助区分设计层面的有效性与实现层面的漏洞风险。
7.4 逻辑与人工智能
形式证明也被用于人工智能中的推理与知识处理任务，尤其是在需要严格推导和可追踪结论的场景中。
7.4.1 知识表示
知识表示试图把信息编码为适合推理的形式结构。形式证明为这种编码提供了严谨的语义基础，使知识能够被机器处理。
7.4.2 推理引擎
推理引擎负责根据已有知识和规则生成新结论。它与形式证明关系密切，核心功能就是将显式前提转化为可验证的结果。
7.4.3 可解释性分析
由于形式证明保留了完整推导链条，因此天然具有较强的可解释性。它能够说明结论从何而来、依赖了哪些前提，这对分析系统输出尤为重要。
8 历史与发展
8.1 早期逻辑传统
早期逻辑传统可追溯至古代关于论辩、演绎和三段论的研究。虽然当时尚未形成现代符号化体系，但已经体现出对推理形式与有效性的关注。
8.2 现代符号逻辑的形成
随着符号化方法的发展，逻辑逐步摆脱自然语言的模糊性，形成了更系统的表示方式。命题演算、一阶逻辑等框架的建立，为形式证明奠定了现代基础。
8.3 20世纪形式化研究
20世纪中，数学基础、可计算性与证明论等领域推动了形式证明研究的深化。人们开始系统研究公理系统的性质、证明长度以及逻辑与计算之间的关系。
8.4 计算机时代的证明自动化
计算机时代使形式证明从纯理论工具扩展为可操作的工程手段。证明助手、自动推理程序和形式化数学库的发展，使大规模机器验证成为现实。
9 相关概念
9.1 定理
定理是能够在某一理论系统中被证明的命题。它通常由公理、定义和已有结果推导而来，是数学知识的重要组成部分。
9.2 命题
命题是具有真假判断意义的陈述单位。在形式逻辑中，命题可作为证明的对象，也可作为推理的中间环节。
9.3 演绎
演绎是从一般规则或已知前提出发，按逻辑规则推出结论的过程。形式证明本质上就是一种严格的演绎活动。
9.4 证明对象
证明对象指可被形式化表示并接受验证的对象，既可以是命题，也可以是定理、序列、类型或程序等。在不同体系中，其具体形态会有所不同。
9.4.1 证明树
证明树是将证明过程以树状结构表示的方法，适合展示分支推理与子目标之间的关系。
9.4.2 证明项
证明项是类型论或相关系统中对证明的程序化表示，强调证明与构造之间的对应关系。
9.4.3 证明检查器
证明检查器是用于验证形式证明是否符合规则的软件工具。它通常不负责“发现”证明，而负责精确核对证明的合法性。