查看“︁演绎”︁的源代码

{{InfoBox
|name=演绎
|eng_name=deduction
}}
{{InfoBox
|name=可演绎的
|eng_name=deducible
}}
'''演绎'''('''deduction''')指某个推理系统的变形规则下，从一些前提到某一结论的一系列步骤。
对应地，这个步骤的存在性被称为'''可演绎'''('''deducible''')。

== 定义 ==

在指定[[形式化公理系统（逻辑）|形式化公理系统]] <math>\mathbf{H}</math> 中，对指定公式集 <math>\Gamma</math> 和公式 <math>\phi</math> ，满足下列条件的公式序列 <math>\phi_0, \phi_1, \dots, \phi_n</math> ：
* <math>\phi_n = \phi</math>；
* 对任意 <math>k < n</math>， <math>\phi_k</math> 符合以下任一条件：
** 是 <math>\mathbf{H}</math> 中的公理；
** 是 <math>\Gamma</math> 中的元素；
** 能运用 <math>\mathbf{H}</math> 中的推理规则从 <math>\phi_0, \dots, \phi_{k-1}</math> 得到。
则称公式序列 <math>\phi_0, \phi_1, \dots, \phi_n</math> 是 <math>\mathbf{H}</math> 中从公式集 <math>\Gamma</math> 到公式 <math>\phi</math> 的一个'''演绎'''('''deduction''')。

对任意公式集 <math>\Gamma</math> 和公式 <math>\phi</math> ，若存在 <math>\mathbf{H}</math> 中从 <math>\Gamma</math> 到 <math>\phi</math> 的演绎，则称 <math>\phi</math> 是 <math>\mathbf{H}</math> 中从 <math>\Gamma</math> '''可演绎的'''('''deducible''')，记作 <math>\Gamma \vdash \phi</math>。
对 <math>\Gamma=\{\psi_1,\psi_2,\dots,\psi_m\}</math> 时也记作 <math>\psi_1,\psi_2,\dots,\psi_m \vdash \phi</math>。
此时，<math>\Gamma</math> 的元素称为'''假设'''('''hypothesis''')或'''前提'''('''premise''')， <math>\phi</math> 称为<math>\mathbf{H}</math> 中 <math>\Gamma</math> 的'''演绎结论'''或'''演绎后承'''('''deductive consequence''')。


{{逻辑演算}}