直接证明

直接证明是所有证明策略里最朴素的一种：顺着定义向前走。它不改造目标的逻辑形状（不取否定、不换质换位），而是把假设拆开——$P$ 说了什么？涉及的名词按定义展开是什么？——再把这些原材料逐步组装成 $Q$ 需要的形状。实际书写时常配合"由后向前"的草稿分析：先看 $Q$ 按定义需要交付什么，再回头检查假设能供应什么，两头凿通后按正向次序誊写。这个模式最防不胜防的失败方式不是推错，而是"用词代替推理"：把某步标注为"显然"，实际上跳过了唯一需要论证的环节。可靠的操作准则是：每一步要么是定义展开，要么是已证结果的实例化，要么是初等的逻辑组装；凡不属于这三类的句子都欠着一笔账。

直接证明从已知假设出发，沿定义、已知定理和合法推理逐步到达结论，不改变命题的逻辑形态。它最适合结论能由假设中的结构显式构造或计算出来的情形。直接并不等于短，也不排斥引理；关键是没有把目标替换为逆否或矛盾。

正例（偶数和）：设 $a,b$ 为偶数。按定义存在整数 $m,n$ 使 $a=2m$、$b=2n$，于是

而整数对加法封闭保证 $m+n\in \mathbb{Z}$，故 $a+b$ 是偶数。麻雀虽小，结构俱全：展开定义（偶数即二倍整数）、代数运算、再收拢回定义——最后一步"$m+n$ 是整数"看似多余，恰是把结果重新装回"偶数"定义所必需的核查。稍进一层的例子是整除公理库整除Divisibility存在整数倍关系时定义的二元关系。的传递性：$a\mid b$ 且 $b\mid c$ 时写 $b=ak$、$c=bl$，代入得 $c=a(kl)$，同一套"展开—组装—回填"的节奏。

边界情形之一：验证有限多个数值样本不是直接证明——检查 $n=1,\dots ,{10}^6$ 都满足某性质，对 $\mathrm{\forall }n$ 的命题只是证据；"设 $n$ 任意"与"取一批具体的 $n$"之间隔着全称量词。之二："任意"元素在推导中途不得被追加特殊性：证明中若写"不妨设 $x$ 是有理数"，除非配上对无理情形的补证或对称性理由，全称结论即告失效。之三，并非所有命题都顺手：目标形如否定（"$\sqrt{2}$ 不是有理数"）或本身缺乏可展开结构时，反证法公理库反证法Proof by contradiction · Reductio ad absurdum假设目标命题为假并推出矛盾，从而证明目标。或逆否证明公理库逆否证明法Proof by contrapositive通过证明 ¬Q→¬P 来证明 P→Q。往往更直接——策略选择本身是证明设计的一部分。

证明“两个偶数之和为偶数”：写 $a=2m,b=2n$，则 $a+b=2(m+n)$。证明集合包含关系 $A\cap B\subseteq A$ 时，任取 $x\in A\cap B$，由定义立即得 $x\in A$。若命题本质是不存在性，硬做直接构造可能比反证或逆否更绕。

直接证明是其余证明技术的底座与默认选项：分情形证明公理库分类讨论证明Proof by cases · Exhaustion把所有可能情形穷尽划分并在每个情形中证明结论。在每个分支内部执行的是直接证明，数学归纳法公理库数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。的归纳步"假设 $P(n)$ 证 $P(n+1)$"同样是一段直接证明，逆否与反证不过是先变换目标再回到直接模式。代数恒等式、集合包含关系（"设 $x\in A$，证 $x\in B$"）、函数单调性与闭包性质的验证是它的主场。计算机科学中，算法正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。论证里"循环不变式公理库循环不变式Loop invariant在循环初始化后成立，并在每次循环迭代后继续成立的断言。在一次迭代后保持"正是标准的直接证明义务；程序验证工具生成的多数证明义务也按"假设前置条件，推出后置条件"的直接格式陈列。写作规范上，成熟的直接证明会在关键步骤点明所援引的定义或定理名，使每一步都可独立核查。

肯定前件与全称实例化构成直接推理的基本步骤，存在唯一性证明中的存在部分常要求直接构造见证。选择直接证明还是逆否证明，取决于哪一侧的定义更容易展开。