Chapter 2: First-Order Logic and Model Theory (2.3~2.4)

2.3 First-Order Theories

一阶理论：一个一阶理论 \(\mathcal{K}\) 使用一个一阶语言的符号及其公式，以及如下这些公理（公理分两种： 逻辑公理和非逻辑公理）以及演绎规则

2.3.1 Logical Axioms

逻辑公理

如果 \(B\)，\(C\)，\(D\) 都是合式公式，则如下是 \(\mathcal{K}\) 的逻辑公理

• A1: \(B \Rightarrow (C \Rightarrow B)\)
• A2: \((B \Rightarrow (C \Rightarrow D)) \Rightarrow ((B \Rightarrow C) \Rightarrow (B \Rightarrow D))\)
• A3: \((\neg C \Rightarrow \neg B) \Rightarrow ((\neg C \Rightarrow B) \Rightarrow C)\)
• A4: 如果 \(B(x_i)\) 是一个合式公式，且项 \(t\) 可以自由替换 \(x_i\) 则 \((\forall x_i)B(x_i) \Rightarrow B(t)\) （特别地，\(t\) 可以是 \(x_i\)，于是总有 \((\forall x_i)B \Rightarrow B\)）
• A5: 如果 \(B\) 不包含 \(x_i\) 的自由变量，则 \((\forall x_i)(B \Rightarrow C) \Rightarrow (B \Rightarrow (\forall x_i)C)\)

2.3.2 Proper Axioms

每一个理论都有可能有其他的非逻辑公理，也可能完全没有，如果没有的话则称为一阶谓词演算（first-order predicate calculus）

2.3.3 Rules of Inference

演绎规则有两个

1. Modus ponens（缩写为 MP)：\(B\) 和 \(B \Rightarrow C\) 推出 \(C\)
2. Generalization（缩写为 Gen)：\(B\) 推出 \((\forall x_i)B\)

注意到根据 2.2 的 Property 3 和 Property 6， 在一个解释下，如果对为真的式子运用 MP 和 Gen 仍然会得出为真的式子

一些一阶理论的例子

1. Partial order：该理论使用的语言只有一个谓词符号 \(A_1^2(x_i, x_j)\) 写作 \(x_i < x_j\)，并且有两个非逻辑公理
   1. \((\forall x_1)(\neg x_1 < x_1)\) （irreflexivity）
   2. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1 < x_2 \wedge x_2 < x_3 \Rightarrow x_1 < x_3)\) （transitivity）
2. Group theory：该理论使用语言有一个谓词符号 \(A_1^2(t, s)\) 写作 \(t = s\)，一个函数符号 \(f_1^2(t, s)\) 写作 \(t + s\)， 一个常量符号 \(a_1\) 写作 0，并且有以下非逻辑公理
   1. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1 + (x_2 + x_3) = (x_1 + x_2) + x_3)\) （associativity）
   2. \((\forall x_1)(0 + x_1 = x_1)\) （identiy）
   3. \((\forall x_1)(\exists x_2)(x_2 + x_1 = 0)\) （inverse）
   4. \((\forall x_1)(x_1 = x_1)\) （reflexivity of =）
   5. \((\forall x_1)(\forall x_2)(x_1 = x_2 \Rightarrow x_2 = x_1)\) （symmetry of =）
   6. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1 = x_2 \wedge x_2 = x_3 \Rightarrow x_1 = x_3)\) （transitivity of =）
   7. \((\forall x_1)(\forall x_2)(\forall x_3)(x_2 = x_3 \Rightarrow x_1 + x_2 = x_1 + x_3 \wedge x_2 + x_1 = x_3 + x_1)\) （substitutivity of =）

2.4 Properties of First-Order Theories

Proposition 2.1

\(\mathcal{K}\) 中的重言式 \(B\) 也是 \(\mathcal{K}\) 的定理，且其证明只需要公理 A1~A3 和 MP

