演绎

演绎
术语名称	演绎
英语名称	deduction

可演绎的
术语名称	可演绎的
英语名称	deducible

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

定义

在指定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中，对指定公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi }[/math] ，满足下列条件的公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] ：

[math]\displaystyle{ \phi_n = \phi }[/math]；
对任意 [math]\displaystyle{ k \lt n }[/math]， [math]\displaystyle{ \phi_k }[/math] 符合以下任一条件：
- 是 [math]\displaystyle{ \mathbf{H} }[/math] 中的公理；
- 是 [math]\displaystyle{ \Gamma }[/math] 中的元素；
- 能运用 [math]\displaystyle{ \mathbf{H} }[/math] 中的推理规则从 [math]\displaystyle{ \phi_0, \dots, \phi_{k-1} }[/math] 得到。

则称公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中从公式集 [math]\displaystyle{ \Gamma }[/math] 到公式 [math]\displaystyle{ \phi }[/math] 的一个演绎(deduction)。

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

性质

[math]\displaystyle{ \Gamma\vdash B }[/math] 且 [math]\displaystyle{ \Gamma\subseteq\Delta }[/math] 则 [math]\displaystyle{ \Delta\vdash B }[/math] 。
演绎定理： [math]\displaystyle{ \Gamma,A\vdash B }[/math] 当且仅当 [math]\displaystyle{ \Gamma\vdash A\rightarrow B }[/math] 。
切消定理： [math]\displaystyle{ \Gamma \vdash A }[/math] 且 [math]\displaystyle{ \Gamma,A\vdash B }[/math] 则有 [math]\displaystyle{ \Gamma\vdash B }[/math] 。
前提为空，即 [math]\displaystyle{ \Gamma=\varnothing }[/math] 时，演绎被称为证明。

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性