演绎定理

在数理逻辑中，演绎定理声称如果公式 F 演绎自 E，则蕴涵 E → F 是可证明的(就是或它可以自空集推导出来)。用符号表示，如果 <math> E vdash F </math>，则 <math> vdash E

ightarrow F </math>。

演绎定理可以推广到假定公式的可数序列，使得从

<math> E_1, E_2, ... , E_{n-1}, E_n vdash F </math>，推出 <math> E_1, E_2, ... , E_{n-1} vdash E_n

ightarrow F </math>，等等直到

<math> vdash E_1

ightarrow(...(E_{n-1}

ightarrow (E_n

ightarrow F))...) </math>。

演绎定理是元定理: 在给定的理论中使用它来演绎证明，但它不是这个理论自身的一个定理。

这个定理的逆命题也成立。