谓词逻辑

谓词

就是返回 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] $$