Effectiveness and Computability

Sentential Logic

在不严谨地定义 effective 下给出 effective procedure 的特征：

指令有限，每一步的指令都是确定的
指令是机械的（non-intelligent），是可以被机器执行的
给定 wff $τ$ 的情况下，在有限的时间（通常是 $τ$ 的函数；只要求有限，数值可以很夸张到远超出现有硬件支持/时间认知的范围）内停止并给出确定性的答案
输入的形式也需要是有限的，因为现实不接受“无限”的现实性存在
我们的 Sentential Logic 语言系统实际上的符号数量是无限的，不过通过形如 $v_{3}$ 到 $v^{‴}$ 的替换，可以将我们的符号数量限制为有限的。

在这样不严谨的讨论环境下，我们的讨论范围无法囊括形如 “某一过程不存在 effective procedure” 的断言，不过对于正面的论证 effective procedure 的存在性时，直接给出符合以上特征的过程在一定程度上是可以接受的。

对于形式语言系统而言，我们讨论的对象都是表达式，表达式的全集是可数的。

可判定性（Decidability）：（狭义的，注意区别于计算理论中的可判定性）可判定性可以定义为：表达式集合 $Σ$ 是可判定的，当且仅当存在一个 effective procedure，其接受任意一个表达式 $α$ 作为输入，并输出 $α \in Σ$ 的正确性。

$Theorem 1$ ：所有 wff 构成的集合 $U$ 是可判定的。

可以利用 wff 的 parsing algorithm 来直接通过公式的结构判断。另一方面，由于 wff 构成的集合是 countable 的，所以也可以通过枚举比对来实现？wff 构成的集合是无限的，不能直接以列举的形式作为输入。

$Theorem 2$ ：存在 effective procedure，接受有限的 wff 集合 $Σ$ 以及 wff $τ$ 作为输入，并判断 $Σ$ tautologically imply $τ$ 的正确性。

由于 $Σ$ 的有限性，其真值表也是有限的，从而可以枚举真值表的有限取值。

$Corollary$ ：对于任意有限的 wff 集合 $Σ$ ，其 tautological consequences 是可判定的。特别地，所有重言式构成的集合是可判定的。

可有效枚举性（Effectively Enumerability）：其与半可判定性都是一种较弱的 "可判定性"，定义为：表达式集合 $Σ$ 是可有效枚举的，当且仅当 $Σ$ 可数（对于 Sentential Logic 而言这是正确的）且对于某个枚举 $E$ ，存在一个 effective procedure，其接受 $Σ$ 的一个元素 $ϕ$ 作为输入，输出 $E$ 以 $ϕ$ 结尾的前缀序列。特别地，当 $Σ$ 有限时，这个定义等价于可以将 $Σ$ 的所有元素以一定顺序输出。

半可判定性（Semidecidability）：表达式集合 $Σ$ 是半可判定的，当且仅当存在 effective procedure，其接受一个表达式 $α$ 作为输入，如果 $α \in Σ$ ，那么输出"正确"。

$Theorem 3$ ：表达式集合 $Σ$ 的半可判定性与可有效枚举性是等价的。

若 $Σ$ 可有效枚举，那么存在 effective procedure $P$ ，当 $α \in Σ$ 时，以 $α$ 作为输入执行 $P$ 必有输出，构造 $Q$ ：以 $α$ 作为输入执行 $P$ ，当 $P$ 输出时，输出 "正确"，从而 $Σ$ 是半可判定的。

若 $Σ$ 半可判定，假设有效程序为 $Q$ ，由于 Sentential Logic 中 wff 集合是可数的，所以我们枚举 wff： $φ_{1}, φ_{2}, φ_{3}, \dots$ ，我们定义任务 $i$ 为以 $φ_{i}$ 作为输入执行 $Q$ （即半判定 $φ_{i} \in Σ$ ），由于半判定程序不一定有输出，所以不能一个任务执行到死，将 $P$ 定义为以 $α$ 为输入的如下伪代码，由于 $P$ 的输出是一个以 $α$ 结尾的由 $Σ$ 中元素构成的序列，所以 $Σ$ 是半可判定的。

for (i = 1; ; i++)
	for (j = 1; j <= i; ++j)
		if task_i not ended
			do task_i for 1 second
			if task_i output "yes"
				output_list append varphi_i
				if varphi_i == alpha
					terminate and output output_list

其中任务的时间分配保证了每个任务都会被充分地执行（”充分“解释为任务如果没有结束那么其执行时间随着 $P$ 运行时间的增加可以任意大），任务时间分配方案不是唯一的，只要保证“每个任务都被充分执行”即可。

注意此处如果 $P$ 不终止的话，给定任何 $Σ$ 中的元素 $τ$ ，经过有限的时间后 $P$ 的输出序列可以包含 $τ$

$Kleene’s Theorem$ ：表达式集合 $Σ$ 可判定当且仅当 $Σ$ 和 $U ∖ Σ$ 均半可判定

充分性是显然的。必要性可以通过类似 $Theorem 3$ 的任务时间分配机制交替执行 $Σ$ 半判定 $α$ 和 $U ∖ Σ$ 半判定 $α$ 得到证明。

