第二十七章　步骤、引理与证明模块

一、数学中的封装，首先不是把证明缩短

一份证明可以很短，却把全部困难藏在一句“由显然结论可得”里；也可以很长，却已经把各项依赖组织得清楚可用。封装的质量不能只按可见文字长度判断。真正的问题是：内部义务是否完成，外部调用是否保留必要条件，以及需要时能否重新展开。

数学中把一个已经证明的结论作为引理使用，可以成为理解封装的清晰入口。上层证明通常不需要每次重写引理的全部推导，但必须确认引理的条件在当前处境满足。被折叠的是内部论证，不是对当前适用性的判断。

因此，模块至少具有两个层面：内部说明它为什么成立，接口说明在什么情况下可以使用。内部再复杂，也不能使接口含糊；接口再简洁，也不能凭简洁获得内部依据。两者之间的连接，构成数学封装的基本义务。

本章采用几个基础逻辑模型展开这些关系。它们用于说明工作机制，不作为本书首次发现的数学定理，也不声称已经替代正式证明工具。模型的价值在于把一些容易混淆的判断条件明确写出来。

二、一个最小证明模块的组成

设一个模块M被表示为“在前提集合Γ下，可以得到结论P”，记作Γ⊢P。这里Γ包含当前证明实际允许使用的条件，符号⊢表达相应推导关系。要把它作为可靠模块使用，还需要关联支持这项推导的证明或验证依据。

对于实际研究，本书建议把模块记录扩展为：对象语境、前提、结论、证明依据、依赖版本、适用映射与当前状态。对象语境说明变量属于什么；适用映射说明当前任务中的对象怎样代入模块；状态则区分候选、条件性、已核验和需复核等情形。

不是每次调用都要把整份记录展示给人。它可以被系统保存，按层级提供摘要。比如上层显示“当前条件满足，依赖已核验”，需要时再展开具体前提与证明。这里的封装减少界面负担，却不应删除底层证据。

如果一个所谓模块只包含名称和自然语言结论，就可能只是一个待核对的知识条目，而不是完整证明封装。条目仍然有检索价值，但应以相应身份进入研究，不能因为名字看起来像成熟定理就自动跳过依据检查。

三、最简单的组合为什么也需要条件

假设模块M₁证明P蕴含Q，模块M₂证明Q蕴含R。那么在接受这两个模块依据的前提下，可以得到P蕴含R。论证是：任取满足P的情形，由M₁得到Q，再由M₂得到R。因为对任意满足P的情形都成立，所以得到所需蕴含。

这个简单组合依赖于两处Q具有相同含义。如果第一个模块的Q指某区间上的连续，第二个模块要求整个定义域上的连续，就不能仅凭都出现“连续”两个字进行连接。接口一致性既包括形式类型，也包括范围和定义。

进一步，若M₂实际上证明Q与H共同蕴含R，那么M₁与M₂只能支持P与H共同蕴含R，除非还能从已有条件得到H。组合并没有制造缺失前提。把两个可靠模块连起来，并不自动得到一个不需要额外条件的可靠整体。

这可以直接对应AI工作中的常见风险：上游摘要只输出Q，丢掉其适用范围；下游把Q作为更强条件使用，最终文本仍然流畅。每个局部句子都可能引用真实结果，但连接方式没有获得支持。此时问题不是某个模块内部证明不够长，而是接口判断缺席。

四、前提账本怎样避免条件凭空消失

设M₁在A与B下证明C，M₂在C与D下证明E。在不增加其他信息时，组合可以在A、B、D下证明E。B和D不能因为没有在最终推导最后一行出现，就从整体前提中删除。它们的作用已经进入中间结果。

可以给每个已得结论附上当前使用的前提集合。组合时取必要依赖的并集，再根据已有逻辑关系检查是否可以简化。若某个前提事实上多余，需要给出不依赖它的推导或相应消去依据，而不是由文本编辑器自行删去。

这个账本可以保守地记录较多条件。保守记录不一定给出最弱前提，却能够减少无依据增强结论的风险。寻找最弱前提是进一步的研究任务，不应与基础核验混成一项自动承诺。一个工具能追踪实际依赖，不等于它已经解决所有逻辑最小化问题。

另一方面，条件越多也不是越好。过多而无必要的前提会使模块难以使用，并遮蔽真正机制。成熟过程可以先确保不遗漏，再通过新的证明分析哪些条件能削弱或去掉。可靠与简洁之间应通过论证连接，而不是选一个口号替代另一个。

五、对象代入为什么不是简单替换字符串

一个关于实数a、b的引理，在代入具体表达式时，需要确认表达式属于相应对象范围。若引理要求a非零，代入a=g(x)以后，新的义务就是确认当前x满足g(x)非零。变量名称消失，不意味着条件消失。

设已知对a非零有ab=ac推出b=c。若把a代为x−1，就需要x不等于一。只检查代入后的公式外观，容易忽略这一义务。正确调用应让条件随代入一起变换，并进入当前任务的待证列表。

