一阶谓词逻辑演算
一 基本概念
首先是基本单元的概念
- 个体词：用来表示研究对象。分个体常元和个体变元。前者常用 a , b , c ⋯ a,b,c\cdots a,b,c⋯ 表示，后者常用 x , y , z ⋯ x,y,z\cdots x,y,z⋯ 表示
- 个体域：个体变元的取值范围，用 D D D 表示
- 谓词：用于表示研究对象的性质，或表示研究对象之间关系的词，用大写英文字母表示。n 元谓词指含有 n 个个体变元的谓词
- 函词：用于描述个体域之间的映射，用 f , g , h , ⋯ f,g,h,\cdots f,g,h,⋯ 表示。含有 n n n 个变元的函词称为 n n n 元函词
- 量词：用于表示个体词的数量，有全程量词和存在量词
定义基本单元的组合
- 项：由个体词和函词有限次复合的表达式
- 个体常元和个体变元是项
- 如果 f f f 是一个 n n n 元函词，且 t 1 , t 2 , ⋯ , t n t_1,t_2,\cdots,t_n t1,t2,⋯,tn 都为项，则 f ( t 1 , t 2 , ⋯ , t n ) f(t_1,t_2,\cdots,t_n) f(t1,t2,⋯,tn) 也为项
- 由
1和2经过有限次复合产生结果都为项
- 合式公式：由谓词、联结词和量词组合而成的公式，合式公式也称为为此公式，或简称为公式
- 不含联结词的谓词（原子谓词）是合式公式
- 若 A A A， B B B 是合式公式，则 ¬ A \neg A ¬A、 A ∨ B A\vee B A∨B、 A ∧ B A\wedge B A∧B、 A → B A\to B A→B、 A ↔ B A\leftrightarrow B A↔B 都是合式公式
- 若 A A A 是合式公式， x x x 是变元符号，则 ( ∀ x ) A (\forall x)A (∀x)A、 ( ∃ x ) A (\exist x)A (∃x)A 都是合式公式
- 只有
1-3确定的公式才是合式公式
以下概念建立在项和合式公式的基础上
- 约束变元与自由变元：受量词约束的个体变元称为约束变元，反之称为自由变元
- 辖域：量词所约束的范围
- 易名规则：将辖域中某个约束变元全部改成未在该辖域中出现的个体变元。改名后的公式称为改名式。如： ( ∀ x ) P ( x ) (\forall x)P(x) (∀x)P(x) 和 ( ∀ x ) P ( y ) x y (\forall x)P(y)^y_x (∀x)P(y)xy 都是 ( ∀ y ) P ( y ) (\forall y)P(y) (∀y)P(y) 的改名式
- 可代入：设 v v v 为谓词公式 A A A 中的自由变元，且项 t t t 中不含 A A A 中的约束变元符，则称项 t t t 对 v v v 是可代入的
- 代入：对公式 A A A 中的自由变元 v v v 的所有自由出现均替换为项 t t t，记为 A t v A^v_t Atv，若 A A A 中无 v v v，则有 A t v = A A^v_t=A Atv=A
- 全称化： v 1 , v 2 , ⋯ , v n v_1,v_2,\cdots,v_n v1,v2,⋯,vn 为公式 A A A 中所有变元，则公式 ∀ v i 1 ∀ v i 2 ⋯ ∀ v i k A \forall v_{i_1}\forall v_{i_2}\cdots\forall v_{i_k}A ∀vi1∀vi2⋯∀vikA 称为 A A A 的全程化，公式 ∀ v 1 ∀ v 2 ⋯ ∀ v n A \forall v_1\forall v_2\cdots\forall v_n A ∀v1∀v2⋯∀vnA 称为 公式 A A A 的全称封闭式。若 A A A 无自由变元，则其自身就是全称封闭式，不含自由变元
二 一阶谓词演算形式系统
1、公理模式
由下列公式以及其所有的全称化组成
A 1 : A → ( B → A ) A 2 : ( A → ( B → C ) ) → ( ( A → B ) → ( A → C ) ) A 3 : ( ¬ A → ¬ B ) → ( B → A ) A 4 : ∀ v A → A t v ( t 对 A 中 的 变 元 v 可 代 入 ) A 5 : ∀ v ( A → B ) → ( ∀ v A → ∀ v B ) A 6 : A → ∀ v A ( v 在 A 中 无 自 由 出 现 ) \begin{aligned} &A_1:A\to(B\to A)\\ &A_2:(A\to(B\to C))\to((A\to B)\to(A\to C))\\ &A_3:(\neg A\to\neg B)\to(B\to A)\\ &A_4:\forall vA\to A_t^v\quad(t 对 A 中的变元 v 可代入)\\ &A_5:\forall v(A\to B)\to(\forall vA\to\forall vB)\\ &A_6:A\to\forall vA\quad(v 在 A 中无自由出现) \end{aligned} A1:A→(B→A)A2:(A→(B→C))→((A→B)→(A→C))A3:(¬A→¬B)→(B→A)A4:∀vA→Atv(t对A中的变元v可代入)A5:∀v(A→B)→(∀vA→∀vB)A6:A→∀vA(v在A中无自由出现)
推理规则
r m p : A , A → B B r_{mp}:\frac{A,A\to B}{B} rmp:BA,A→B
F C FC FC 中的定理、证明以及演绎、演绎结果的定义与 P C PC PC 中一致。
2、FC 的基本定理
定理 1
⊢ F C ∀ v A → A \vdash_{FC}\forall vA\to A ⊢FC∀vA→A定理 2
⊢ F C A → ¬ ∀ v ¬ A o r ⊢ F C A → ∃ v A d e f ( ∃ v ) = ¬ ∀ v ¬ \vdash_{FC}A\to\neg\forall v\neg A\\ or \vdash_{FC}A\to\exist vA\quad def(\exist v)=\neg\forall v\neg ⊢FCA→¬∀v¬Aor⊢FCA→∃vAdef(∃v)=¬∀v¬定理 3
⊢ F C ∀ v A → ∃ v A \vdash_{FC}\forall vA\to\exist vA ⊢FC∀vA→∃vA定理 4（全称推广定理）
对于 F C FC FC 中的任何公式 A A A，变元 v v v，如果 ⊢ A \vdash A ⊢A，那么 ⊢ ∀ v A \vdash \forall vA ⊢∀vA
定理 5（全称推广定理）
对于 F C FC FC 中的任何公式集合 Γ \Gamma Γ，公式 A A A，以及不在 Γ \Gamma Γ 的任意公式里自由出现的变元 v v v，如果 Γ ⊢ v \Gamma\vdash v Γ⊢v 那么 Γ ⊢ ∀ v A \Gamma\vdash\forall vA Γ⊢∀vA
定理 6（演绎定理）
设 Γ \Gamma Γ 为 F C FC FC 中的任一公式集合， A A A， B B B 为 F C FC FC 中的任意两个公式，那么 Γ ; A ⊢ B \Gamma;A\vdash B Γ;A⊢B 当且仅当 Γ ⊢ A → B \Gamma\vdash A\to B Γ⊢A→B
定理 7
设 Γ \Gamma Γ 为 F C FC FC 中的任一公式集合， A A A、 B B B 为 F C FC FC 中的任意两个公式，那么 Γ ; A ⊢ ¬ B \Gamma;A\vdash\neg B Γ;A⊢¬B 当且仅当 Γ ; B ⊢ ¬ A \Gamma;B\vdash\neg A Γ;B⊢¬A
定理 8（反证法）
如果 F C FC FC 中的公式集合 Γ ∪ { A } \Gamma\cup\{A\} Γ∪{ A} 是不一致的，那么 Γ ⊢ ¬ A \Gamma\vdash\neg A Γ⊢¬A
定理 9
设 Γ \Gamma Γ 为 F C FC FC 中的任一公式集合， A A A、 B B B 为 F C FC FC 中的任意两个公式，并且变元 v v v 不在 Γ \Gamma Γ 的任何公式里面自由出现，那么 Γ ; A ⊢ B \Gamma;A\vdash B Γ;A⊢B 蕴含 Γ ; ∀ v A ⊢ B \Gamma;\forall vA\vdash B Γ;∀vA⊢B 和 Γ ; ∀ v A ⊢ ∀ v B \Gamma;\forall vA\vdash\forall vB Γ;∀vA⊢∀vB
定理 10（存在消除）
设 Γ \Gamma Γ 为 F C FC FC 中的任一公式集合， A A A、 B B B 为 F C FC FC 中的任意两个公式，并且变元 v v v 不在 Γ \Gamma Γ 的任何公式以及公式 B B B 里自由出现，那么由 Γ ⊢ ∃ v A \Gamma\vdash\exist vA Γ⊢∃vA 以及 Γ ; A ⊢ B \Gamma;A\vdash B Γ;A⊢B 可以推出 Γ ⊢ B \Gamma\vdash B Γ⊢B
定理 11（替换原理）
设 A A A、 B B B 为 F C FC FC 的公式，且满足 A ⊢ ⊣ B A\vdash\dashv B A⊢⊣B， A A A 是 C C C 的子公式， D D D 是将 C C C 中 A A A 的若干出现换为公式 B B B 得到的公式，则 C ⊢ ⊣ D C\vdash\dashv D C⊢⊣D
定理 12（改名定理）
在 F C FC FC 中，若 A ′ A’ A′ 是 A A A 的改名式，且 A ′ A’ A′ 改用的变元不在 A A A 中出现，则 A ⊢ ⊣ A ′ A\vdash\dashv A’ A⊢⊣A′
其他定理
- ∃ x ¬ A ⊢ ⊣ ¬ ∀ x A \exist x\neg A\vdash\dashv\neg\forall xA ∃x¬A⊢⊣¬∀xA
- ∀ x ¬ A ⊢ ⊣ ¬ ∃ x A \forall x\neg A\vdash\dashv\neg\exist xA ∀x¬A⊢⊣¬∃xA
- ∀ x ( A ∧ B ) ⊢ ⊣ ∀ x A ∧ ∀ x B \forall x(A\wedge B)\vdash\dashv\forall xA\wedge\forall xB ∀x(A∧B)⊢⊣∀xA∧∀xB
- ∃ x ( A ∨ B ) ⊢ ⊣ ∃ x A ∨ ∃ x B \exist x(A\vee B)\vdash\dashv\exist xA\vee\exist xB ∃x(A∨B)⊢⊣∃xA∨∃xB
- ∃ x ( A ∧ B ) ⊢ ∃ x A ∧ ∃ x B \exist x(A\wedge B)\vdash\exist xA\wedge\exist xB ∃x(A∧B)⊢∃xA∧∃xB
- ∀ x A ∨ ∀ x B ⊢ ∀ x ( A ∨ B ) \forall xA\vee\forall xB\vdash\forall x(A\vee B) ∀xA∨∀xB⊢∀x(A∨B)
- ∃ x ∀ y B ( x , y ) ⊢ ∀ y ∃ x B ( x , y ) \exist x\forall yB(x,y)\vdash\forall y\exist xB(x,y) ∃x∀yB(x,y)⊢∀y∃xB(x,y)
三 F C FC FC 系统的语义
语义（结构）： F C FC FC 的一个语义是一个结构，该结构包括：
- 非空集合 U U U，称为论域或个体域
- 一个称为解释的映射 I I I， I : L a ∪ L f ∪ L p → U ∪ U f ∪ U p I:L_a\cup L_f\cup L_p\to U\cup U_f\cup U_p I:La∪Lf∪Lp→U∪Uf∪Up，其中 U f U_f Uf 为 U U U 上所有函数符号构成的集合。 U p U_p Up 是 U U U 上的所有关系构成的集合。
- 对于任一常元 a a a， I ( a ) ∈ U I(a)\in U I(a)∈U，记为 a ˉ \bar{a} aˉ
- 对于每一个 n n n 元函词 f ( n ) f^{(n)} f(n)， I ( f ( n ) ) I(f^{(n)}) I(f(n)) 记为 f ˉ ( n ) \bar{f}^{(n)} fˉ(n)
- 对于每一个 n n n 元谓词 P ( n ) P^{(n)} P(n)， I ( P ( n ) ) I(P^{(n)}) I(P(n)) 记为 P ˉ ( n ) \bar{P}^{(n)} Pˉ(n)
指派：确定了系统的语义的前提下，一个指派是指一个映射 s : L v → U s:L_v\to U s:Lv→U，该映射可以扩展到项的集合 L t L_t Lt 到 U U U 的映射
语义的记号：记“公式 A A A 在结构 U \mathcal{U} U 和指派 S S S 下取值真” 为 ⊨ U A [ S ] \models_\mathcal{U}A[S] ⊨UA[S]，反之记为 ̸ ⊨ U A [ S ] \not\models_{\mathcal{U}}A[S] ⊨UA[S]。 ⊨ U A \models_{\mathcal{U}}A ⊨UA 表示在结构中，对于一切指派 A A A 均为真。 ⊨ T A \models_{T}A ⊨TA 或 ⊨ A \models A ⊨A 表示公式 A A A 在任意的结构中都为真，此时称 A A A 永真。
⊨ U A [ S ] \models_\mathcal{U}A[S] ⊨UA[S] 的递归定义
若 A A A 为原子公式 P ( n ) t 1 ⋯ t n P^{(n)}t_1\cdots t_n P(n)t1⋯tn 时
⊨ U A [ S ] \models_\mathcal{U}A[S] ⊨UA[S] 当且仅当 < s ˉ ( t 1 ) , ⋯ , s ˉ ( t n ) > ∈ P ˉ ( n ) <\bar{s}(t_1),\cdots,\bar{s}(t_n)>\in\bar{P}^{(n)} <sˉ(t1),⋯,sˉ(tn)>∈Pˉ(n)
A A A 为公式 ¬ B \neg B ¬B 时
⊨ U A [ S ] i f f ̸ ⊨ U B [ S ] \models_\mathcal{U}A[S]\quad iff\quad \not\models_\mathcal{U}B[S] ⊨UA[S]iff⊨UB[S]
A A A 为公式 B → C B\to C B→C 时
⊨ U A [ S ] i f f ̸ ⊨ U B [ S ] o r ⊨ U C [ S ] \models_\mathcal{U}A[S]\quad iff\quad\not\models_\mathcal{U}B[S]\,or\,\models_\mathcal{U}C[S] ⊨UA[S]iff⊨UB[S]or⊨UC[S]
A A A 为公式 ∀ v B \forall vB ∀vB 时
⊨ U A [ S ] \models_\mathcal{U}A[S] ⊨UA[S] 当且仅当对每一个 d ∈ U d\in U d∈U 都有 ⊨ U A [ S ( v ∣ d ) ] \models_\mathcal{U}A[S(v|d)] ⊨UA[S(v∣d)]
s ( v ∣ d ) ( u ) = { s ( u ) u ≠ v d u = v s(v|d)(u)= \begin{cases} s(u)\quad &u\neq v\\ d\quad &u=v \end{cases} s(v∣d)(u)={ s(u)du=vu=v
