计算机科学逻辑/查询

查询和可定义性

可满足性问题是数学逻辑的核心：对于结构域 D 上的逻辑 L，尝试在 D 中找到给定公式 φ 从 L 的模型。在逻辑 L 和结构域 D 上的模型检验的更特殊问题尝试回答，${\mathfrak {A}}\vDash \psi \$ 是否对给定结构 ${\mathfrak {A}}\in D$ 和公式 $\psi \ \in L$ 成立。模型检验是计算机科学中的一个重要领域。查询的概念超越了这些“真假”评估，它引入了结果集作为其结果。

查询

动机

想想一个客户数据库。现在可以查询这样的数据库，例如“所有非洲客户”，这将导致所有非洲客户的列表。对于像“所有客户及其国家”这样的查询，结果将包含客户和国家的二元元组，而查询“（我们）有卢旺达的客户吗？”会导致是或否。类似地，可以定义对结构的查询，这些查询提供宇宙元素的集合，其中宇宙与数据库中的数据相关联。

概念

首先重新捕获绑定变量和自由变量的概念：而像 $\forall _{x}\exists _{y}xRy$ 这样的句子（没有自由变量）计算为真或假，公式的 $\forall _{x}xRy$ 真值相对于自由变量 y，因此意味着 y 的值的集合，对于这些值它是真的。一般来说，对于一个具有 n 个自由变量的公式，我们得到一个 n 元组的集合（它也可能为空）。从这个意义上讲，句子在它们为真时提供 0 元组。

定义

令 ${\mathfrak {A}}$ 是具有宇宙 A 的 S 结构，m 是一个非负整数，Q 是从 S 结构到 A^m 的子集的集合的映射，使得每个 ${\mathfrak {A}}$ 映射到 A^m 的子集。

如果 Q 在同构下是封闭的，则称 Q 是 S 结构上的 m 元查询，

其中在同构下封闭（或保留）是：如果 ${\mathfrak {A}}\cong {\mathfrak {B}}$ 通过同构 $f$ 那么 $f(Q({\mathfrak {A}}))=Q({\mathfrak {B}})$.

备注

• 0 元 Q 也称为布尔查询。在这种情况下，Q 映射到 A⁰，即 0 元组，或空集。前一个结果也称为 TRUE，后一个结果称为 FALSE。
• 对于布尔查询 Q，可以定义 S-结构的子集 C 为：${\mathfrak {A}}\in C$ 当且仅当 $Q({\mathfrak {A}})=true$
• 封闭条件确保只查询结构的“形状”，即宇宙的构成无关紧要，只要它们以相同的方式相关联。因此，有关宇宙元素类型的问题无法通过查询得到解答。
• 从一元查询中，可以得到查询结构 ${\mathfrak {A}}$ 的子结构 ${\mathfrak {B}}$，方法如下：

  $R^{\mathfrak {B}}=R^{\mathfrak {A}}\cap Q^{m}$，对于 m 元 R，并且常数有 1-1 映射。

示例

简单示例

取 S = {<}。我们查询“所有没有更小元素的元素”。对于宇宙 {10, 11, 12}，这将得到结果 {(10)}（一组一元元组）。查询“所有具有更小元素的元素”将得到 {(11), (12)}。查询“所有直接后续元素”将得到 {(10, 11), (11, 12)}（一组二元元组）。查询“存在最大元素”将得到 {()}（零元元素），而“不存在最大元素”将得到 {}（假）。

图

对图 $G=(V,E)$ 的典型查询是：

• 传递闭包（最小的传递扩展）是一个二元查询

  ${\big \{}(x,y)\in V^{2}|{\mbox{ there is a path from x to y }}{\big \}}$

• 孤立节点是一个一元查询

  $\{(x)\in V|{\mbox{ there is no node connected with x }}\}$

• 平面性是一个零元（布尔）查询

  ${\begin{cases}\{()\}&{\mbox{if G is planar}}\\\{\}&else\end{cases}}$

可定义性

一方面，我们有或多或少“复杂”的查询。只需考虑一个简单的数据库查询，查询所有名为“Ubuntu”的客户，与查询名为 Ubuntu 且不在非洲或中东的客户相比。另一方面，我们有不同表达能力的语言，如 FO 和 MFO（一阶单调逻辑）。因此，人们可以问一个语言的表达能力是否足够强大以表达（定义）某个特定的查询。

结构类别的定义

令 C 为有限结构的类，L 为逻辑。如果存在 L 中的句子 φ，使得 C 是 φ 的所有有限模型的集合，则称 C 在逻辑 L 中可定义。

查询的定义

令 Q 为查询，L 为逻辑

如果存在 L 中的公式 φ(x₁, ..., x_m)，使得对于所有 ${\mathfrak {A}}$，$Q({\mathfrak {A}})$ 中的所有元素都是 φ 的赋值，使得 ${\mathfrak {A}}\vDash \varphi$，则称 Q 在 L 中可定义。

