演绎定理

逻辑演算中的一个重要的元定理，是一个重要的导出的推演规则：如果有某一个推演，就有另一个推演。在命题演算中，演绎定理是说：如果从A，…，An可推出B，那么从A，…，A可推出A→B。在谓词演算中，因为涉及对自由个体变元概括问题，比较复杂一些，有附加限制性条件：如果从A，…，A，B可推出C，并且在推演过程中B保持不变，则从A，…，A可推出B→C。条件“在推演过程中B保持不变”，是指：在推演过程中对那些依赖B的公式应用全称概括规则时，不以B中的自由个体变元作量化变元。应用演绎定理，可以使定理的证明变得简捷容易。例如，很容易证明，从p→q，q→r，p可以推出r，3次应用演绎定理，就可证明：(p→q)→((q→r)→(p→r))。这比不用演绎定理直接证明(p→q)→((q→r)→(p→r))要容易得多。