三段论

A:大前提，B：小前提，C：结论，
$$A,B\Rightarrow C$$
的推理是有效的但是却无法使用命题逻辑论证

谓词公式

命题与命题函数，命题与命题函数的表达

$$金子闪光，但闪光的不一定都是金子$$

$$\begin{gathered} 令G(x):x是金子，F(x):x闪光 \\ 命题表达为\forall x(G(x)\to F(x))\wedge \exists x(\neg G(x)\wedge F(x))或\forall x(G(x)\to F(x))\wedge \neg \forall x(F(x)\to G(x)) \end{gathered}$$

谓词公式的赋值

谓词公式的永真式：给谓词公式付任何值，公式的值都为真，如I(x)V¬I(x)

谓词公式的等价

$$对于谓词公式A,B，如果A⟷B是永真式，记作A⟺B$$

谓词公式的永真蕴含式

$$对于谓词公式A,B，如果A\to B是永真式，记作A\Rightarrow B$$

$$只要不牵涉到量词的运算，命题逻辑中的等价公式与重言蕴含公式均可推广到谓词逻辑中$$

谓词公式中量词的消去与转换

有限论域消去量词

如 论 域 D = { 1 , 2 , 3 } ∀ x A ( x ) ⇔ A ( 1 ) ∧ A ( 2 ) ∧ A ( 3 ) ∃ x A ( x ) ⇔ A ( 1 ) ∨ A ( 2 ) ∨ A ( 3 ) 如论域D=\{ 1,2,3\} \\ \forall xA(x) \Leftrightarrow A(1) \wedge A(2) \wedge A(3) \\ \exist x A(x) \Leftrightarrow A(1) \vee A(2) \vee A(3) \\ 如论域D={1,2,3}∀xA(x)⇔A(1)∧A(2)∧A(3)∃xA(x)⇔A(1)∨A(2)∨A(3)

量词转换

$$“并非所有的x具有性质A”与“存在x没有性质A”是同一个意思:\neg \forall xA(x)\iff \exists x\neg A(x)$$

量词辖域的扩充与收缩

$$\begin{gathered} 不受量词约束的部分可以添加或消除到量词的辖域 \\ 1.\forall xA(x)\vee B<-->\forall x(A(x)\vee B) \\ 2.\forall xA(x)\wedge B<-->\forall x(A(x)\wedge B) \\ 3.\exists xA(x)\vee B<-->\exists x(A(x)\vee B) \\ 4.\exists xA(x)\wedge B<-->\exists x(A(x)\wedge B) \end{gathered}$$

量词分配公式

$$\begin{gathered} \forall x(A(x)\wedge B(x))\iff \forall xA(x)\wedge \forall xB(x) \\ \exists x(A(x)\vee B(x))\iff \exists xA(x)\vee \exists xB(x) \\ \exists x(A(x)\wedge B(x))\Rightarrow \exists xA(x)\wedge \exists xB(x) \\ \forall xA(x)\vee \forall xB(x)\Rightarrow \forall x(A(x)\vee B(x)) \\ 注意后两个公式的变化:比如最后一个：有张三、李四2人,张三会唱歌但不会跳舞,李四不会唱歌但会跳舞。 \\ “所有人或者会唱歌或者会跳舞”是对的，“所有人会唱歌或者所有人会跳舞”是错的。所以：全称量词对析取没有分配律。 \end{gathered}$$

范式

前束范式

所有量词前都没有连接词，所有量词都在公式左面，所有量词的辖域都延伸到公式的末尾

$$例如\forall y\exists x(A(x)\to B(x,y))$$

$$\begin{gathered} 求\forall xA(x)\to \exists xB(x)的前束范式 \\ \neg \forall xA(x)\vee \exists xB(x) \\ \exists x\neg A(x)\vee \exists xB(x) \\ \exists x\neg A(x)\vee \exists yB(y)(换名原则) \\ \exists x(\neg A(x)\vee \exists yB(y))(量词的辖域扩充) \\ \exists x\exists y(\neg A(x)\vee B(y))(量词的辖域扩充) \end{gathered}$$

求前束范式的步骤：
1.$$消除公式中的连接词：\to 与\leftrightarrow (双条件：p\leftrightarrow q等于（p\to q）\wedge （q\to p）)$$
2.
$$如果量词前有\neg ,利用前边的量词转换律后移$$
3.
$$利用约束变元的改名规则，为量词的扩充做准备$$
4.
$$量词扩充后提取量词，将式子化为前束范式$$

谓词验算的推理

推理

推理的方法

$$\begin{array}{c}推理方法\\ P_1\wedge P_2\wedge P_3\Rightarrow Q\end{array}\{\begin{array}{l}直接推理\\ 间接推理\{\begin{array}{l}条件论证(P_1\wedge P_2\Rightarrow P_3\to Q)\\ 反证法(P_1\wedge P_2\wedge P_3\wedge \neg Q\iff F)\end{array}\end{array}$$

推理的规则

$$推理的规则\{\begin{array}{l}P规则(证明过程中引入初始条件)\\ T规则(证明过程中引入中间结论)\\ CP(ConditionalProof)规则(使用条件论证)\\ 脱掉或添加量词的规则\{\begin{array}{c}US\\ ES\\ EG\\ UG\end{array}\end{array}$$
US规则：全称特指规则Universal Specialization
去掉全称量词
$$\forall xA(x)\Rightarrow A(c)(c是个体域中任意指定个体)$$

ES规则：特称特指规则Existential Specialization
去掉全存在量词
$$\exists xA(x)\Rightarrow A(c)(c是使得A(c)为真的)$$

EG规则：存在推广规则Existential Generalization
添加存在量词
$$A(c)\Rightarrow \exists xA(x)(c个体域内的某个个体)$$

UG规则：全称推广规则Universal Generalization
添加全称量词
$$A(c)\Rightarrow \forall xA(x)(c个体域内的任意某个个体)$$

谓词逻辑的推理