定义置换规则

定义置换规则（rule of definitional replacement）是某些形式系统中定义的左右两方（定义项与被定义项）可以相互代换的规则。置换规则只要求在公式中多次出现被替换项时，替换可以只在某一位置上进行；代入规则却要求，变项在被替换的公式中出现的一切位置上，要处处进行替换。