Proposition 2.2

一阶谓词演算（没有非逻辑公理）的定理在所有解释下都是真的（逻辑有效 logically valid）

Corollary 2.3

一阶谓词演算是一致的（\(B\) 和 \(\neg B\) 不能同时有证明）

演绎定理的一些前置说明

命题演算里的演绎定理没办法原封不动地移植到一阶理论中，例如 \(B \vdash_{\mathcal{K}} (\forall x_i)B\) 总是成立（Gen）， 但 \(\vdash_{\mathcal{K}} B \Rightarrow (\forall x_i)B\) 却不一定成立（相当意外的）：例如 \(x_1 = 0 \Rightarrow (\forall x_1)x_1 = 0\) ¹，当 \(x_1 = 0\) 时不成立，故其不是逻辑有效，由 Proposition 2.2 知不可能是定理

一个有修改但依然有用的演绎定理是可以推导出来的，不过首先要一些额外的定义

Depend upon

令 \(\Gamma\) 是一个合式公式集，合式公式 \(B \in \Gamma\)，又 \(D_1, D_2, ..., D_n\) 是从 \(\Gamma\) 推导出的一个证明； 称 \(D_i\) 依赖于（depend upon）\(B\) 当且仅当：

1. \(D_i\) 就是 \(B\)，或者
2. \(D_i\) 是一些前面的公式用 MP 或 Gen 产生的直接结果，而这些前面的公式中至少有一个是依赖于 \(B\) 的

Proposition 2.4

假如 \(C\) 在 \(\Gamma, B \vdash C\) 的一个证明中不依赖于 \(B\)，则有 \(\Gamma \vdash C\)

Proposition 2.5 (Deduction Theorem)

（拗口的）演绎定理

假设在 \(\Gamma, B \vdash C\) 的证明序列（步骤） \(D_1, D_2, ..., D_n\) 里，不存在 Gen 某个公式的步骤且该公式依赖于 \(B\) 且添加的量词变量是 \(B\) 的自由变量，则 \(\Gamma \vdash B \Rightarrow C\)

不过这个演绎定理里的条件太过拗口冗长，下面这些弱一些的推论可能在实际中更有用

Corollary 2.6

如果 \(\Gamma, B \vdash C\) 的证明序列中没有涉及到添加 \(B\) 的自由变量为量词的 Gen 的话，则 \(\Gamma \vdash B \Rightarrow C\)

Corollary 2.7

如果 \(B\) 是封闭公式的话（没有自由变量）且 \(\Gamma, B \vdash C\)，则 \(\Gamma \vdash B \Rightarrow C\)

Extension of Propositions 2.4–2.7

（这一段有点不太好理解，直接按我自己的理解方式来说明）

演绎定理实际上是将旧证明 \(\Gamma, B \vdash C_j\) 转换为新证明 \(\Gamma \vdash B \Rightarrow C_j\) 的一个算法 （当然首先旧证明序列必须满足上述那些条件）；如下是一种具体方法

按顺序读取旧证明的每一步 \(C_j\)，在上图左边确定 \(C_j\) 所属，然后输出对应右边的一组公式序列， 这些一组组的公式序列连接起来即组成新的证明

观察上图可知：

1. 右边每一组序列的最后一个公式必定是 \(B \Rightarrow C_j\)，这正是演绎定理归纳法要证明的

2. 所有不依赖于 \(B\) 的 \(C_j\) 会同时出现在新旧证明中：见 * 或 ** 处， 其中 ** 处的意思是，该 \(C_j\) 在本组公式序列里实际上是没有用到的， 特意补全上去就是为了保证所有不依赖于 \(B\) 的 \(C_j\) 也都出现在新证明中， 也许后续证明（例如某个 Gen）会用到

3. 所有不依赖于 \(B\) 的 \(C_j\) 不单止会同时出现在新旧证明，而且它们的 \(\Gamma\) 依赖集也是一样的 （因为证明过程是完全相同的）

