谓词逻辑

定义

$n$ 元谓词 $R_n(x_1,\cdots ,x_n)$ 中每个 $x_i$ 叫作个体。如果每个个体都是常量、变量或者函数，就叫作一阶谓词，如果阶数最高的那个 $x_i$ 是 $k$ 阶谓词，则 $R_n$ 叫作 $k+1$ 阶谓词。

IMPORTANT

谓词的阶是从 $1$ 开始编号的，一阶谓词没有被 R 过。而常见的自由 $T$ 代数 $G$ 中 $G_n$ 的 $n$，或是 $T$ 中函数的阶，都是从 $0$ 开始编号的。

相比命题逻辑，还增加了存在量词和全称量词。

变元和项

所有个体变元 $x$ 构成个体变元集 $X$。所有个体常元 $c$ 组成个体常元集 $C$，它们也是 $T_0$ 的元素。项集 $I$ 是 $X\cup C$ 通过 $T$ 中的 $i$ 元运算 $f_i^{(j)}$ 得到的东西，其中不含个体变元的称为闭项。

集合 $\left\{f_i^{(j)}\right\}$ 叫作函数词集合。

谓词和原子公式

谓词 $R_n(t_1,\cdots ,t_n)$ 是一个 $n$ 元关系，其中 $t_i\in I$。谓词逻辑中的原子公式是给谓词中的 $t_i$ 以确定的个体得到的公式，比如 $R_n$ 是一个谓词，但是 $R_n(x_1,c_3,c_2,x_9)$ 是一个原子公式。不含个体变元的公式称为闭式。

NOTE

谓词和原子公式的关系类似函数和函数值的关系。

谓词公式和谓词代数

谓词代数 $P$ 是原子公式集 $Y={\bigcup }_{R_n}\{R_n(t_1,\cdots ,t_n):t_i\in I\}$ 上的自由 $T$-代数，其中 $T=\{F,\to ,\forall x:x\in X\}$。把 $P(Y)$ 叫作谓词公式集，里面的每个公式叫作谓词公式。谓词公式不是谓词。

IMPORTANT

谓词代数和项集都是自由 $T$ 代数，但是它们的生成集不同，$T$ 也不同。

项集 $I$ 的生成集是个体集 $X\cup C$，$T$ 是函数词集合 $f_i^{(j)}$，$I$ 中是所有的项；

谓词代数 $P$ 的生成集是原子公式集 $Y$，$T$ 是 $\{F,\to ,\forall x:x\in X\}$，$P$ 中是所有的谓词公式。

NOTE

不需要考虑 $\exists x$，因为可以定义 $\exists x:=\neg \forall x\neg$

量词深度和层次

谓词公式 $p$ 的

• 量词深度 $d(p)$：遇到 $\to$ 取两边最深的，然后每次增加一个真的起约束作用的 $\forall$ 就加 $1$
• 量词层次 $\ell (p)$：遇到 $\to$ 取两边最层的加 $1$，然后每次增加任意一个 $\forall$ 就加 $1$

TIP

遇到存在量词，需要先转成全称量词。

NOTE

例如，考虑 $p:=(\forall x(x\wedge y))\to (\forall y(x\wedge z))$，则 $d(p)=1$，而 $\ell (p)=2$

自由

变元的自由

如果有 $\forall x\dots$ 这样的式子，称 $x$ 在这个谓词公式中约束出现，否则是自由出现。

NOTE

例如，在谓词公式 $\forall x(x\wedge y)$ 中，$x$ 约束出现，而 $y$ 自由出现。

项的自由

设 $p(x)$ 是一个谓词公式，而 $x$ 是一个自由变元。如果一个项 $t\in I$ 替换掉 $x$ 之后，$t$ 里面的变元不会受到约束，就称 $t$ 对于 $x$ 自由。

NOTE

例如，设 $p:=\forall y(x\wedge a)$，则项 $t:=z\wedge y$ 对于 $p$ 中的 $x$ 不自由，因为用 $t$ 替换掉 $p$ 中的 $x$ 之后，$p$ 变成了 $\forall y(z\wedge y\wedge a)$，这时 $t$ 里面的变元 $y$ 受到了全称量词 $\forall y$ 的约束。

解释

解释域 $\mathcal{U}$ 负责把形式的个体常元集 $C$、函数词集合 $\{f_i\}$、谓词集合 $R$ 全都转换到论域 $U$ 上相关内容。

给定一个变元指派 ${\phi }_0:X\to U$，可以唯一产生一个项解释 $\phi :I\to U$。

NOTE

这里 $I$ 是 $X$ 生成的自由 $T$-代数，而 $U$ 是一个 $T$-代数。