可判定集合构成的类、半可判定集合构成的类在集合交、集合并、集合补集操作下都是封闭的。

$Theorem 4$ ：如果 wff 集合 $Σ$ 是半可判定集，那么 $Σ$ 的 tautological consequences 构成的集合是半可判定的

设 $Theorem 2$ 中判定有限 wff 集合的 tautological consequence 的一个 effective procedure 为 $P$ 。考虑 $Σ$ 的某一个枚举（半可判定必可数；利用对应的半可判定程序可以生成这样的序列）： $σ_{1}, σ_{2}, σ_{3}, \dots$ 。对于任意 wff $τ$ ，确认 $Σ ⊨ τ$ 的正确性的半可判定程序 $Q$ 可以定义为利用 $P$ 依次确认 $\emptyset ⊨ τ, {σ_{1}} ⊨ τ, {σ_{1}, σ_{2}} ⊨ τ, \dots$ 。根据 Sentential Logic 的紧致性定理可以知道 $Σ ⊨ τ$ 时 $Q$ 一定会输出。

First-Order Logic

符号声明：

$Σ ⊨ τ$ 在本节中意味着 $Σ$ logically imply $τ$ 而不是 $Σ$ tautologically imply $τ$ 。

定义 Reasonable Language 为满足以下要求的（一阶逻辑）语言：

parameter 集合可以被有效枚举（意味着 parameter 集合可数）
${⟨ P, n ⟩ | P is a n-place predicate symbol}$ 和 ${⟨ f, n ⟩ | f is a n-place function symbol}$ 均可判定

仅仅包含有限参数的语言，称为有限语言（Finite Language），显然是 reasonable language。

$Enumerability Theorem$ ：对于 reasonable language 而言，valid wffs 构成的集合可以被有效枚举。

对于给定的 expression （reasonableness 决定了可以给定）， $⊨ τ$ 等价于 $⊢ τ$ ，构造程序：首先判断是否为 wff，再判断是否属于 $Λ$ （ $Λ$ 可判定），再判断是否 $Λ ⊢ τ$ （等价于 $Λ$ tautologically imply $τ$ ，根据 Sentential Logic 的 $Theorem 4$ 可以完成半可判定的判断）。

进一步地，如果限定为 finite language，也无法保证 valid wffs 是可判定的（因为 $Λ$ 不一定是有限的）

$Corollary$ ： $Γ$ 是 reasonable language 下的可判定的一个公式集合，那么 $Γ$ 的 theorems（或者 $Γ$ 的 logical consequences）所构成的集合是可有效枚举的

Proof 1: 由于 reduction inference 只涉及 sentential logic，所以如果 $τ$ 是 $Γ$ 的 theorem，那么 $Γ \cup Λ$ tautologically imply $τ$ ，因为 $Γ \cup Λ$ 是可判定的，依 Sentential Logic $Theorem 4$ $Γ \cup Λ$ 的 tautological consequences 是可以有效枚举的。

Proof 2: $Γ$ 的 tautological consequences 本质是 $Γ$ 本身在“所有普遍正确的公式（valid wff）”的假设下利用 modus ponens 进行扩充的结果，而所有 valid wffs 恰恰是用 $Λ$ 经 modus pones 的生成集合。枚举所有 valid wff，对于具有形式 $α_{n} \to α_{n - 1} \to \dots \to α_{1} \to α_{0}$ 的 valid wff，如果 $α_{1}, α_{2}, \dots, α_{n}$ 在 $Γ$ 中（可判定的），那么将 $α_{0}$ 加入 $Γ$ 的输出序列。Proof 2 是对 Proof 1 的具象化。

在构建公理化的理论时，我们期望我们的公理集合是可判定的，这意味着我们公理化的证明是"可以验证"的。

$Corollary$ ： $Γ$ 是 reasonable language 下的可判定的一个公式集合，若任意 sentence $σ$ 都有 $Γ ⊨ σ$ 或者 $Γ ⊨ \neg σ$ ，那么集合 ${σ is a sentence | Γ ⊨ σ}$ 是可判定的。

"任意 sentence 都有 $Γ ⊨ σ$ 或者 $Γ ⊨ \neg σ$ " 意味着如果 $Γ$ 是一致的那么 $Γ$ 是语义完备的（Semantically Complete），即 $Γ$ 足够强大，以至于可以决定任意 sentence 的真假。稠密无端点线性序是一个常见的语义完备的理论。在模型论中，可以用 $Łoś-Vaught$ 判别法来充分地判断一个理论是否为语义完备的。

$Γ$ inconsistent 时是显然的。 $Γ$ consistent 时，给定 $σ$ ，枚举 $Γ$ 的 logical consequences 并判断是否为 $σ$ 或 $\neg σ$ 。在 $Γ$ 语义完备时，我们可以确保 $σ$ 和 $\neg σ$ 至少其一在 $Γ$ 的 logical consequences 中出现。

注意在此处我们并不需要判断 $Γ$ 时 inconsistent 还是 consistent，因为它不是作为输入而是作为参数存在的，无论 $Γ$ 是否一致存在都存在对应的 effective procedure。