代入还可能带来变量依赖与作用域问题。某个对象在局部假设下定义，不能未经说明就移到全局；某个见证随参数变化，不能在模块接口中被写成统一常量。上一章量词次序的例子，在这里表现为接口中的依赖管理。

因此，证明封装的接口不只是输入输出类型，还包括条件如何随对象映射而变化。上层可以不看内部推导，却必须有机制确认这次代入实际满足接口。这正是封装之后仍然在运行的判断，而不是封装尚未完成的缺陷。

六、有限无环证明网络的条件性可靠性

为了进一步说明组合，可以考虑一个有限有向无环图。每个节点是一项结论，入边来自该结论使用的前提节点。基础节点具有已经接受的依据；其他节点附带一项局部推理，说明从其直接前驱可以推出自身。

在这些条件下，若所有局部推理在同一逻辑语境中有效，全部接口一致，则每个节点都能从基础节点推出。证明可以按图的拓扑顺序进行。没有入边的基础节点已经有依据；假设此前节点均已得到支持，当前节点的前驱也已得到支持，再用其局部推理即可得到当前结论。有限次继续，覆盖全部节点。

这个证明是对组合条件的展开。它没有证明实际图中每条边都正确，也没有保证基础公理适当，更没有保证目标表达符合研究意图。模型给出的只是：如果这些义务确实满足，整体连接为什么能够保持推导支持。

因此，工程实现的任务是让模型中的条件能够被检查，而不是仅仅把文稿画成一张漂亮的有向图。图上每个节点的身份、前提版本、局部依据和语义接口，都需要真实对应。绘图是显露工具，不能代替证明本身。

七、循环依赖与合法归纳不能混为一谈

如果M₁的唯一依据是M₂，而M₂的唯一依据又是M₁，那么两者互相引用并没有提供起点。把这个环保存成两个模块，也不能使其变成两个独立证据。循环的外观可能很有结构，实际仍然缺少依据。

但不能据此把所有递归和归纳证明都判为循环错误。数学归纳法包含基础情形与明确的推进规则；良基归纳依靠相应的下降或良基结构。它们不是在同一层级无条件地把目标当成前提，而是使用获得接受的推理原则组织依赖。

例如，要证明对所有非负整数n有命题P(n)，可以先证明P(0)，再证明任意n下P(n)蕴含P(n+1)，最后应用归纳原则。这里对较小情形的使用有明确范围与规则，不等于直接假设全部结论。封装记录应当保留这个结构。

所以，一个简化的模块管理原型可以拒绝未解释的循环依赖，却不能因此宣布所有有递归外观的正式证明无效。它需要把合法归纳作为单独、已验证的证明结构处理，或者把该部分交给能够检查其规则的工具。管理层的保守限制，不是数学逻辑的全部。

八、压缩证明与保留解释的两种需要

一个形式证明可能已经得到可靠核验，但人类读者仍然难以理解它为什么如此组织。反过来，一段解释可能使人迅速理解思路，却省略了必要边界。有效证明和可理解解释相关，却不能互相替代。

可以把同一个模块提供为不同视图。使用视图突出条件与结论；研究视图展示关键构造和依赖；教学视图解释为什么想到这一步；审查视图提供完整依据与版本。这些视图共享同一任务身份，而不是各自改写出不同命题。

封装的成熟因而不必追求一个适合所有人的唯一摘要。不同使用者在不同层级需要不同差异。一个专家可能只需确认条件，一个学习者需要展开关键推理，一个审查者需要核对基础依赖。界面应允许这种粒度差异，而不是把最简形式强加给所有任务。

解释还应能够反向约束模块。如果教学展开发现结论依赖此前未说明的条件，就不能只修改说明而保持底层完成状态不动。新的差异应返回正式记录，必要时触发复核。不同视图不是彼此隔绝的宣传材料，而是同一复合能力的不同进入方式。

九、版本改变以后，什么需要重新检查

一个模块的文字变化未必影响证明，但定义、前提、结论或依赖变化可能改变支持关系。系统不能仅按文件名判断同一性，也不必把每次空格调整都当作整个数学结果失效。需要说明哪些变化影响语义与依据。

设M依赖某个函数定义f。后来库中同名f的定义改变，原证明记录就不能只凭名称继续使用。最简单的工程办法是把依赖版本或内容标识与模块绑定，发现变化后将相关节点转为待复核。是否最终仍成立，需要再次检查，而不是由版本变化自动判假。

影响范围可以沿依赖图传播。直接依赖M的节点需要重新确认，通过它间接得到支持的节点也可能受影响；没有相关路径的独立模块则不必自动全部作废。这样既保护依据，也避免无差别重算。

版本记录同样要涵盖目标。一个经过核验的证明可以继续是正确的旧结果，但若研究者修改了目标，就需要说明旧模块是否仍然适用。旧结果存在，与当前任务完成，是两个不同判断。保存版本能够让两者同时清楚。

十、边界案例为什么应当进入模块的说明

一个模块在边界附近常常显露最容易被误用的条件。例如，要求严格正数与要求非负数在零处不同；闭区间与开区间在端点处不同；有限集合与可数集合在某些操作中不同。边界不是附属细节，而可能决定适用关系。

