| 定义置换规则 rule of definitional replacement 某些形式系统中定义的左右两方(定义项与被定义项)可以相互代换的规则。例如在某些以，∨为初始联结词的系统中： p→q定义为p∨q p∧q定义为(p∨q) 在前出现的p→q，p∧q为被定义项，p∨q和(p∨q)分别为它们的定义项。在这种情况下，当某个公式中出现p→q时，可用p∨q去置换;出现p∧q时，可用(p∨q)去置换。定义置换规则和代入规则是有区别的。置换规则只要求在公式中多次出现被替换项时，替换可以只在某一位置上进行;代入规则却要求，变项在被替换的公式中出现的一切位置上，要处处进行替换。 |