推理规则

维基百科，自由的百科全书

在逻辑中，特别是数理逻辑中，推理规则(推论规则)是构造有效推论的方案。这些方案建立在一组叫做前提的公式和叫做结论的断言之间的语法关系。这些语法关系用于推理过程中，新的真的断言从其他已知的断言得出。规则也适用于非形式逻辑和逻辑论证，但是形式化更加困难和有争议。

按照规定，推理规则的应用纯粹是语法过程。尽管如此它必须是有效的，或者更精确的说保持有效性。为了使保持有效性的要求有意义，某种形式的语义与推理规则有关和推理规则自身的断言是必需的。对于在推理规则和和语义之间相互关系的讨论请参见命题逻辑。

命题逻辑中推理规则的显著例子是肯定前件和否定后件规则。对于一阶谓词逻辑，推理规则需要处理逻辑量词。对这种论证的更详细的描述请参见有效性。在一阶谓词逻辑中把所有推理规则作为一个单一规则来统一处理请参见一阶归结。

注意有很多不同的形式逻辑系统，每个都带有合式公式、推理规则和语义的自己的集合。参见时间逻辑、模态逻辑或直觉逻辑的实例。量子逻辑也是不同寻常的逻辑的一种形式。参见证明论。在谓词演算中，需要一个补充的推理规则。它叫做普遍化。

在形式逻辑的设置(和很多有关领域)中，推理规则通常用如下形式给出:

前提#1
前提#2
...
前提#n 
-------
结论

这个表达式声称，在某个逻辑推导期间已经获得了给定前提，同样可以认可特定结论。用来描述前提和结论二者的的精确的形式语言依赖于推导的实际上下文。在一个简单的情况下，你可以使用逻辑公式，比如

A→B
A
-------
B

它是命题逻辑的肯定前件规则。推理规则通常通过使用全称变量而公式化为规则模式。在上面的规则(模式)中，A 和 B 可以被实例化为论域(有时约定为某种受限制的子集比如命题)的任何元素，来形成推理规则的无限集合。

证明系统形成自一组规则，它们可以被链接在一起形成证明或推导。任何推导都只有一个最终结论，它是要证明或推导的陈述。如果在推导中留下了未满足的前提，则推导就是假言陈述: "如果前提成立，那么结论成立"。

[编辑] 可接纳性和可推导性

在规则的集合中，一个推理规则可能是多余的，在它是“可接纳的”或“可推导的”的意义上。一个可推导规则是可以使用其他规则从它的前提推导出它的结论的规则。可接纳规则是只要前提成立结论就成立的规则。所有可推导规则都是可接纳规则。要鉴别它们的区别，考虑定义自然数的下列规则集合(判断 $n\,\,\mathsf{nat}$ 断言 $n$ 是自然数的事实):

$\begin{matrix} \frac{}{\mathbf{0} \,\,\mathsf{nat}} & \frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \end{matrix}$

第一个规则声称 0 是自然数，第二个声称 s(n) 是自然数，如果 n 是自然数。在这个证明系统中，下列规则示范了自然数的第二个后继者也是自然数，是可推导的:

$\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}$

它的推导只是上述后继规则的两次使用的复合。下列规则断言任何非零自然数有前驱者存在，只是可接纳的:

$\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}$

这是自然数的事实，并可以通过数学归纳法证明。(要证明这个规则是可接纳的，你可以假定这个前提的一个推导，并在其上归纳出生成 $n \,\,\mathsf{nat}$ 的推导)。但是，它不是可推导的，因为它依赖于前提的推导的结构。为此“可推导性”在增加到证明系统下是稳定的，而“可接纳性”不是。要看出区别，假设下列无意义规则被增加到证明系统:

$\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}$

在这个新系统中，双后继规则仍是可推导的。但是，找到前驱者的规则不再是可接纳的，因为没有方式来得到 $\mathbf{-3} \,\,\mathsf{nat}$ 。可接受性的脆弱来自它被证明的方式: 因为这个证明可以归纳于前提的推导的结构上，对系统的扩展向这个证明增加了新情况，而它可能不再成立。

可接纳规则可以被认为是一个证明系统的定理。例如，在相继式演算中切消成立，“切”规则是可接纳的。

[编辑] 其他考虑

推理规则也可以用如下形式陈述: (1) 某些(可能为零)前提，(2)十字转门(turnstile)符号 $\vdash$ ，它意味着"推出"、"证明"或"得出"，(3) 一个结论。十字转门符号化了执行能力。蕴涵符号 $\rightarrow$ 没有这种能力: 它只指示潜在的推理。 $\rightarrow$ 是另一个逻辑运算符，它运算于真值之上。 $\vdash$ 不是逻辑运算符。它是一个催化剂，代谢真陈述来建立新陈述。

推理规则必须区别于一个理论的公理，它是被假定为真而无须证明的断言。依据语义，公理是有效的断言。公理通常被当作应用推理规则和生成一组结论的起点。注意在推理规则和公理之间没有明确的区别，在规则可以被人工编码为公理或反之的意义上。例如，一个规则的前提的集合可以为空，所以结论总是为真。反过来说，一个公理通常假定是一个单一子句，但是实际上你可以指定生成一个公理的无限集合的模式，它浅薄的有着和推理规则有一样的形式。

或者用更少的技术术语:

规则是关于系统的陈述，公理是系统内的陈述。例如: