推导规则

在逻辑学中, 推导规则是句法意义下从前提得到结论的一些规则.

1语法

对于命题 $p_1,\dots ,p_n,q$,$$\frac{p_1\dots p_n}{q}$$表示 “$p_1,\dots ,p_n$ 可以推导出 $q$”, $p_k$ 是前提, $q$ 是结论.

推导规则可以压缩为相继式. 上面的推导规则可以用相继式写作

$$p_1,\dots ,p_n⊢q$$

在描述逻辑时, 需要描述该逻辑允许什么样的推导规则, 而这需要借助推导规则的推导规则实现, 这写起来会比较难以阅读, 所以内层的推导规则往往被压缩为相继式.

2例子

•	肯定前件: $$\frac{\Gamma ⊢\chi \to \phi \Gamma ⊢\chi }{\Gamma ⊢\phi }$$

这个推导规则说的是, 若在语境 $\Gamma$ 下, $\chi \to \phi$ 成立, 且 $\chi$ 也成立, 那么 $\phi$ 成立.

又见:

•	结构性规则是大部分逻辑都具有的规则 (例外是亚结构逻辑, 例如线性逻辑),

•	相继式演算与自然演绎.

3相关概念

借助推导规则, 可以形式化定义什么是 “证明”:

一段演绎是一个有限树, 每一个节点是一个相继式, 节点之间的关系满足一些推导规则. 证明是一种抽象的概念, 而演绎可以看作是一种证明. 在研究逻辑时, 演绎往往是唯一考虑的证明, 因此也可以把演绎直接称为证明.

如果存在一段演绎使得其全部的分支的前提总是没有条件的命题、而最终结论是 $p$, 我们就认为命题 $p$ 成立.

术语翻译

推导规则 • 英文 inference rule • 日文 推論規則