4. 旧证明 \(C_j\) 与对应新证明 \(B \Rightarrow C_j\) 也有相同的 \(\Gamma\) 依赖集

   Proof

   以 \(j\) 进行归纳

   • 若 \(C_j\) 是公理，不依赖于 \(\Gamma\) 中任何前提，对应右侧 \(B \Rightarrow C_j\) 仅由公理 MP 得出，也不依赖于 \(\Gamma\) 中任何前提
   • 若 \(C_j \in \Gamma\)，则依赖于自身，右侧由 \(C_j\) 和公理 MP 得出，故也依赖于 \(C_j\)
   • 若 \(C_j\) 是 \(B\)，不依赖于 \(\Gamma\) 中任何前提，右侧是 Lemma 1.8， 无任何依赖，自然也不依赖于 \(\Gamma\) 中任何前提
   • 若 \(C_j\) 为 \(C_l \Rightarrow C_j\) 和 \(C_l\) MP 所得，则其 \(\Gamma\) 依赖集为这两前件依赖集的并集， 由归纳假设，该并集等于 \(B \Rightarrow (C_l \Rightarrow C_j)\)¹ 和 \(B \Rightarrow C_l\)² 依赖集的并集， 右侧恰好涉及到公式 ¹² （两个 MP），因此两侧 \(\Gamma\) 依赖集相同
   • 若 \(C_j\) 为 \((\forall x_i)C_l\)，则其依赖集等于 \(C_l\) 的依赖集； 右侧有两种可能的输出，第一种用到 Gen \(C_l\)，由 3 知新旧证明中的 \(C_l\) 是有相同依赖集的； 第二种用到 Gen \(B \Rightarrow C_l\)，由归纳假设知左侧 \(C_l\) 和右侧 \(B \Rightarrow C_l\) 也是有相同依赖集的

5. 当且仅当旧证明有 Gen 时（\((\forall x_i)C_l\)），新证明有 Gen（\((\forall x_i)C_l\) 或者 \((\forall x_i)(B \Rightarrow C_l)\)），由 3 和 4 知两边的 \(\Gamma\) 依赖集一样，且两边添加的量词变量也一样（\(x_i\)）， 因此可以得出下面的结论

如果 \(\Gamma, A, B \vdash C\) 的证明满足

• a 没有一个 Gen 的步骤是依赖于 \(A\) 的且其添加的量词变量是 \(A\) 的自由变量
• b 没有一个 Gen 的步骤是依赖于 \(B\) 的且其添加的量词变量是 \(B\) 的自由变量

则可以直接 \(\Gamma \vdash A \Rightarrow (B \Rightarrow C)\)

这个结论可以推而广之，只要原始证明对多个前提都满足条件的话，则可以一步多次演绎定理

Exercises

2.27 证明以下定理

• a \(\vdash (\forall x)(B \Rightarrow C) \Rightarrow ((\forall x)B \Rightarrow (\forall x)C)\)

  Proof

  1. \((\forall x)(B \Rightarrow C)\) Hyp
  2. \((\forall x)(B \Rightarrow C) \Rightarrow (B \Rightarrow C)\) A4
  3. \(B \Rightarrow C\) MP 上述两个
  4. \((\forall x)B\) Hyp
  5. \((\forall x)B \Rightarrow B\) A4
  6. \(B\) MP 上述两个
  7. \(C\) MP 3 和 6
  8. \((\forall x)C\) Gen

  上述证明了 \((\forall x)(B \Rightarrow C), (\forall x)B \vdash (\forall x)C\) 注意上述证明只有最后一步是 Gen， 且量词 \(x\) 不是两个前提的自由变量，故可以使用 DT（Deduction Theorem）得出证明

