代入規則

代入規則

目錄

正文


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