谓词逻辑
谓词
就是返回 bool 的函数
量词
就是 $\forall$ 和 $\exists$。
注意量词的优先级比 $\wedge$ 和 $\vee$ 高，例如：$\forall x A \wedge B$ 意思是 $(\forall x A) \wedge B$
substitution（替换）
设有一个式子 $A$，其中有一个变量 $x$，给定一个项 $t$，用 $t$ 替换所有自由出现的 $x$ 的操作称为一次 substitution，记作：
$$ A[t/x] $$
就是返回 bool 的函数
就是 $\forall$ 和 $\exists$。
注意量词的优先级比 $\wedge$ 和 $\vee$ 高，例如：$\forall x A \wedge B$ 意思是 $(\forall x A) \wedge B$
设有一个式子 $A$，其中有一个变量 $x$，给定一个项 $t$，用 $t$ 替换所有自由出现的 $x$ 的操作称为一次 substitution，记作：
$$ A[t/x] $$