特定理论扩展的局部性结果解读

### 特定理论扩展的局部性结果解读 在理论研究中，理论扩展的局部性是一个重要的概念，它对于解决许多逻辑和计算问题具有关键作用。本文将深入探讨特定理论扩展的局部性结果，包括局部扩展的示例、绝对自由数据结构上的函数、递归定义函数的类别以及递归定义与有界性的结合等内容。 #### 局部扩展示例 理论扩展的局部性可以通过直接证明，也可以通过证明部分模型可嵌入到全模型来证明。以下是一些局部理论扩展的例子： 1. **带有自由函数符号的理论扩展**：任何带有自由函数符号的理论扩展都是局部的。 2. **满足特定公理形式的函数扩展**：对于任何基础理论 \(T_0\)，如果扩展的函数满足以下形式的公理，则该扩展是局部的： - \(GBounded(f)\)：\(\bigwedge_{i = 1}^{n}(\varphi_i(x) \to s_i \leq f(x) \leq t_i)\) - 其中 \(\Pi_0\) 包含一个具有自反二元关系 \(\leq\) 的排序 \(s\)，\(s_i\) 和 \(t_i\) 是 \(\Sigma_0\) 项，\(\varphi_i\) 是 \(\Pi_0\) 公式，且对于 \(i \neq j\)，\(\varphi_i \land \varphi_j \models_{T_0} \bot\)，同时 \(T_0 \models \forall x(\varphi_i(x) \to s_i(x) \leq t_i(x))\)。 #### 绝对自由数据结构上的函数 我们定义了绝对自由构造函数的理论 \(AbsFree_{\Sigma_0}\)，它由以下公理组成： - \((Inj_c)\)：\(c(x_1, \ldots, x_n) = c(y_1, \ldots, y_n) \to \bigwedge_{i = 1}^{n} x_i = y_i\) - \((Acyc_c)\)：如果 \(x\) 出现在某个 \(t_i\) 中，则 \(c(t_1, \ldots, t_n) \neq x\) - \(Disjoint(c, d)\)：如果 \(c \neq d\)，则 \(c(x_1, \ldots, x_n) \neq d(y_1, \ldots, y_k)\) 需要注意的是，\((Acyc_c)\) 是一个公理模式，表示无限个公理。以下理论是局部的： 1. **绝对自由构造函数理论**：\(AbsFree_{\Sigma_0}\) 是局部的。 2. **去除部分构造函数无环条件的理论**：从 \(AbsFree_{\Sigma_0}\) 中去除一组构造函数 \(\Sigma \subseteq \Sigma_0\) 的无环条件后得到的理论 \(AbsFree_{\Sigma_0 \setminus \Sigma}\) 是局部的。 3. **带有选择器的理论**：\(T \cup Sel(\Sigma')\) 是局部的，其中 \(T\) 是上述 (1) 或 (2) 中的理论，\(Sel(\Sigma') = \bigwedge_{c \in \Sigma'} \bigwedge_{i = 1}^{n} Sel(s^c_i, c)\) 公理化了一组选择器 \(s^c_1, \ldots, s^c_n\)，对应于构造函数 \(c \in \Sigma' \subseteq \Sigma_0\)。这里 \(Sel(s_i, c)\) 定义为：\(\forall x, x_1, \ldots, x_n (x = c(x_1, \ldots, x_n) \to s_i(x) = x_i)\)。 此外，\(K = AbsFree_{\Sigma_0} \cup Sel(\Sigma_0) \cup IsC\) 具有以下性质：对于任何一组基础 \(\Sigma_0 \cup Sel \cup \Sigma_c\) 子句 \(G\)（其中 \(\Sigma_c\) 是一组额外的常量），\(K \land G \models \bot\) 当且仅当 \(K[\Psi(G)] \land G \models \bot\)，其中 \(\Psi(G) = st(G) \cup \bigcup_{a \in \Sigma_c \cap st(G)} \bigcup_{c \in \Sigma_0} (\{s^c_i(a) | 1 \leq i \leq a(c)\} \cup \{c(s^c_1(a), \ldots, s^c_n(a))\})\)。 这个结果的证明是通过证明 (a) - (c) 中公理的每个弱部分模型都可以弱嵌入到公理的全模型中。局部性则从 [7] 中建立的可嵌入性和局部性之间的联系得出。 通过这个结果实现的向纯等式理论的归约与 Oppen 的方法非常相似，用于通过双向闭包来判定自由递归数据结构的基础公式的可满足性。结合量词消去和这个归约，可以得到由 \(AbsFree_{\Sigma_0} \cup Sel(\Sigma_0) \cup IsC\) 公理化的绝对自由构造函数的一阶理论的判定过程。 #### 一类递归定义的函数 我们考虑 \(AbsFree_{\Sigma_0}\) 的扩展，引入新的函数符号，这些函数的余域可能是不同的排序。假设签名 \(S = \{d, s\}\)，其中 \(d\) 是“数据”排序，\(s\) 是不同的排序（一些递归定义函数的输出排序）。 设 \(T_s\) 是排序 \(s\) 的理论。我们考虑 \(AbsFree_{\Sigma_0}\) 和 \(T_s\) 的不相交组合的扩展，扩展的函数集合为 \(\Sigma = \Sigma_1 \cup \Sigma_2\)，其中 \(\Sigma_1\) 中的函数的元数为 \(d \to d\)，\(\Sigma_2\) 中的函数的元数为 \(d \to s\)。 对于每个 \(f \in \Sigma\)，我们指定一个子集 \(\Sigma_r(f) \subseteq \Sigma_0\)，表示存在 \(f\) 的递归公理的构造函数集合。我们考虑以下形式的理论： - \(T = AbsFree_{\Sigma_0} \cup T_s \cup Rec_{\Sigma}\)，其中 \(Rec_{\Sigma} = \bigwedge_{f \in \Sigma} Rec_f\) 是一组公理，形式如下： - \(Rec_f\)： - \(f(k) = k_f\) - \(f(c(x_1, \ldots, x_n)) = g_{c,f}(f(x_1), \ldots, f(x_n))\) - 其中 \(k\) 和 \(c\) 遍历 \(\Sigma_r(f) \subseteq \Sigma_0\) 中的所有构造函数，\(a(k) = 0\)，\(a(c) = n\)，\(k_f\) 是基础 \(\Sigma_{o(f)}\) 项，\(g_{c,f}\) 可以用 \(\Sigma_{o(f)}\) 项表示。 我们还考虑满足以下形式的受保护递归定义的函数扩展： - \(Rec^g_{\Sigma} = \bigwedge_{f \in \Sigma} Rec^g_f\) - \(Rec^g_f\)： - \(f(k) = k_f\) - \(f(c(x_1, \ldots, x_n)) = \begin{cases} g_{c,f}^1(f(x_1), \ldots, f(x_n)) & \text{如果 } \varphi_1(f(x_1), \ldots, f(x_n)) \\ \vdots \\ g_{c,f}^k(f(x_1), \ldots, f(x_n)) & \text{如果 } \varphi_k(f(x_1), \ldots, f(x_n)) \end{cases}\) - 其中 \(k\) 和 \(c\) 遍历 \(\Sigma_r(f) \subseteq \Sigma_0\) 中的所有构造函数，\(a(k) = 0\)，\(a(c) = n\)，\(k_f\) 是基础 \(\Sigma_{o(f)}\) 项，\(g_{c,f}^i\) 可以用 \(\Sigma_{o(f)}\) 项表示，\(\var