• 4 一阶逻辑：证明论
  • 4.5 完全性定理
    • 预备
    • 可替代系统
    • 一致扩充的模型
  • 4.6 模型和一致性
    • 判定
  • 附录
• 勘误集
  • ml-4_3.pdf

4 一阶逻辑：证明论

4.5 完全性定理

预备

0. Q: 完全性定理是说“真值为真推出是定理”还是“重言式是定理”？
   A: 对于FOL，两者都不对。是“逻辑有效（任何解释真值为真）”推出是定理。
1. Q: 命题逻辑完全性定理Henkin证法：\(\mathscr A\)不是定理则其否定\(\sim\mathscr A\)能够被（）。扩充找到一组赋值使得\(\mathscr A\)赋值为（）从而（）。
   A: 加入系统不影响一致性
   0（假）
   不是定理就不是重言式（完全性定理得证）
2. Q: 下面开始比较一阶逻辑和命题逻辑的区别。
   对于证明\(\mathscr A\)不是定理则其否定\(\sim\mathscr A\)能够被加入系统而不影响（），我们需要用闭式保证（）定理能用。
   由上，可以得到“一致完全扩充”，和命题逻辑相同。
   A: 一致性，演绎
3. Q: 对比一阶逻辑和命题逻辑中完全性定理和“系统的完全性”
   A: 都是说包含的定理不能太少。
   命题逻辑：完全性定理是说包含一切重言式；系统（\(L\)的扩充）的完全性是说任何\(\mathscr A\)，其自身或者否定是定理。
   完全性定理是对一切\(L\)的扩充都成立的，但系统的完全性未必。
   一阶逻辑：完全性定理是说包含一切逻辑有效式；系统（\(K\)的扩充）的完全性是说任何闭式\(\mathscr A\)，其自身或者否定是定理。（回忆“闭式”和定理的联系）
   完全性定理是对一切\(K\)的扩充都成立的，但系统的完全性未必。
   两者类似，只有“闭式”一处不同。
4. Q: \(S^+\)系统作为\(S\)在\(\mathscr L^+\)的扩充是什么意思？
   A: 只是增加了一些\(\mathscr L\)常元。仍用原来的公理模式。
   所以可以把\(\mathscr A(b_1)\)换成\(\mathscr A(x_i)\)这样操作，从\(S^+\)的公理得到对应的\(S\)的公理。（当然，这需要\(S\)中常元、变元等不能都只有有限个）

可替代系统

0. Q: 为什么可替代系统只研究只含一个自由变元的公式就够了？
   A: 在证明一致扩充有模型时，Gen一次最多针对一个自由变元。如果Gen后是闭式那么Gen前最多一个自由变元。（回忆完全性定义中要求闭式）
1. Q: 回忆命题逻辑中技术，添加一条公理使得一致的体系不一致了，这就一定使得（）能\(\vdash\)（）。即添加的这条公理在原系统中是矛盾式。
   但是\(\sim \forall x_{i_n}\mathscr F_n(x_{i_n}) \to \sim \mathscr F_n(c_n)\)不可能是矛盾式，因为（）
2. Q: 上述步骤得到了一列一致扩充，先进行无穷次，得到\(S_\infty\)（也是（）扩充）。它是完全扩充吗？
   A: 一致。
   不是。认识论意义的完全扩充需要扩充的比它更多（不过具体技术有一点是类似的，都是扩充可数次，不影响一致性）
3. Q: 刚刚的一致完全系统只是说所有闭式都有了真值。那闭项呢？
   A: 我们构造的\(\mathscr L^+\)的解释\(I\)的论域\(D_I\)就是所有的闭项集合（可数集）。所以直接取解释就是对应的闭项即可。

一致扩充的模型

0. Q: 刚刚的一致完全系统可以帮助构造一致扩充的模型。归纳起点是（）
   对于\(\sim\)，注意如果\(\mathscr B\)在解释\(I\)不为真，则根据\(\mathscr B\)是（），有（）。
   对于\(\to\)也类似地利用（）性和（）式。并且需要重言式\(\mathscr B\to (\sim\mathscr C \to \sim(\mathscr B\to \mathscr C))\)等等。
   注：构造出的模型要“限制”一下，不能包含多余的记号的解释。
   A: 完全性（构造该系统时就规定了一切闭式的真值）
   闭式，\(\sim\mathscr B\)在解释\(I\)为真
   完全，闭
