判定问题
数理逻辑中解决判定问题是要寻求一个具有一般性的方法(能行的方法)，从而能够判定某一类事物中的任一个是否有某种性质，能够得到某一类问题中的任一个的解答
能行方法
- 直观来说，能行的方法就是机械的方法：每一步都是由某个事先给定的规则明确规定了的并且在有穷步内可以结束的方法
- 规定了第一步如何作，并且在某一步作完之后下一步的作法也是明确规定了的
- 数学中一般的定理证明就不是能行的
能行可判定
一类问题或一类事物中的任一个是否具有某一特定性质是能行可判定的，当且仅当存在着一种能行的方法，此方法能够对此类问题中的任一个作出解答
对狭谓词演算而言，下列问题是能行可判定的：
- 任一符号是否是初始符号
- 任一符号序列是否合式
- 任一合式公式是否为一公理
- 任一合式公式是否能直接从某一个或某两个公式根据变形规则得到
- 任一给定的公式序列是否为一证明
- 狭谓词逻辑的以下问题不是能行可判定的：
- 任一公式是否可证，是否为一定理
- 任一公式是否普遍有效
- 任一公式是否可满足(有穷步内可对可满足公式作出肯定解答的方法应用于不可满足公式将永无休止而得不到否定的解答)
建立一个逻辑演算时总是要求在此系统内1~5是能行可判定的
- 数理逻辑的判定问题指
- 可证性的判定问题
- 普遍有效性的判定问题
判定问题是数理逻辑的重要问题
- 判定问题的解决有赖于能行方法的获得
- 判定问题研究的内容：可证明性和普遍有效性
- 普遍有效性问题实际上是逻辑公式所表达的命题的正确性问题
- 一公式的可证明性问题是一公理系统的推演能力问题，间接地也是此公式是否普遍有效的问题
普遍有效的公式是正确的推理形式，正确的推理形式是数理逻辑的基本内容
某些情况下，普遍有效性的判定是正确推理形式的判定
- 可证明性和普遍有效性问题一般地是不可判定的
- 某些较为简单的系统里是可判定的：如命题演算公式的普遍有效性问题可以通过真值表方法能行地判定，公式的证明可以通过范式判定
- 某些特殊类型的公式的判定问题是可以解决的
赋值方法
- 设有k个体域 ${ a_1, a_2, …, a_k }$，在此个体域中各种变项和公式的取值范围如下：
- 命题变项取真、假二值
- 个体变项可取 ${ a_1, …, a_k }$ 中任一为值
- 一n元谓词变项可取 ${ a_1, a_2, …, a_k }$ 上任一具体n元谓词为值
狭谓词演算公式的真值决定于所含谓词的外延，而等值的谓词的外延都相同
从公式的真值来说，外延相同的谓词都可算是相同的
在k个体域 ${ a_1, a_2, …, a_n }$ 上某一具体谓词的外延是 ${ a_1, a_2, …, a_n }$ 上某一类特定的n元组
- 例如：个体域 ${ 1, 2 }$ 上二元谓词 $x \leq y$ 的外延为一类二元组 ${ <1, 1="">, <1, 2="">, <2, 2=""> }$
在 ${ a_1, …, a_n }$ 上共有$2^{k^{n}}$个不同的由n元组构成的类
- 即$2^{k^n}$个不等值或不同的n元谓词：逻辑函项
- $¬, \bigvee, \bigwedge, \rightarrow, \leftrightarrow$ 作为定义在真假二值上的真值函项与以前相同
- 公式 $(x)A(x)$ 的值为真，如果 $A(x)$ 对于x在 ${ a_1, …, a_k }$ 中的每一个值都为真，否则 $(x)A(x)$ 的值为假；公式 $(\exists x)A(x)$ 的值为真，如果对于x在 ${ a_1, …, a_k }$ 中的某些值为真，否则 $(\exists x)A(x)$ 的值为假
对于个体域，任一变项能取的值的数是有穷的
- 赋值：假定一公式中的一系列变项取该个体域中某一特定系列的值(赋值系)
- 若对于一k个体域中一切赋值系，一公式都是真的，则该公式是普遍有效的；若有一赋值系使公式为真，该公式是k可满足的
- 若一公式对于任一不空的个体域中一切赋值系都是真的，该公式是普遍有效的；若有一不空的个体域，其中有一赋值系使公式为真，该公式就是可满足的
定理一：公式在一个体域中的可满足性和普遍有效性依赖于其中个体的数目
- 例：$(x)(\exists y)(x < y)$ 在个体数目有穷的情况下不可满足；传递的关系R，$(x)(\exists y)R(x, y)$ 在有穷个体域里必是自反的，但在无穷个体域中自反的性质不是普遍有效的
定理二：公式在一个体域中可满足性和普遍有效性质依赖于个体域中个体的数目
- 一公式若在某一个体域中可满足或普遍有效的，则在个体数目相同的个体域中也是可满足的或普遍有效的
定理三：若个体域是有穷的，则判定方法常有
- 对于有穷个体域，经过特定转换谓词逻辑的公式都可转换为命题逻辑的公式，而命题逻辑的公式总是可判定的
定理四：(1)若公式A为k普遍有效的，则¬A为k不可满足的，反之亦然；(2)若A普遍有效，则¬A不可满足，反之亦然
定理五：若A为 k(k>0) 可满足，则A也是 k+1 可满足
定理六：若A为 k(k>1) 普遍有效，则A也是 k-1 普遍有效
在有穷个体域中谓词逻辑公式的判定方法是常有的
在无穷个体域中一般的判定方法是不存在的，并且是不可能存在的对于普遍有效性，在较小(个体数目较少)个体域里不是普遍有效的公式在较大的个体域里也必然不普遍有效；在小的个体域里普遍有效的公式，在大的个体域里不一定普遍有效
对于可满足性，一个在小的个体域里可满足的公式，在更大的个体域里也可满足；在小的个体域里不可满足的公式，在较大的个体域里不必不可满足
定理七：只含有一元谓词变项的公式是能行可判定的
- 设A含有k个一元谓词变项而无多元谓词变项，若A在任一不大于$2^k$的个体域普遍有效，则A常普遍有效
定理八：形式为 $(x_1)(x_2)…(x_m)A(x_1, …, x_m)$ 的公式，其中A无量词且无其它自由个体变项，其判定方法常有
- 若此公式m普遍有效，则常普遍有效
定理九：形式为 $(\exists x_1)(\exists x_2)…(\exists x_m)A(x_1, …, x_m)$ 的公式，其中A无量词且无其它自由个体变项，其判定方法常有
- 若此公式在只有一个个体的个体域中普遍有效，则常普遍有效
定理十：形式为 $(x_1)(x_2)…(x_m)(\exists y_1)(\exists y_2)…(\exists y_n)A(x_1, …, x_m, y_1, …, y_n)$ 的公式，其中A无量词且无其它自由个体变项，其判定方法常有
- 若此公式m普遍有效，则常普遍有效
一致性
狭谓词演算是一致的
无穷个体域和一些困难问题以及悖论有深刻的联系，而一个系统的一致性证明就是证明系统中不会出现悖论(逻辑矛盾)
在一致性证明中要避免涉及无穷个体域的全体，使用的方法必须是能行的非能行的方法其本身的可靠性就有待于证明，不能作为证明一致性的方法
- 三种一致性：古典的、语义的、语法的
- 狭谓词演算在古典的和语法意义下的一致性可以能行地证明
- 语义一致性在有穷个体域中可以能行地证明，无穷个体域中只能用非能行的方法证明
定义：A是和谓词演算的公式A相联的命题演算公式，当且仅当A是用以下方法得到的
- 划去一切量词
- 用相同的命题变项代替相同的谓词变项，不论在此谓词变项的目式里出现的个体变项是否相同。 例如：和 $(x)F(x) \rightarrow F(y)$ 相联的公式是 $p \rightarrow p$
与A相联的公式实际上是当个体域中的个体只有一个时经过转换而与A相对应的命题演算公式
引理一：和谓词演算的六个公理相联的公式都是重言式
引理二：谓词演算的变形规则保留以下性质：有一个重言的相联的公式
- 如果某些公式的相联公式是重言式，那么从这些公式出发应用变形规则所得公式仍以重言式为其相联公式
引理三：在谓词演算里一切可证的公式，其相联的公式都是重言式
一致性定理一：狭谓词演算是在古典的意义下一致的，即不可能有一公式A，并且A和¬A都是在演算里可证的
一致性定理二：狭谓词演算是语法一致的，即有一公式A，A在演算中是不可证的
有效性定理一：对任一给定的整数 $k(k \geq 1)$，狭谓词演算的定理都是k普遍有效的
- 引理(一)：狭谓词演算的公理都是k普遍有效的
- 引理(二)：狭谓词演算的变形规则保留k普遍有效性
根据有效性定理一，可以得到狭谓词演算一致性的证明(古典的、语法的)
有效性定理的证明是能行的，是因为在有穷个体域中赋值系数目有穷，因而赋值方法是能行的
若个体域为无穷，则赋值系有无穷多，一般地，赋值方法就不是能行的
有效性定理二：狭谓词演算的定理都是普遍有效的
- 非能行证明
完全性
狭谓词演算在一切普遍有效的公式都是可证的这个意义下是完全的：语义的完全性(相对于解释的完全性)
其他两种完全性狭谓词演算都不具有
- (一)古典的完全性：对任一公式A，或者A可证或者¬A可证；这种完全性是针对不含有自由变项的公式，命题演算和狭谓词演算都含有自由变项
- (二)语法的完全性：把一不可证的公式作为公理增加到已有的公理中，可以使系统里任一公式都是可证的
狭谓词演算的完全性定理(语义意义下的完全性)
- 在狭谓词演算里凡普遍有效的公式都是可证的
- 在狭谓词演算里任一公式或者是可证的，或者不普遍有效
- 在狭谓词演算里任一公式A，或者A是可证的，或者¬A是可满足的
证明略…
骆文海-司寇伦定理：若狭谓词演算的一个公式A在自然数的个体域中普遍有效，则A常普遍有效
引用
- 《数理逻辑引论》，王宪钧，北京大学出版社