推理规则 · aiwiki.page

推理规则是一种模式化的指令，规定如何在形式系统中从前提推出结论。在逻辑学中，这类规则构成了演绎推理的各个步骤：它们规定证明可以如何进行，而不只是列出被接受为真的陈述。形式证明由这些规则的应用构成，从假设或公理出发，最终得到待证命题。规则可以作用于公式、判断或可推导性陈述。(cs.cmu.edu)

形式与解释

推理规则通常将前提写在横线上方，将结论写在下方：

\frac{A_1\quad A_2\quad\cdots\quad A_n}{B}.

其中的字母通常代表相应类型的任意表达式。因此，这种写法描述的是一类允许的推理步骤，而不只是某一个论证。应用规则时，必须将其前提和结论一致地匹配到具体表达式，并满足所有附加限制。证明可以写成由这些规则应用构成的树，也可以写成带编号的各行，并引用先前的步骤。(leanprover.github.io)

例如，肯定前件式具有以下形式：

\frac{A\qquad A\to B}{B}.

给定“开关已闭合”和“如果开关已闭合，那么灯亮着”，这条规则允许推出“灯亮着”。规则关注的是论证的形式，并不判定任何一个前提是否准确描述了某盏具体的灯。这里，联结词 $\to$ 表示实质蕴涵，而推理横线则表示可以从上方的陈述推到下方的陈述。(leanprover-community.github.io)

公理提供一个起始陈述，而推理规则通常规定一个推导步骤。不过，在更一般的表述中，公理本身也可视为一条没有前提的规则。公理模式则规定了一族这样的起始陈述。(cs.cmu.edu)

命题规则与假设的解除

在命题逻辑中，规则作用于由合取、析取、蕴涵、否定等联结词构成的公式。自然演绎将其中许多规则分为引入规则和消去规则：前者用于建立含有某个联结词的陈述，后者说明如何使用含有该联结词的陈述。对于合取，这些规则包括：

\frac{A\qquad B}{A\land B}, \qquad \frac{A\land B}{A}, \qquad \frac{A\land B}{B}.

析取引入允许从 $A$ 推出 $A\lor B$ ，但析取消去要求分情况推理：分别假设 $A$ 和假设 $B$ ，都必须能推出同一个结论。仅仅知道 $A\lor B$ ，并不能确定究竟哪一种情况成立。(leanprover.github.io)

有些规则作用于整个子推导。蕴涵引入允许在推出 $B$ 后解除临时假设 $A$ ：

\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}.

这里， $\Gamma$ 表示其余假设， $\vdash$ 表示形式上的可推导性。解除假设意味着，所得的条件命题不再依赖于将该假设作为独立接受的前提。这种对假设依赖关系的记录，将条件证明与毫无依据地断言其后件区分开来。(leanprover-community.github.io)

在经典逻辑中，双重否定消去允许从 $\neg\neg A$ 推出 $A$ 。类似地，经典反证法允许在假设 $\neg A$ 后推出矛盾，进而得出 $A$ 。这些不加限制的原则在直觉主义逻辑中通常不被接受。在通常的直觉主义规则基础上，它们与排中律 $A\lor\neg A$ 可以相互推导。(leanprover.github.io)

量词与附加条件

一阶逻辑增加了量词规则。全称消去允许从全称量化的公式推出它的一个实例：

\frac{\forall x\,P(x)}{P(t)}.

项 $t$ 必须能够代入而不导致意外的变量捕获。全称引入要求，被概括的变量不得自由出现于任何尚未解除的假设中：推导必须针对任意对象，而不是受某个特殊前提约束的对象。(leanprover-community.github.io)

存在引入从一个适当的实例 $P(t)$ 推出 $\exists x\,P(x)$ 。存在消去允许使用一个满足 $P$ 的新代表对象进行推理，但最终结论不得依赖于该代表对象的具体身份。对代表对象必须是新的这一要求，以及对假设的限制，都是规则的必要组成部分，而非可有可无的约定。(leanprover-community.github.io)

可靠性与完备性

规则属于证明系统的句法描述；也可以通过语义学研究它们的合理性。对于通常保持真值的演绎而言，如果一条规则在相关解释下不可能从真前提推出假结论，那么它就是可靠的。在经典命题逻辑中，可以用真值表检验这一条件。因此，逻辑有效性涉及解释，而可推导性涉及可用的形式规则。(leanprover.github.io)

当一个系统满足

\Gamma\vdash A\quad\Longrightarrow\quad\Gamma\models A,

时，它具有可靠性；当反方向也成立时，它具有完备性。符号 $\models$ 表示语义后承关系。标准的经典命题演算同时满足这两项性质；相应的一阶逻辑结果由哥德尔完备性定理表述。完备性关注的是一个演算整体的推导能力，而不是某一条规则单独是否足够。(leanprover.github.io)

派生规则与机械化证明

证明论区分原始规则与派生规则；派生规则的应用，是对已有步骤的组合所作的简写。可容许规则保证，只要其前提可推导，其结论也可推导；不过，可容许性不一定意味着存在一个从假定前提出发的固定推导。这些区别取决于具体的演算。(cs.cmu.edu)

在证明助手中，推理模式可以表示为对证明对象的操作。根据柯里—霍华德对应，命题表示为类型，证明表示为项：蕴涵消去对应于将函数应用于一个实参。例如，Lean证明助手通过两个分量各自的证明来构造合取的证明，以此表示合取引入；通过提取任一分量的证明来表示合取消去。随后，已命名的定理便可以作为可重复使用的推理模式，而不必成为新的原始逻辑规则。(leanprover.github.io)