演绎定理

演绎定理
术语名称	演绎定理
英语名称	deduction theory,DT

演绎定理(deduction theory，DT)是重要的元定理。在希尔伯特系统中，由mp规则、Cut定理及前两条公理即可得出，且其中必要性方向仅依赖演绎定义和mp规则；在自然演绎系统中则对应于蕴含引入及消去。因此适用于绝大多数常见推理系统。

定理

对公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi,\psi }[/math] ，有： [math]\displaystyle{ \Gamma, \phi \vdash \psi }[/math] 当且仅当 [math]\displaystyle{ \Gamma \vdash \phi\rightarrow\psi }[/math] 。

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