計算機科學邏輯/查詢

查詢和可定義性

可滿足性問題是數學邏輯的核心：對於結構域 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 中還有其他方法來區分這些結構嗎？在某些情況下，就像在...的情況下一樣。

因此，我們需要一個決策工具（方法）來判斷具有特定屬性的結構是否可以區分，即對所有可能的屬性都給出“是”或“否”的響應，即具有健全性和完備性。

一階邏輯和無限邏輯的特殊作用

待辦事項