示例

简单示例

在有限图上，查询“存在一个与所有其他元素相邻的元素”可以用 FO 写成 $\exists _{x}\forall _{y}xRy$。该语言甚至可以进一步限制，例如，只允许每个公式使用 2 个变量（因此在逻辑 FO² 中可定义）。

负面

图的单步连通性可以用 FO 定义为

$\forall _{xy}E(x,y)$

因此，我们得到了 2 步连接性，

$\forall _{xz}\exists _{y}E(x,y)\land E(y,z)$

这可以扩展到固定 n 的 n 步连接性，但不能扩展到任意 n，因为 FO 公式的长度总是固定的。要将上述方法扩展到任意长度，需要一些“无限合取”。由于 FO 中没有其他方法来表达任意连接性（这里省略了部分内容），因此我们说连接性查询在 FO 中不可定义。可以证明它可以在 UMSO（通用单调二阶逻辑）中表达。

图

上面讨论的查询的可定义性如下：

• 传递闭包查询在 FO 中不可定义
• 孤立节点查询在 FO 中可定义为

  $\forall _{y}\neg E(x,y)$

• 平面性在 FO 中不可定义

命题

查询安全性

待办事项

顺序的影响

待办事项

有限结构

概念

定义

当且仅当结构的全集是有限的时，该结构被称为有限结构。

示例

有限结构在计算机科学中的非凡有效性

计算机科学中的数据结构通常是有限的，例如数据库总是保存有限数量的条目。但是，当限制为有限结构时，我们有以下两个问题：

• 我们仍然需要处理任意大小的结构，例如，要从 1 加到 3，可以写成 1 + 2 + 3，从 1 加到 4：1 + 2 + 3 + 4，但从 1 加到任意自然数，我们必须使用一个特殊的运算符，如“Σ”，它扩展了我们简单的“+”语言（另外，“…”符号也不起作用，因为它也扩展了我们的语言）。
• 现在我们必须处理之前没有遇到的复杂性问题。示例...

有限模型论

因此，处理有限结构的理论（有限模型论（FMT））不仅仅是对涵盖无限结构的理论（模型论（MT））的简化。它有它自己的特点。这在证明方法方面尤其是一个问题。MT 中最重要的工具之一是紧致性定理，但当我们只处理有限结构时，它就完全没有用处。

考虑以下句子 σ3

$\exists _{x}\exists _{y}\exists _{z}(x\neq y\land y\neq z\land x\neq z)$

它表示宇宙中至少有 3 个不同的元素。可以轻松地扩展 σ3 以适用于 3 之外的其他 n。因此，令 Σ = {σ1, σ2, σ3, ...} 为所有这些句子的无限集合。现在，Σ 显然不能被有限模型满足，尽管 Σ 的每个有限子集都是可满足的。好吧，但这为什么重要呢？一般模型论中最有用的工具之一是紧致性定理，它指出：“令 Σ 为一组 FO 句子。如果 Σ 的每个有限子集都是可满足的，则 Σ 是可满足的。”但正如刚才所展示的，这对于有限情况并不成立，因此有限模型论中没有紧致性定理！

而且（不幸的是），对于许多其他重要定理（实际上是绝大多数定理）也是如此，例如哥德尔完备性定理。此外，MT 的重要定义必须适用于有限情况。例如，类型概念在 MT 中非常核心。但应用于 FMT 时，它被证明是相当无用的，因为它已经将有限结构表征为同构。因此，类型定义在 FMT 中必须被细化（到 FO[k] 中的类型概念，取决于整数 k）。

因此，有限模型论者不能简单地采用来自模型论的经典工具，他们必须找到自己的工具。基本工具在“证明”部分介绍。

基本等价性质

查询是关于区分结构的。因此，基本问题是“我能否将一个结构与所有不同的结构区分开来？”，其中“不同”意味着不等于同构。这可以对有限结构实现（但不能对无限结构实现）。例如...

有限数量结构的属性

因此，属于特定结构可以被视为一个基本属性，它将一类同构结构与所有其他结构区分开来。现在，我们可以考虑将两个不同的（非同构）结构与其他结构区分开来的属性。它们也可以通过简单地连接属性来区分开来，例如...

这可以扩展到有限数量结构的属性，例如...

无限数量结构的属性

还可以考虑那些对无限数量结构成立的属性。但这些属性无法以上述方式进行区分。例如...

有一些逻辑允许这种无限析取，例如...

那么，在 FO 中还有其他方法来区分这些结构吗？在某些情况下，就像在...的情况下一样。

因此，我们需要一个决策工具（方法）来判断具有特定属性的结构是否可以区分，即对所有可能的属性都给出“是”或“否”的响应，即具有健全性和完备性。

一阶逻辑和无限逻辑的特殊作用

待办事项