計算機科學邏輯/邏輯

子 FO 邏輯

模態邏輯

模態邏輯透過對模態“可能性”和“必要性”的運算子擴充套件了命題邏輯。這些基本的模態運算子通常用 $\Box$ (或L) 表示必然，用 $\Diamond$ (或M) 表示可能。每個都可以透過以下方式從另一個定義

$\Diamond P\leftrightarrow \lnot \,\Box \,\lnot \,P.$

合取邏輯

合取邏輯是 FO 的一個片段，它被限制為由合取連線的原子 FO 表示式，這些表示式可以被存在量詞所引導。它在資料庫理論中尤為重要。

定義 CON

1. 原子
2. $\varphi \land \psi$
3. $\exists _{x}\varphi$

備註

1. 換句話說：CON 公式是由原子公式構建的（關係）FO 公式，它只使用合取和存在量化。
2. FO 的語義相應地適用於此。
3. 自由變數和繫結變數的“通常”概念也適用於此。
4. 形式為 $\exists _{x_{1}}...\exists _{x_{n}}\varphi _{1}\land ...\land \varphi _{m}$ 的公式，其中每個 φ 都是無量詞的，被稱為正規化
5. 每個 CON 公式都等價於一個正規化公式
6. 所有 CON 公式都是可滿足的

例子

1. $\exists _{x}(\varphi (x,y)\land \psi (x,y))$ 有一個繫結變數 x 和一個自由變數 y。
2. $\exists _{x}(\varphi (x))\land \exists _{y}(\psi (y))$ 等價於 $\exists _{x}\exists _{y}(\varphi (x)\land \psi (y))$。後者被稱為標準形式。

等式

此外，可以透過以下方式引入變數或常量之間的等式

• $x\equiv y$

例如，不總是可滿足的。每個可滿足的 CON 公式都等價於一個沒有等式的公式。

高階邏輯

不動點邏輯

不動點邏輯透過一個不動點運算元來增強 FO 的語法，該運算元是一種允許表示式遞迴的機制，從而提高了表達能力。這個想法與在指令式程式設計語言中新增 while 迴圈結構非常相似。

示例 閉包

閉包的說明

考慮圖 G 的閉包。對於距離為一，我們有

$G(x,y)\,$

對於距離最大為二

$G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y))$

因此，我們可以透過擴充套件此析取來進一步固定距離（僅此而已）。為了表達任意距離的閉包（對於大多數情況至關重要），可以使用以下方法引入遞迴

$\varphi (T)=G(x,y)\lor T(x,y)\lor \exists _{z}(T(x,z)\land G(z,y))$

其中 T 是直到某個 i 的閉包。因此 φ(T) 給出了直到 i + 1 的閉包。因此，可以定義一個序列

$J_{0}=\emptyset ;J_{i}=\varphi (J_{i-1}),i>0$

很明顯，這給出了某個 k 的閉包，即序列收斂（即 J_k = J_k+j，對於所有 j > 0），並且它的極限是閉包。

在插圖中，我們有一個初始圖 G，如 (a) 所示，因此

(a) 為 $J_{1}=G(x,y)\,$

(b) 為 $J_{2}=G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y)$

不動點 (c) 為

$J_{3}=G(x,y)\lor \exists _{z}(G(x,z)\land G(z,y))\lor \exists _{z}(\exists _{t}(G(x,t)\land G(t,z))\land G(z,y))$

因此 J₃ = J₄ = ... 。

♣

正如我們在本例中所看到的，遞迴可以用來表達任意長度的公式。但由於我們在這裡始終處理的是有限的公式，因此必須為遞迴提供一些終止符。這個角色可以由不動點來扮演。在上面的例子中，這樣的不動點存在。但並非總是如此，正如我們接下來看到的。

示例

待辦事項 跳線

♣

正如我們在本例中所看到的，遞迴的不動點並不總是存在。因此，我們必須小心定義基於遞迴的邏輯。我們將 FO 擴充套件為 PFP，以處理存在不動點的情況。

部分不動點邏輯 (PFP)

待辦事項

♣

上述假設不動點存在並不真正令人滿意，因此現在可以考慮對遞迴進行限制，以確保在所有情況下都存在不動點。因此，引入了三個概念：遞迴的單調性、正性和膨脹性。

膨脹性不動點邏輯 (IFP)

概念

待辦事項 生命遊戲

定義

待辦事項

最小不動點邏輯 (LFP)

概念

待辦事項

定義

待辦事項

♣

IFP 和 LFP 的比較

待辦事項

♣