代入規則

一個變元在一公式中可能不只出現一次，如果用某一公式B代入該變元，那麼，在這公式裏，在該變元出現的一切位置上，都必須用B替換。在命題演算中，只有命題變元，所以只有命題變元代入規則。但在狹謂詞演算中，有個體變元、命題變元和謂詞變元，所以它就有關於個體變元、命題變元和謂詞變元的三個代入規則。在有些邏輯系統中，如果用公理圖式去替代公理時。變形規則中就沒有代入規則 ^[1]  。