谓词逻辑
谓词
就是返回 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] $$