个体变量指派函数

$$ \sigma x\rightarrow d =\left{\begin{align} & d & \mathrm{when} \ y=x \ & \sigma(y) & \mathrm{when} \ y \neq x \end{align}\right. $$

直观理解: $y$ 中所有的 $x$ 项赋为 $d$

解释

已知一阶逻辑公式の

• 非逻辑符号集 $\mathcal{L}$
• 个体变量集 $V$
• 论域 $D$
• 一个 个体变量指派函数 $\sigma: V\rightarrow D$

则 $\mathcal{L}$ 的一个解释 $\mathcal{M}$ 是 $[![t]!]_{\sigma}$ $:=$

• $[![c]!]_{\sigma}=c$
• $[![x]!]_{\sigma}=\sigma(x)$
• $[![f(t_{1},\dots,t_{n})]!]_{\sigma}= ![f]! $

直观理解: 一个解释 $\mathcal{M}$ 是对公式中所有

• 函数 $f$
• 谓词 $F$
• 个体常量 $c$ の一个赋值

真值问题

详见 谓词逻辑等值式模式

例化

在 $D$ 为有限集时应用以下规则求一阶逻辑公式真值

1. $$\exists xF(x)=\bigvee_{a\in D}\sigma x\rightarrow a =\bigvee_{a\in D}F(a)$$

2. $$\forall xF(x)=\bigwedge_{a\in D}\sigma x\rightarrow a =\bigwedge_{a\in D}F(a)$$

换序

1. $\forall x\forall yF(x,y)\equiv \forall y\forall xF(x,y)$
2. $\exists x \exists y F(x,y)\equiv \exists y\exists xF(x,y)$
3. $\forall x\exists yF(x,y) \nRightarrow \exists y\forall xF(x,y)$
4. $\exists x\forall yF(x,y) \Rightarrow \forall y\exists x F(x,y)$