查看“︁推理规则”︁的源代码

{{multiple issues|
{{disputed|time=2019-06-18T15:19:32+00:00}}
{{expert|time=2019-06-18T15:19:32+00:00}}
{{unreferenced|time=2019-06-18T15:19:32+00:00}}
}}
在[[逻辑]]中，特别是[[数理逻辑]]中，'''推理规则'''（推论规则）是构造有效[[推论]]的方案。这些方案建立在一组叫做'''前提'''的公式和叫做'''结论'''的断言之间的[[语法]]关系。这些语法关系用于推理过程中，新的真的断言从其他已知的断言得出。规则也适用于[[非形式逻辑]]和[[逻辑论证]]，但是形式化更加困难和有争议。

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

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

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

在[[形式逻辑]]的设置（和很多有关领域）中，推理规则通常用如下形式给出：

 前提#1
<br> 前提#2
<br> '''...'''
<br><u> 前提#n </u> 
<br> 结论

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

 A→B
<br><u> A   </u>
<br> B

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

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

==可接纳性和可推导性==

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

:<math>
\begin{matrix}
\frac{}{\mathbf{0} \,\,\mathsf{nat}} &
\frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\
\end{matrix}
</math>

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

:<math>
\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}
</math>

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

:<math>
\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}
</math>

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

:<math>
\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}
</math>

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

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

==其他考虑==

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

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

或者用更少的技术术语：

规则是关于系统的陈述，公理是系统内的陈述。例如：
*规则从<math>\vdash p</math>推出<math>\vdash Provable (p)</math>是个陈述，声称如果你已经证明了p则p是可证明的（通常是合理的主张）。
*公理<math>p \to Provable (p)</math>将意味着所有真的陈述都是可证明的（通常不是个合理的主张）。

在证明论中，推理规则在[[逻辑演算]]比如[[相继式演算]]和[[自然演绎]]的规定中扮演了关键角色。

==参见==
*[[命题演算]]
*[[自然演绎]]
* {{link-en|推理规则列表|List of rules of inference}}

{{数理逻辑}}

[[Category:推理规则| ]]
[[Category:命题演算]]
[[Category:形式系统]]
[[Category:句法 (逻辑学)]]
[[Category:邏輯真理]]
[[Category:推論]]
[[Category:逻辑表达式]]