对于谓词公式的赋值，只需要考虑原子公式即可，因为对原子公式的赋值可以唯一扩张为 $P(Y)\to {\mathbb{Z}}_2$ 的同态映射 $v$。定义对原子公式的赋值 $v_0(R_n(t_1,\cdots ,t_n))=[R_n^{\prime }(\phi (t_1),\cdots ,\phi (t_n))]$，其中 $t_i\in I$，而 $R_n^{\prime }$ 是解释域 $\mathcal{U}$ 把关系 $R_n$ 映到的另一个关系。

NOTE

可以说，有了项解释之后，谓词公式的赋值就确定了。

则 $v$ 满足运算规则：

$$\begin{array}{rlrl}v(p\to q)& =v(p)\to v(q)& & =1+v(p)(1+v(q))\\ v(\neg p)& =v(p\to F)& & =1+v(p)\\ v(p\vee q)& =v(\neg p\to q)& & =v(p)+v(q)+v(p)v(q)\\ v(p\wedge q)& =v(\neg (\neg p\vee \neg q))& & =v(p)v(q)\\ v(p\leftrightarrow q)& =v((p\to q)\wedge (q\to p))& & =1+v(p)+v(q)\\ v(\exists xp)& =v(\neg \forall x\neg p)& & =1+v(\forall x\neg p)\end{array}$$

NOTE

和命题逻辑中的演算规则差不多，多了一个 $v(\exists xp)$。

若 $\{p\}\models q$ 并且 $\{q\}\models p$，则称 $p$ 和 $q$ 语义等价 $p\models \mid q$。若 $p\models \mid q$，则 $\forall xp\models \mid \forall xq$，并可以推广至将一个谓词公式中任何 $p$ 的出现修改为 $q$ 前后两个谓词公式语义等价。

证明方法

一阶谓词的演算用 $Pred(Y)$ 表示。公理：

$$\begin{array}{rlrl}{\mathcal{A}}_1& :=p\to (q\to p)& & \\ {\mathcal{A}}_2& :=(p\to (q\to r))\to ((p\to q)\to (p\to r))& & \\ {\mathcal{A}}_3& :=\neg \neg p\to p& & \\ {\mathcal{A}}_4& :=\forall x(p\to q)\to (p\to \forall xq),& & x\notin var(p)\\ {\mathcal{A}}_5& :=\forall xp(x)\to p(t),& & t对p(x)中的x自由\\ MP& :=\{p,p\to q\}⊢q& & \end{array}$$

全称推广规则：对一般的 $x$ 证明 $p(x)$ 之后，有 $\forall xp(x)$。

演绎定理也成立。

可以使用的结论：

$$\begin{array}{rlrl}p\to q& \mid -\mid \neg p\vee q& & \\ p\leftrightarrow q& \mid -\mid (\neg p\vee q)\wedge (\neg q\vee p)& & \\ p\leftrightarrow q& \mid -\mid (p\wedge q)\vee (\neg p\wedge \neg q)& & \\ \neg \neg p& \mid -\mid p& & \\ \neg \mathrm{\vartheta x}p(x)& \mid -\mid {\vartheta }^{\prime }x\neg p(x)& & \\ p\wedge \mathrm{\vartheta x}q(x)& \mid -\mid \mathrm{\vartheta x}(p\wedge q(x)),& & x\notin var(p)\\ p\vee \mathrm{\vartheta x}q(x)& \mid -\mid \mathrm{\vartheta x}(p\vee q(x)),& & x\notin var(p)\\ \forall xp(x)\wedge \forall xq(x)& \mid -\mid \forall x(p(x)\wedge q(x))& & \\ \exists xp(x)\vee \exists xq(x)& \mid -\mid \exists x(p(x)\vee q(x))& & \\ {\vartheta }_{1}xp(x)\wedge {\vartheta }_{2}yq(y)& \mid -\mid {\vartheta }_{1}x{\vartheta }_{2}y(p(x)\wedge q(y)),& & x\notin var(q),y\notin var(p)\\ {\vartheta }_{1}xp(x)\vee {\vartheta }_{2}yq(y)& \mid -\mid {\vartheta }_{1}x{\vartheta }_{2}y(p(x)\vee q(y)),& & x\notin var(q),y\notin var(p)\end{array}$$

其中，定义 $\vartheta \in \{\forall ,\exists \}$ 和 ${\forall }^{\prime }:=\exists ,{\exists }^{\prime }:=\forall$。

TIP

证明含 $\exists$ 的式子时，可以证明它的逆否式，因为公理里没有 $\exists$，所以转换成逆否式里的 $\forall$ 会简化证明。

前束范式

前束范式 $p$ 是具有这个形式的谓词公式：$p={\vartheta }_1{x}_1{\vartheta }_2{x}_2\cdots q$，其中 $q$ 不含量词。斯柯伦范式在此基础上要求 $\exists$ 都在 $\forall$ 前面。

TIP

将谓词公式转化成前束范式的方法：把箭头转化成 $\neg$、$\vee$ 和 $\wedge$，然后把量词逐步移到所有东西之前。

性质

谓词演算也具有完备性等性质，略。