1. Q: 接上，对于\(\forall x_i\)，如果内层是闭式，那么很简单（可以用归纳假设）。内层不是闭式，不能直接用归纳假设，那注意到内层最多（）个（）变元就是（）。所以可以利用前述“可替代系统”指定的公式（）是公理做出论证。
   A: 1，自由，\(x_i\)，\(\sim \forall x_{i_m} \mathscr F_m(i_m) \to \sim \mathscr F_m(c_m)\)
2. Q:
   接上，具体地，\(I\models \mathscr A\)（其中\(\mathscr A\)是\(\forall x_{i_m} \mathscr F_m(x_{i_m})\)）推出\(I\models \mathscr F_m(c_m)\)（这里只用到（）论）
   从而（）。
   而如果\(I\)不\(\vdash \mathscr A\)则（），矛盾。
   A: 模型
   \(\vdash \mathscr F_m (c_m)\)（归纳假设）
   根据\(\mathscr A\)闭得到\(\vdash \sim\mathscr A\)从而根据公理得\(\vdash \sim\mathscr F_m(c_m)\)
3. Q: 反之，如果\(I\vdash \mathscr A\)但是存在一个赋值不满足，那么由于变元的赋值在论域中，也就是（），得到\(\vdash \sim\mathscr F_m(d)\). 进而容易得到矛盾。
   A: 闭项（如设为\(d\)）
4. Q: 由上证明完全性定理。若一个公式有效，则其（）有效。若一个公式不是定理，则其（）也不是定理（逻辑等价性）。于是（）被加入不影响一致性，而（）有模型，从而容易推出矛盾。
   A: 全称闭式，全称闭式，该公式否定，新的（一致）系统

4.6 模型和一致性

0. Q: 公式集的模型和一阶系统的模型有什么联系？
   A: 一阶系统的所有公理也是一个公式集。
1. Q: 为什么一致但不完全的一阶系统至少有两个不同的模型？
   A: 至少有两个不同的一致扩充。
2. Q: 由于“有模型推出一致”并不要求论域是否可数。所以对于存在（）模型的一阶系统，可以推出存在（）模型。
   A: 论域为不可数集的，论域为可数集的
3. Q: 论域基数小有模型则论域基数更大也有模型。那论域基数大有模型则论域基数小也有模型嘛？
   A: 不一定，比如\(\forall x_i A(x_i)\wedge \exists x_i \sim A(x_i)\)在论域为单元素集时无模型。
4. Q: 由于证明序列的有限，所以一阶系统的不一致性可以转化为（）条（）的（）。
   A: 有限，公理，不一致性
5. Q: 比较一致系统诱导模型与模型诱导一致系统的异同。
   A: 前者是对已知一致性和可靠性时考察认识论完全性，后者已知认识论完全性和可靠性时考察一致性。
   前者不一定唯一，后者唯一。等等

判定

0. Q: 公理化、完全、半可判定是何关系？
   A: 公理化和完全推出半可判定
   公理化：能行判断是否是公理（注意这里是一定“停机”）。但不一定能判断是否是定理。
   但如果这样了，就可以能行枚举公理，从而利用完全性定理能行枚举定理。
   联系理论计算机：停机一定是定理，但是不停机不知道是暂未停机还是不是定理。
1. Q: 不一致和判定是何关系？
   A: 不一致则一切公式都是定理。可判定。

附录

0. Q: 为什么之前说的FOL是广义FOL的特例，也是二阶逻辑的特例？
   A: 限制广义FOL的非逻辑符号可数，就是FOL
   一阶逻辑是二阶逻辑的子系统（只包含一部分符号，公理，模式）
1. Q: 二阶公理系统新增的公理和模式之中，哪些和之前的类比最不明显？
   A: 其它基本都有直接类比。只有谓词的引入（Comprehensive）和函项的引入（function definition）没有直接类比。
2. Q: 二阶逻辑可靠而不（）。所以我们不妨做出一定限制使其完全，并让他更容易在（）等领域应用。
   A: 完全，定理自动证明 数学 逻辑编程……

勘误集

ml-4_3.pdf

• p99 有个LaTeX引用没了。
• p103 也有
• p103 应当是“若有对象没有性质……”