【数理逻辑】谓词逻辑 ( 前束范式 | 前束范式转换方法 | 谓词逻辑基本等值式 | 换名规则 | 谓词逻辑推理定律 )

一、 前束范式

公式 A A A 有如下形式 :

Q 1 x 1 Q 2 x 2 ⋯ Q k x k B Q_1 x_1 Q_2 x_2 \cdots Q_kx_k B Q1​x1​Q2​x2​⋯Qk​xk​B

则称 A A A 是 前束范式 ; 前束范式 A A A 的相关元素 说明 :

量词 : Q i Q_i Qi​ 是量词 , 全称量词 ∀ \forall ∀ , 或 存在量词 ∃ \exist ∃ ;

指导变元 : x i x_i xi​ 是 指导变元 ;

B B B 公式 : B B B 是谓词逻辑公式 , 其中不含有量词 , B B B 中 可以含有 前面的 x 1 , x 2 , ⋯   , x k x_1 , x_2 , \cdots , x_k x1​,x2​,⋯,xk​ 指导变元 , 也 可以不含有 其中的某些变元 ;

( B B B 中一定不能含有量词 )

二、 前束范式转换方法

求一个谓词逻辑公式的前束范式 , 使用 基本等值式 , 或 换名规则 ;

基本等值式 : 参考博客 【数理逻辑】谓词逻辑 ( 谓词逻辑基本等值式 | 消除量词等值式 | 量词否定等值式 | 量词辖域收缩扩张等值式 | 量词分配等值式 )

换名规则 : 公式 A A A 中 , 某个量词辖域中 , 某个约束 出现的 个体变元 对应的 指导变元 x i x_i xi​ , 使用公式 A A A 中没有出现过的 变元 x j x_j xj​ 进行替换 , 所得到的公式 A ′ ⇔ A A' \Leftrightarrow A A′⇔A ;

如 : ∀ x F ( x ) ∨ ∀ x ¬ G ( x , y ) \forall x F(x) \lor \forall x \lnot G(x, y) ∀xF(x)∨∀x¬G(x,y) 如果要求其前束范式 , 前后有两个 x x x , 这里使用换名规则 , 将某个换成没有出现过的 指导变元 z z z , 换名后为 ∀ x F ( x ) ∨ ∀ z ¬ G ( z , y ) \forall x F(x) \lor \forall z \lnot G(z, y) ∀xF(x)∨∀z¬G(z,y) ;

三、 前束范式示例

求 ∀ x F ( x ) ∨ ¬ ∃ x G ( x , y ) \forall x F(x) \lor \lnot \exist x G(x, y) ∀xF(x)∨¬∃xG(x,y) 的前束范式 ;

上述公式不是前束范式 , 其 量词 ∀ x \forall x ∀x 的辖域是 F ( x ) F(x) F(x) , 量词 ∃ x \exist x ∃x 的辖域是 G ( x , y ) G(x, y) G(x,y) , 两个辖域都没有覆盖完整的公式 ;

使用 等值演算 和 换名规则 , 求前束范式 ;

∀ x F ( x ) ∨ ¬ ∃ x G ( x , y ) \forall x F(x) \lor \lnot \exist x G(x, y) ∀xF(x)∨¬∃xG(x,y)

使用 量词否定等值式 , 先把 否定联结词 移动到量词后面 , 使用的等值式为 ¬ ∃ x A ( x ) ⇔ ∀ x ¬ A ( x ) \lnot \exist x A(x) \Leftrightarrow \forall x \lnot A(x) ¬∃xA(x)⇔∀x¬A(x) ;

⇔ ∀ x F ( x ) ∨ ∀ x ¬ G ( x , y ) \Leftrightarrow \forall x F(x) \lor \forall x \lnot G(x, y) ⇔∀xF(x)∨∀x¬G(x,y)

使用 换名规则 , 将第二个 ∀ x ¬ G ( x , y ) \forall x \lnot G(x, y) ∀x¬G(x,y) 中的 x x x 换成 z z z ;

⇔ ∀ x F ( x ) ∨ ∀ z ¬ G ( z , y ) \Leftrightarrow \forall x F(x) \lor \forall z \lnot G(z, y) ⇔∀xF(x)∨∀z¬G(z,y)

使用 辖域扩张等值式 , 将 ∀ x \forall x ∀x 辖域扩张 , 使用的等值式为 ∀ x ( A ( x ) ∨ B ) ⇔ ∀ x A ( x ) ∨ B \forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B ∀x(A(x)∨B)⇔∀xA(x)∨B

⇔ ∀ x ( F ( x ) ∨ ∀ z ¬ G ( z , y ) ) \Leftrightarrow \forall x ( F(x) \lor \forall z \lnot G(z, y) ) ⇔∀x(F(x)∨∀z¬G(z,y))

再次使用 辖域扩张等值式 , 将 ∀ z \forall z ∀z 辖域扩张 , 使用的等值式为 ∀ x ( A ( x ) ∨ B ) ⇔ ∀ x A ( x ) ∨ B \forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B ∀x(A(x)∨B)⇔∀xA(x)∨B

⇔ ∀ x ∀ z ( F ( x ) ∨ ¬ G ( z , y ) ) \Leftrightarrow \forall x \forall z ( F(x) \lor \lnot G(z, y) ) ⇔∀x∀z(F(x)∨¬G(z,y))

此时已经是前束范式了 ;

使用 命题逻辑 等值式 中的 蕴涵等值式

⇔ ∀ x ∀ z ( G ( z , y ) → F ( x ) ) \Leftrightarrow \forall x \forall z ( G(z, y) \to F(x) ) ⇔∀x∀z(G(z,y)→F(x))

四、 谓词逻辑推理定律

下面推理定律是单向的 , 从左边可以推理出右边 , 从右边不能推理出左边 ; ( 不是等值式 )

① ∀ x A ( x ) ∨ ∀ x B ( x ) ⇒ ∀ x ( A ( x ) ∨ B ( x ) ) \rm \forall x A(x) \lor \forall x B(x) \Rightarrow \forall x ( A(x) \lor B(x) ) ∀xA(x)∨∀xB(x)⇒∀x(A(x)∨B(x))

对应 全称量词 分配率 , 等值式中 只适用于 合取联结词 , 就是因为上述 析取时 , 从右往左 是错误的 , 只能从左往右推理 ;

② ∃ x ( A ( x ) ∧ B ( x ) ) ⇒ ∃ x A ( x ) ∧ ∃ x B ( x ) \rm \exist x ( A(x) \land B(x) ) \Rightarrow \exist x A(x) \land \exist x B(x) ∃x(A(x)∧B(x))⇒∃xA(x)∧∃xB(x)

③ ∀ x ( A ( x ) → B ( x ) ) ⇒ ∀ x A ( x ) → ∀ x B ( x ) \rm \forall x ( A(x) \to B(x) ) \Rightarrow \forall x A(x) \to \forall x B(x) ∀x(A(x)→B(x))⇒∀xA(x)→∀xB(x)

④ ∀ x ( A ( x ) → B ( x ) ) ⇒ ∃ x A ( x ) → ∃ x B ( x ) \rm \forall x ( A(x) \to B(x) ) \Rightarrow \exist x A(x) \to \exist x B(x) ∀x(A(x)→B(x))⇒∃xA(x)→∃xB(x)