内涵逻辑（五）
假设我们有一个结构 ⟨D,R1,…,Rn⟩，并假设我们有一个与之关联的 LPCR 语言。此结构中的赋值 v 是从个体变量到 D 的成员的映射，也是从辅助关系符号到 D 上的偏关系的映射。我们希望将每个赋值 v 关联到一个从 LPCR 公式到真值的映射 Tv，但由于像说谎者句子这样的事物是可公式化的，因此 Tv 必须是偏函数，因此我们必须小心，即使是对于像命题联结词这样熟悉的事物也是如此。人们已经开发了各种三值逻辑；也许最常见的是克莱尼的强三值逻辑，它受到递归理论的启发，并且在真理论的大量研究中为人所熟知。下表说明了联结词和量词的行为方式。未明确涵盖的情况被理解为真值赋值未定义的情况。（例如，如果 X 的真值未定义，则 ¬X 的情况也是如此。)
Tv(¬X)≃t Tv(X)≃f
Tv(¬X)≃f Tv(X)≃t
Tv(X∧Y)≃t Tv(X)≃t 且 Tv(Y)≃t
Tv(X∧Y)≃f Tv(X)≃f 或 Tv(Y)≃f
Tv(X∨Y)≃t Tv(X)≃t 或 Tv(Y)≃t
Tv(X∨Y)≃f Tv(X)≃f 且 Tv(Y)≃f
对于 v 的所有 x 变量 v′，Tv((∀x)X)≃t Tv′(X)≃t
对于 v 的某些 x 变量 v′，Tv((∀x)X)≃f Tv′(X)≃f v
对于 v 的某个 x 变量 v′，Tv((∃x)X)≃t；对于 v 的某个 x 变量 v′，Tv′(X)≃t
对于 v 的所有 x 变量 v′，Tv((∃x)X)≃f；对于 v 的所有 x 变量 v′，Tv′(X)≃f
仍然需要处理一些公式。假设我们有以下公式：
ϕ0，其中 {P1(x1)≃ϕ1,…,Pk(xk)≃ϕk}
为了避免讨论过于复杂，我们做了两个简化假设。首先，我们假设 ϕi 不包含嵌套的 where 子句。在这个条件下，基本思想已经得到了充分的说明，但所有假设都很容易推广到一般情况。一般要求 xi 中的变量是 Pi(xi)≃ϕi 的“局部变量”，也就是说，它们在这个公式中被认为是绑定的。在此基础上，我们添加另一个简化假设：xi 中的变量是唯一可以在 ϕi 中自由出现的变量。粗略地说，这意味着我们没有参数，只有局部变量。这有助于我们更简洁地讨论问题。同样，一切都扩展到更一般的情况，没有根本的变化。
继续 (23)，考虑以下关联方程组 E。
P1(x1) ≃ϕ1
P2(x2) ≃ϕ2
⋮
Pk(xk) ≃ϕk
当然，困难在于每个 Pi 都允许出现在一个或多个 ϕj 中，甚至可能出现在 ϕi 中，因此 E 是自指的。在许多计算机编程语言中，我们会看到类似 x=x+1 的情况。向初学者解释，这会获取 x 的当前值，加 1，然后将结果再次调用 x。 x 在右侧出现时，取“之前”值；在左侧出现时，取“之后”值。类似地，我们将 E 的成员视为（同时的）赋值语句。Pi 在 ≃ 右侧的出现表示当前值，在 ≃ 左侧的出现表示后续值。考虑到 P1, ..., Pk 的全部，我们可以将 E 视为定义一个函数，它将 k 个偏关系元组（这些关系符号的“之前”值）映射到 k 个偏关系元组（这些关系符号的“之后”值）。现在，我们来更正式地阐述一下细节。
假设我们有一个 k 个偏关系元组 ⟨P1,…,Pk⟩，其中对于每个 i，Pi 的元数与偏关系变量 Pi 的元数匹配。这是我们的输入（“之前”值）。对于每个 i，我们需要定义一个输出偏关系，我们称之为 P
′
i
，其元数与 Pi 相同，这样 ⟨P
′
1
,…,P
′
k
⟩ 就是我们的总输出（“之后”值）。为此，我们必须对每个包含 D 元素的 d 分别说明 P
′
i
(d) 何时映射到 t，何时映射到 f，以及何时未定义。设 v 为赋值函数，将相应的偏关系 Pi 赋给每个辅助关系符号 Pi（这就是偏关系符号“之前”值的由来），并将 d 的相应成员赋给 xi 中的变量。现在，只需令 P
′
i
(d)≃Tv(ϕi)。这样就指定了一个新的偏关系 P
′
i
，更一般地说，指定了它们的向量 ⟨P
′
1
,…,P
′
k
⟩。方程组 E 可以被认为是一个函数，将 k 元组 ⟨P1,…,Pk⟩ 转换为 ⟨P
′
1
,…,P
′
k
⟩。设此函数为 [E]，记作 [E](⟨P1,…,Pk⟩)=⟨P
′
1
,…,P
′
k
⟩。
如果要使方程 E 在逻辑环境中表现良好，那么无论在哪里看到 Pi，每个 Pi 的值都应该相同——我们之前所说的左侧和右侧之间应该没有区别；Pi 和 P
′
i
应该相同。换句话说，我们希望有偏关系 P1, …, Pk 来解释 P1, …, Pk，使得 [E](⟨P1,…,Pk⟩)=⟨P1,…,Pk⟩——“之前”和“之后”的值一致。这被称为 [E] 的不动点。因此，我们需要知道 [E] 有一个不动点，如果它有多个不动点，那么就有一个合理的候选点，我们可以从中选择一个最佳不动点。
如果 f 和 g 是从空间 S 到 R 的两个偏函数，则写为 f⊆g，表示每当 f(x)≃w 时，g(x)≃w 也成立。那么，对于两个元数相同的偏关系 P 和 Q，P⊆Q 表示每当 P(d) 有定义时，Q(d) 也有定义，并且它们具有相同的真值。我们可以将其扩展到 k 元组，即如果对于每个 i，Pi⊆Qi，则设定 ⟨P1,…,Pk⟩⊆⟨Q1,…,Qk⟩。证明上面基于 (23) 定义的函数 [E] 具有单调性并不难：如果 ⟨P1,…,Pk⟩⊆⟨Q1,…,Qk⟩，则 [E](⟨P1,…,Pk⟩)⊆[E](⟨Q1,…,Qk⟩)。有一个非常普遍的单调映射理论，由此可以得出 [E] 确实存在一个不动点。此外，如果存在多个不动点，则存在一个唯一的最小不动点，即它与任何其他不动点都呈⊆关系。这个最小不动点正是我们上面提到的最佳候选者。它包含任何不动点都必须具备的信息。
现在我们讲完了如何求公式 (23)。首先，构造相关的方程组 E。接下来，构造函数 [E]。[E] 有一个最小不动点，我们假设它是 ⟨F1,…,Fk⟩。最后，用 Fi 计算 ϕ0，并解释每个 i 的 Pi。得到的真值，或者说未定义，就是与 (23) 相关的值（符号）。
现在我们已经讲完了如何将真值（或者说未定义）与 LPCR 的每个公式（在我们简化的假设下）关联起来。我们有（部分）符号。
4.4 意义
LPCR 的每个公式都指定了一种算法来求值，也就是确定其真值（如果可能）。Moschovakis 将公式的意义与该算法联系起来。两个求值结果相同（因此具有相同含义）的公式，由于其相关的算法不同，可能具有不同的意义。例如，在 (20) 中，我们给出了一个定义偶数的公式。这里是另一个这样的公式。
even(x)≡E(x)，其中 {E(x)≃x=0∨(∃y)(S(y,x)∧¬E(y))}
我们留给你验证 (25) 是否也定义了偶数。直观上看，(20) 和 (25) 使用不同的算法求值，因此意义也不同。但这当然必须精确。我们需要一种统一的算法比较方法。这里我们只是简要概述一下这些想法。
有一种非常通用的机制，源自 Moschovakis 1989 年提出的递归形式语言 (FLR)。使用它，可以彻底探索递归定义和不动点。我们这里讨论的语言 LPCR 嵌入到 FLR 中，甚至允许嵌套子句和参数，这是我们在讨论外延时忽略的。FLR 中有一种将递归定义转换为范式的方法，该范式无法进一步简化。该范式结构非常简单，由一组自指方程组成，完全没有嵌套。范式最清晰地揭示了本质的求值结构。当使用单一结构 ⟨D,R1,…,Rn⟩ 时，所有范式都将基于一组通用泛函构建。这使得比较范式变得容易。其原理是，如果 LPCR 的两个公式嵌入到 FLR 中时，它们的范式不同，则这两个公式的含义也不同。当然，这必须有一定的灵活性。例如，两组仅在变量重命名或方程顺序改变方面不同的方程，其本质上并无区别。理解了这一点，如果两个 LPCR 公式嵌入到 FLR 中时，具有真正不同的范式，则这两个 LPCR 公式被定义为具有不同的意义。这满足了人们希望意义概念具备的所有非形式化条件。Moschovakis 甚至证明了一个重要定理：意义相等，按照上述定义，在自然条件下是可判定的。
4.5 算法不必有效
“算法”一词暗示着某种有效的东西，但在这里，它被用作更广义的用法，作为一组指令，由于我们有限的局限性，我们可能无法真正执行这些指令。再次考虑范式公式 (22)。如果其中一个 ϕi 在正位置包含一个存在量词（或在负位置包含一个全称量词），则可以将其理解为在域 D 中调用系统性搜索来寻找可验证的证人。对于合理的域，这似乎是合理的。但如果 ϕi 在正位置包含一个全称量词或在负位置包含一个存在量词，则必须对域中的每个成员进行验证，除非域是有限的，否则这并非人工任务。尽管如此，我们通常认为我们理解量化。我们所处理的是与这种理解相关的算法。
量词的问题对于我们经常使用意义和指称进行讨论的许多内容而言是不可避免的。考虑一下罗素对定性描述的处理。在这种情况下，“A 具有属性 B”被替换为“恰好有一个事物具有属性 A 并且它具有属性 B”。要说只有一件事物具有属性A，就等于说某物具有属性A，而其他所有事物都不具有。这其中，第一部分涉及存在量词，第二部分涉及全称量词。如果明确的描述出现在正位置，则我们得到全称量词的正出现；如果它出现在负位置，则我们得到存在量词的负出现。无论哪种方式，都会出现本质问题。Moschovakis并非声称要将意义和指称转化为可计算的东西，而只是提供一种数学机制，能够使用广义的算法概念合理地形式化所涉及的思想。
还有第二个相关的问题，即有效性的缺失。在讨论指称时，我们考虑了一组方程(24)的集合E和一个与之相关的函数[E]。回想一下，[E]将k个偏关系元组映射到k个偏关系元组。我们注意到[E]将是单调的，并且根据非常普遍的结果，这样的函数总是具有最小不动点。有多种方法可以证明这一点。一个著名的论证带有明显的算法色彩。它如下：从最小的k元组偏关系开始——在这个k元组中，每个偏关系始终都是未定义的。将其设为T0。将函数[E]应用于T0，得到T1。将函数[E]应用于T1，得到T2，依此类推。很容易证明T0⊆T1⊆T2⊆……。我们之所以有T0⊆T1，是因为T0与每个k元组都存在⊆关系。根据单调性，我们有[E](T0)⊆[E](T1)，但这表示T1⊆T2。依此类推。继续这个递增序列，最终将达到[E]的最小不动点。
但这很容易误导。“继续”是什么意思？我们有T0，T1，T2，……这些都不是不动点。例如，假设我们利用由 (20) 式得到的关于 even(x) 的泛函进行上述构造。则 T0 将为 ⟨E0,O0⟩，其中 E0 和 O0 均为处处未定义的一位元关系。我们留给您检验是否得到连续的 Ti=⟨Ei,Oi⟩，其中有以下内容，未显示的情况表示未定义。
i Ei Oi
1 E1(0)=t O1(0)=f
2 E2(0)=t O2(0)=f
E2(1)=f O2(1)=t
3 E3(0)=t O3(0)=f
E3(1)=f O3(1)=t
E3(2)=t O3(2)=f
⋮ ⋮ ⋮
T0、T1、T2……都不是不动点，但有一个明确的极限概念，称为 Tω，它会累积沿途产生的结果。在本例中，它是最小不动点。
但仅仅迭代并取极限可能还不够。考虑以下对 (20) 的详细说明。
ϕ(x)≡A(x)，其中 { E(x)≃x=0∨(∃y)(S(y,x)∧O(y)),
O(x)≃(∃y)(S(y,x)∧E(x)),
A(x)≃x=1∧((∀y)(E(y)∨O(y))}
由 (26) 式得到的方程组包含 (20) 式中的两个成员，以及 A 的一个成员。利用这些方程，为了得出 A(1)，我们必须已经存在 E(y) 或 O(y) 中的一个，对于每个数 y 求值为 t。如果我们进行上面概述的构造，直到阶段 ω 时，我们才能得到 E 和 O 的这个结果，因此我们必须再进一步，到达所谓的 Tω+1，才能到达不动点。
可以给出更多极端的例子。不动点的构造可能需要继续进行到更大的以及更大的超限序数。这是一个众所周知的现象，尤其是在真理论等领域。它无法避免。顺便提一句，需要注意的是，克里普克在其真处理中引入的机制自然地嵌入到了LPCR中，但我们在此不讨论这一点。
