一阶逻辑 | 夜雨阁

谓词

原子命题(陈述)分解为：主语(subject)和谓语(predicate)
- 个体词：命题中独立存在的个体，常为主语
- 谓词：刻画个体的性质或它们之间的关系，谓语
例子
- 命题“小张是大学生”
  - “小张”是个体词，“…是大学生”是谓词
- 命题“2小于3”
  - 2和3是个体词，“…小于…”是谓词
个体常量：具体、特定的个体词，常用小写字母a,b等等表示
个体变量：抽象或泛指某个体的个体词，常用小写字母x,y等等表示
个体域(domain of discourse)：所有个体的集合，也即个体变量的取值集合
n元谓词(n-ary predicate)：关于n个个体词的谓词，常用大写字母表示，记为 $P(x_1,x_2,...,x_n)$
一元谓词表示个体的性质，多元谓词表示个体之间的关系.
符号化
- 命题“小张是大学生”
  - 个体常量a：小张
  - 谓词P(x)：x是大学生
  - P(a)：小张是大学生
- 命题“2<3”
  - 个体常量a：2，个体常量b：3
  - 谓词L(y,z)：y < z
  - L(a,b)： 2 < 3

项的递归定义：
- (1)个体词(个体常量和个体变量，在个体域D上)是项
- (2)若 $f(x_1,x_2,…,x_n), n≥1$ 是 $D^n→D$ 上的n元函数， $t_1,t_2,…,t_n$ 是项，则 $f(t_1,t_2,…,t_n)$ 是项
- (3)所有的项都是通过有限次使用(1)和(2)之后得到的符号串
谓词公式的递归定义:
- (1)若 $P$ 是 $n(n≥1)$ 元谓词符号， $t_1,t_2,…,t_n$ 是项，则 $P(t_1,t_2,…,t_n)$ 是谓词公式；
- (2)若A和B是谓词公式，则 $(¬A)、(A∨B)、(A∧B)、(A→B)、(A↔B)$ 也是谓词公式；
- (3)若A是谓词公式， $x$ 是个体变量，则 $∀xA、∃xA$ 也是谓词公式；
- (4)所有的谓词公式都是通过有限次使用(1)、(2)和(3)之后得到的符号串。
在谓词公式 $∀xA$ 和 $∃x$ A中， $x$ 称指导变量，量词的辖域为 $A$ 。辖域中的变量 $x$ 称约束(bound)变量。 $A$ 中的非约束变量称为自由(free)变量。
谓词公式类型：
- 有效公式(validity)：关于一切解释的真值均为真
- 矛盾公式：关于一切解释的真值均为假
- 可满足公式：至少存在一种使其为真的解释
命题公式的代换实例：
- 命题公式 $A(p_1,p_2,…,p_n)$ ，谓词公式 $A_1,A_2,…,A_n$ 。分别用 $A_1,A_2,…,A_n$ 替换A中的 $p_1,p_2,…,p_n$ ，所得到的谓词公式称为 $A$ 的代换实例
- 永真公式的代换实例是有效公式
- 永假公式的代换实例是矛盾公式

谓词公式的解释 $I$ 由下面四部分组成：
- 非空个体域集合 $D$
- 分别指定公式中的自由变量和常量符号为 $D$ 中的元素
- 指定公式中的n元函数符号为 $D^n$ 到 $D$ 的函数
- 指定公式中的n元谓词符号为 $D^n$ 到 $\{0,1\}$ 的函数
谓词公式 $∀xP(x)$ 在解释 $I$ 下为真 $\Leftrightarrow$ 对于任意 $x\in D$ ， $P^I(x)=1$
谓词公式 $∃xP(x)$ 在解释 $I$ 下为真 $\Leftrightarrow$ 存在 $x\in D$ ，使 $P^I(x)=1$
若D有限， $D={a_1,a_2,…,a_n}$ ，则在解释 $I$ 下
- $∀xP(x)$ 为真 $\Leftrightarrow$ $P^I(a_1)∧P^I(a_2)∧...∧P^I(a_n)=1$
- $∃xP(x)$ 为真 $\Leftrightarrow$ $P^I(a_1)∨P^I(a_2)∨…∨P^I(a_n)=1$

$A$ 和 $B$ 是任意的谓词公式， $A(x,y)$ 含自由变量 $x$ 和 $y$ ， $A(x)$ 和 $B(x)$ 含自由变量 $x$ ， $B$ 不含自由变量 $x$
$\neg \forall xA(x) = \exists x \neg A(x)$ ， $\neg \exists x A(x) = \forall x\neg A(x)$
$\forall x\forall y A(x,y) = \forall y\forall x A(x,y)$ ， $\exists x\exists yA(x,y) =\exists y\exists xA(x,y)$
$\forall xB =B$ ， $\exists xB=B$
$A$ 中不含个体变量 $y$ ， $\forall xA(x)=\forall yA(y)$ ， $\exists xA(x) = \exists yA(y)$
$\forall x(A(x)\wedge B(x)) = \forall xA(x) \wedge \forall xB(x)$
$\exists x(A(x)\vee B(x)) = \exists xA(x)\vee \exists xB(x)$
$\forall x(A(x)\vee B) = \forall xA(x)\vee B$ ， $\forall x(A(x)\wedge B) = \forall xA(x)\wedge B$
$\exists x(A(x)\vee B) = \exists xA(x)\vee B$ ， $\exists x(A(x)\wedge B) = \exists xA(x)\wedge B$
$\forall x(A(x)\rightarrow B) = \exists xA(x)\rightarrow B$ ， $\forall x(B\rightarrow A(x))=B\rightarrow \forall xA(x)$
$\exists x(A(x)\rightarrow B) = \forall xA(x)\rightarrow B$ ， $\exists x(B\rightarrow A(x))=B\rightarrow \exists xA(x)$

前束范式：谓词公式，形如 $□x_1□x_2…□x_nB$ , $□$ 是量词 $∀$ 或 $∃$ ， $x_1,x_2,…,x_n$ 是个体变量 $B$ 是不含量词的谓词公式
前缀： $□x_1□x_2…□x_n$
主式： $B$
任何谓词公式都存在与之等值的前束范式

全称量词消去规则(Universal Specification, US)
- $∀$ 个体常量 $e$ ， $∀xA(x)$ 推出 $A(e)$
- $∀$ 个体变量 $y$ ， $∀xA(x)$ 推出 $A(y)$
- 在 $A$ 中， $x$ 不在任何 $∀y$ 和 $∃y$ 的辖域内自由出现
全称量词引入规则(Universal Generalization, UG)
- $A(x)$ 对定义域中的任意 $x$ 成立，推出 $∀xA(x)$
- $A$ 不含额外个体常量，前提中没有任何自由的个体变量 $x$
存在量词消去规则(Existential Specification, ES)
- $∃xA(x)推出A(e)$
- $e$ 是在证明中未出现过的新的额外个体常量
存在量词引入规则(Existential Generalization, EG)
- $∀$ 个体常量 $e$ ， $A(e)$ 推出 $∃xA(x)$ ，在 $A$ 中， $e$ 不在任何 $∀x$ 和 $∃x$ 的辖域内出现
- $∀$ 个体变量 $y$ ， $A(y)$ 推出 $∃xA(x)$ ，在 $A$ 中， $y$ 不在任何 $∀x$ 和 $∃x$ 的辖域内自由出现