定義置換規則

定義置換規則（rule of definitional replacement）某些形式系統中定義的左右兩方（定義項與被定義項）可以相互代換的規則。置換規則只要求在公式中多次出現被替換項時，替換可以只在某一位置上進行；代入規則卻要求，變項在被替換的公式中出現的一切位置上，要處處進行替換。