代入

代入是謂詞演算的基本運算之一。代入的一個重要特徵是，代入必須是處處代入，即用一個項 t 代入一個自由變元 x ，必須用 t 代替 x 在公式中所有的自由出現。

定義

在某個形式語言中，一個元素中某個出現（子項）被另一個元素項所代換。

例如，s 為一個項，x 為 s 中的（子）項，於是 s 可寫成。如果用另一個項 a 代替 x ，即變為。這時就說是用 a 代入的結果。有時可將這個代入的結果寫成或。

如果 s 中的 n 個項被另外 n 個項代替，這樣代入的結果可寫成。

假定為任一公式，A為非空集。如果對一切，存在唯一的y使得成立，則存在定義域為A的函式f，使得對一切，成立。這就是替換引理。

代入消元法是將方程組中的一個方程的未知數用含有另一個未知數的代數式表示，並代入到另一個方程中去，這就消去了一個未知數,得到一個解。代入消元法簡稱代入法。