• b \(\vdash (\forall x)(B \Rightarrow C) \Rightarrow ((\exists x)B \Rightarrow (\exists x)C)\)

  Proof

  1. \((\forall x)(B \Rightarrow C)\) Hyp
  2. \((\forall x)(B \Rightarrow C) \Rightarrow (B \Rightarrow C)\) A4
  3. \(B \Rightarrow C\) MP 上述两个
  4. \((B \Rightarrow C) \Rightarrow (\neg C \Rightarrow \neg B)\) Lemma 1.11#e
  5. \(\neg C \Rightarrow \neg B\) MP 上述两个
  6. \((\forall x)(\neg C \Rightarrow \neg B)\) Gen
  7. \((\forall x)(\neg C \Rightarrow \neg B) \Rightarrow ((\forall x)(\neg C) \Rightarrow (\forall x)(\neg B))\) 2.27#a
  8. \((\forall x)(\neg C) \Rightarrow (\forall x)(\neg B)\) MP 上述两个
  9. \(((\forall x)(\neg C) \Rightarrow (\forall x)(\neg B)) \Rightarrow (\neg (\forall x)(\neg B) \Rightarrow \neg (\forall x)(\neg C))\) Lemma 1.11#e
  10. \(\neg (\forall x)(\neg B) \Rightarrow \neg (\forall x)(\neg C)\) MP 上述两个

  上述证明了 \((\forall x)(B \Rightarrow C) \vdash (\exists x)B \Rightarrow (\exists x)C\)，唯一一步 Gen 其量词变量 \(x\) 不是前提的自由变量，故可以用 DT

• c \(\vdash (\forall x)(B \wedge C) \Leftrightarrow (\forall x)B \wedge (\forall x)C\)

  Proof

  TODO

• d \(\vdash (\forall y_1)...(\forall y_n)B \Rightarrow B\)

  Proof

  1. \((\forall y_1)...(\forall y_n)B\) Hyp
  2. \((\forall y_1)...(\forall y_n)B \Rightarrow (\forall y_2)...(\forall y_n)B\) A4
  3. \((\forall y_2)...(\forall y_n)B\) MP 上述两个
  4. 反复进行上面的操作直到剩下 \(B\)

• e \(\vdash \neg (\forall x)B \Rightarrow (\exists x) \neg B\)

  Proof

  1. \(\neg \neg B \Rightarrow B\) Lemma 1.11#a
  2. \((\forall x)(\neg \neg B \Rightarrow B)\) Gen
  3. \((\forall x)(\neg \neg B \Rightarrow B) \Rightarrow ((\forall x)(\neg \neg B) \Rightarrow (\forall x)B)\) 2.27#a
  4. \((\forall x)(\neg \neg B) \Rightarrow (\forall x)B\) MP 上述两个
  5. \(((\forall x)(\neg \neg B) \Rightarrow (\forall x)B) \Rightarrow (\neg(\forall x)B \Rightarrow \neg (\forall x)(\neg \neg B))\) Lemma 1.11#e
  6. \(\neg(\forall x)B \Rightarrow \neg (\forall x)(\neg \neg B)\) MP 上述两个

2.28 证明以下两个理论有相同的定理集合

令 \(K\) 是一个一阶理论，令 \(K^{\#}\) 是一个有如下公理的形式化理论：

• a \((\forall y_1)...(\forall y_n)B\)，其中 \(B\) 是 \(K\) 中的公理，\(y_1, ..., y_n (n \ge 0)\) 是任意变量
• b \((\forall y_1)...(\forall y_n)(B \Rightarrow C) \Rightarrow ((\forall y_1)...(\forall y_n)B \Rightarrow (\forall y_1)...(\forall y_n)C)\)， 其中 \(B\) 和 \(C\) 是任意公式，\(y_1, ..., y_n\) 是任意变量

且 MP 是 \(K^{\#}\) 的唯一演绎规则

这个证明可以表明了添加额外的公理能把 Gen 替换掉

2.29 证明 Extension of Propositions 2.4–2.7

上面已经证明了