逻辑对局部属性的捕捉及模态逻辑可满足性问题的复杂度研究

### 逻辑对局部属性的捕捉及模态逻辑可满足性问题的复杂度研究 #### 1. 局部属性相关逻辑 在逻辑领域，对于局部属性的研究有着重要意义。首先，对于固定的 $d$，$L^∗_{∞ω}(C) + \{I^k_d | k > 0\}$ 仅能表达 Hanf 局部属性。并且，对于任意的 $d$ 和 $k > 0$，$L^∗_{∞ω}(C) + I^k_d$ 的表达能力严格强于 $L^∗_{∞ω}(C)$。这表明在 $L^∗_{∞ω}(C)$ 的基础上添加 $I^k_d$ 能增加逻辑的表达能力。由此还可得出，$L^∗_{∞ω}(C)$ 无法在任意有限结构上捕捉 Hanf 局部属性。 当把 $I^k_d$ 作为广义量词使用时，逻辑的定义会有所扩展。若 $\phi_1(\vec{v}_1,\vec{z}), \ldots, \phi_l(\vec{v}_l,\vec{z})$ 是公式，其中 $\vec{v}_i$ 是 $m_i$ 元的一阶变量元组，那么 $\psi(\vec{x}, \vec{y},\vec{z}) \equiv I^k_d[m_1, \ldots, m_l](\vec{v}_1, \ldots, \vec{v}_l)(\phi_1(\vec{v}_1,\vec{z}), \ldots, \phi_l(\vec{v}_l,\vec{z}))$ 也是公式。不过，这种扩展并不保留局部性。例如，向 $L^∗_{∞ω}(C)$ 中添加 $I^k_d[m_1, \ldots, m_l]$ 会破坏 Hanf 局部性，向一阶逻辑（FO）中添加 $I^1_1[2]$ 甚至可以定义既非 Hanf 局部也非 Gaifman 局部的属性。 为了填补 $L^∗_{∞ω}(C)$ 与 Hanf 局部性之间的差距，引入了局部二阶量化的概念。其思想类似于局部一阶量化，将量化变量限制在自由变量的固定半径邻域内。 下面是局部二阶量化逻辑的定义流程： 1. 固定 $r \geq 0$ 和关系签名 $\sigma$。 2. 对于每个 $k > 0$ 的元数，有可数无限集的 $k$ 元关系符号 $T^i_k$，$i \in N$，且与 $\sigma$ 不相交。 3. 从 $L^∗_{∞ω}(C)$ 涉及 $\sigma$ 以及 $T^i_k$ 的原子公式开始，通过 $L^∗_{∞ω}(C)$ 的形成规则以及以下规则来定义公式集 $F$： - 若 $\phi(\vec{x},\vec{\imath})$ 是公式，$\vec{y}$ 是 $\vec{x}$ 的子元组且 $d \leq r$，则 $\psi_1(\vec{x},\vec{\imath}) \equiv \exists T^i_k \subseteq S_d(\vec{y}) \phi(\vec{x},\vec{\imath})$ 和 $\psi_2(\vec{x},\vec{\imath}) \equiv \forall T^i_k \subseteq S_d(\vec{y}) \phi(\vec{x},\vec{\imath})$ 是秩为 $rk(\phi) + 1$ 的公式，且 $T^i_k$ 在这些公式中是约束的。 4. 定义 $LSOr_{∞ω}(C)$ 为 $F$ 中所有有限秩且 $T^i_k$ 符号的所有出现都被约束的公式集。 5. 局部二阶带计数逻辑 $LSO^∗_{∞ω}(C)$ 定义为 $\bigcup_{r\geq0} LSOr_{∞ω}(C)$。 其语义为：给定 $\sigma$ 结构 $A$ 和对 $\psi_1$ 中自由出现的所有 $T^i_k$ 符号的解释 $T$，$(A, T) \vDash \psi_1(\vec{a},\vec{\imath})$ 当且仅当存在集合 $T \subseteq S_d(\vec{b})^k$（其中 $\vec{b}$ 是 $\vec{a}$ 对应于 $\vec{y}$ 的子元组），使得 $(A, T, T) \vDash \phi(\vec{a},\vec{\imath})$；对于 $\psi_2$，将 “存在” 替换为 “对于所有”。 例如，公式 ```plaintext ∃x∃T ⊆ S_r(x)∃T ′ ⊆ S_r(x)   ∀y ∈ S_r(x) (T(y) ∧ ¬T ′(y)) ∨ (¬T(y) ∧ T ′(y)) ∧ ∀z, v (T(z) ∧ E(z, v) → T ′(v)) ∧ (T ′(z) ∧ E(z, v) → T(v))   ``` 用于测试图中是否存在节点的 $r$ 邻域是 2 - 可着色的。 主要结果表明，一个 $m$ 元查询 $Q$（$m \geq 0$）是 Hanf 局部的当且仅当它可以由 $LSO^∗_{∞ω}(C)$ 的公式（无自由二阶变量）定义。证明思路如下： 1. 首先证明 $LSO^∗_{∞ω}(C)$ 中可定义的查询是 Hanf 局部的。通过与文献中类似的论证，可在不增加公式秩的情况下从 $LSOr_{∞ω}(C)$ 中消除计数项。 2. 定义了 $(A, \vec{C},\vec{a}) \sim^r_d (B, \vec{D},\vec{b})$ 的关系，当满足三个条件时成立： - $(A,\vec{a}) \cong_d (B,\vec{b})$。 - $adom(\vec{C}) \subseteq S^A_r (\vec{a})$ 且 $adom( \vec{D}) \subseteq S^B_r (\vec{b})$。 - 存在同构 $h : N^A_d (\vec{a}) \to N^B_d (\vec{b})$ 使得 $h(\vec{C}) = \vec{D}$。 3. 引理 1 表明，对于 $LSOr_{∞ω}(C)$ 公式 $\phi(\vec{x},\v