模块说明可以附上少量经过检查的正例与反例，帮助使用者理解边界。它们不能替代一般证明，却能够防止把结论记成过强的口号。比如说明“均匀条件不可随对象随意改变”，再给出一个量词错位的反例，会比单独重复定义更容易参与实际判断。

但例子需要与模块身份连接。一个反例否定的是哪一种删除条件后的命题，应写清楚；不能把它笼统标为“定理的反例”，仿佛已证定理本身被否定。知识封装要同时保存成立范围与越界后的失败方式。

这种说明还能支持创造。研究者在看见某个边界例子后，可以询问是否存在另一种条件替代原条件，或者是否能在较小对象范围内取得更强结论。边界不是永久禁止线，而是有依据地继续研究的起点。

十一、把困难移到引理里，不等于解决困难

研究中使用引理是合理的分层方法，但也可能成为隐藏缺口的方式。若主证明只写“由引理L可得”，而L与原目标实质等价且尚未证明，结构虽然变得整齐，困难却没有减少。需要检查依赖的内容，而不是只数已经创建多少模块。

一种更隐蔽的情况是把核心困难分成多个看似普通的小命题，其中某个连接实际上仍然承担全部原难点。模块多并不自动说明研究取得进展。判断应记录哪些义务已经闭合，剩余义务比原来明确了什么，是否获得了新的可行路线。

当然，即使尚未证明，找到准确的核心引理也可能有研究价值。它可以澄清任务、暴露必要结构或支持合作。问题不在于保留未证模块，而在于是否如实说明其状态，以及是否将结构澄清误报为证明完成。

因此，系统应允许“分解完成而证明未完成”“关键等价已证而核心命题开放”等细分结果。这些状态能使真实进展被看见，又不需要通过夸大成功来鼓励研究。诚实的部分结果是可积累的能力，不是需要被隐藏的失败。

十二、证明模块怎样支持不同路线的比较

当多个模块具有清楚接口，研究者可以比较不同证明路线的条件、代价与可理解性。某条路线条件较弱但实现复杂，另一条路线条件较强却结构透明。比较应说明当前研究目的，而不能只按长度排名。

例如，教学可能优先展示能显露关键机制的路线；自动验证可能重视稳定可检查的构造；进一步推广则关心哪些条件可以替换。这些选择都可以接受价值评估，不应由单一指标默默决定。

六路径在这里不是替代逻辑连接，而是组织研究从哪里进入。可以从已有目标倒查所需模块，也可以从新模块出发寻找可达目标，还可以从反复失败的尝试分析依赖条件。每条路径最终都需要返回清楚的证明义务。

三原理则可以帮助识别是否需要改变目标显露、推进路线或支撑条件。某次模块比较可能不只是选出较优方案，而是形成一种新的组合方式。新的结构若要成为可调用能力，仍需经历证明、核验与使用中的反馈。

十三、封装并不把数学共同体排除在外

一个证明模块的技术记录不能替代全部学术交流。不同研究者可能对问题意义、定义选择或表达方式有不同看法；某些领域知识尚未全部形式化；对新方法的理解也需要解释与讨论。封装应支持这些工作，而不是宣布它们已经不必要。

同时，共同体认可也不能自动代替每一项逻辑依据。声望可以提供检索和注意分配的线索，却不能使缺失前提变得多余。技术检查与同行判断具有不同支持范围，恰当的复合系统应使它们相互补充，而不是寻找一个永久包办全部义务的权威。

后来者能够调用前人的证明成果，是文明积累的重要能力。但可调用不等于不可质疑。新的问题可能要求重新展开旧证明，检查更弱条件，甚至发现先前未被注意的边界。封装的传递与重新打开，在数学中也应同时成立。

本书的贡献若要具体，就应帮助设计这种传递：哪些信息需要随模块保留，哪些状态可以整体显示，什么事件触发回查，以及新发现怎样进入后续使用。它不需要把所有数学实践重新命名，才可能在这些接口上增加价值。

十四、从证明网络到复合能力

一个模块库不等于一套会研究的系统。只有当模块能够被恰当检索、映射、连接、检查和修订，它们才进入当前的判断能力。已经保存的知识，必须被接入实际任务，才能成为可使用的历史承接。

同样，研究者也在这种使用中改变。他可以从检查单个引理转向比较依赖结构，又在遇到边界时回到内部证明。粒度的上升与下降不是能力进退的简单刻度，而是围绕新问题组织差异的动作。

封装因此既保存已有成果，也为新的发生提供材料。它让过去的一段证明过程成为现在的一个使用单位；新的组合又暴露原来尚未成为问题的关系。判断力的复合发生，在这里具有可以逐项检查的结构。

引理作为一个整体被使用，并不意味着它的成立条件从此隐去。恰当接口使过去的推导成为当前可用的单位，同时让调用条件继续接受检查。研究者可以从这些单位出发组合新结构，也可以为了推广重新打开它们。证明封装由此具有历史与当次两个尺度：历史支持工具和模块的使用，当前依据支持这一命题的接受。