演绎定理,是数理逻辑中的元定理。
在数理逻辑中,演绎定理声称如果公式 F 演绎自 E,则蕴涵 E → F 是可证明的(就是或它可以自空集推导出来)。用符号表示,如果 E \vdash F ,则 \vdash E \rightarrow F 。
演绎定理可以推广到假定公式的可数序列,使得从
E_1, E_2, ... , E_, E_n \vdash F ,推出 E_1, E_2, ... , E_ \vdash E_n \rightarrow F ,等等直到
\vdash E_1\rightarrow(...(E_ \rightarrow (E_n \rightarrow F))...) 。
演绎定理是元定理: 在给定的理论中使用它来演绎证明,但它不是这个理论自身的一个定理。
这个定理的逆命题也成立。
数学理科