計算機科學邏輯/一階邏輯

一階邏輯

在命題邏輯中，我們考慮了關於原子物件的公式，這些物件只能是真或假。一階邏輯是本章的主題，它建立在命題邏輯的基礎上，並允許您檢視公式中討論的物件內部。我們可以透過將物件討論為大於集合 $\{0,1\}$ 的集合的元素，幷包括任意複雜的相互關係來提供這種更精細的粒度級別。

我們首先透過定義一階 (FO) 邏輯的語法開始，然後賦予這些結構意義。

語法

一階邏輯的討論域是一階結構或模型。一個一階結構包含

關係，
函式，以及
常量（元數為 0 的函式）。

一階邏輯的詞彙是

一組具有關聯元數的關係符號，以及
一組具有關聯元數的函式符號。

以下是一些示例一階邏輯詞彙

圖
- 關係集 = { $V$ : 一元， $E$ : 二元 }
- 函式集 = { ${\mathit {next}}$ : 一元 }
算術
- 關係集 = { $+$ : 三元， $\times$ : 三元， $\uparrow$ : 三元， $=$ : 二元， $<$ : 二元 }
- 函式集 = { ${\mathit {next}}$ : 一元， $0$ : 常量 }

這裡，圖是由一組頂點 $V$ 和一組邊 $E$ 組成。對於算術集，請注意使用 $+$ 和 $\times$ 純粹是語法上的，我們本可以使用“加”和“乘”符號來代替。我們還沒有給這些符號賦予任何意義。

項表示一階結構中的一個元素。項用於指代我們討論域中的元素。以下是描述項是什麼的規則

每個變數都是一個項，其中變數只是一個符號集合
每個常數都是一個項
如果 $t_{1},t_{2},\ldots ,t_{k}$ 是項，且 $f$ 是 $k$ 元函式，那麼 $f(t_{1},t_{2},\ldots ,t_{k})$ 是一個項。

例如，如果 $f$ 是一個二元函式，而 $g$ 是一個三元函式，那麼以下都是項： $x,a,f(x,y),g(x,f(x,y),a)$ .

原子公式是

R(t_{1},t_{2},\ldots ,t_{k})

,

其中 $R$ 是 $k$ 元關係，而 $t_{1},t_{2},\ldots ,t_{k}$ 是項。當將 $R$ 視為一個集合時，這只是另一種說法，即元組

(t_{1},t_{2},\ldots ,t_{k})\in R

.

一個特殊的“ $=$ ”關係表示“等於”，不能被解釋為其他含義。例如， $t_{1}=t_{2}$ 代表

=(t_{1},t_{2})

.

一階公式是由給定的一階詞彙表、變數和符號 $(,),\neg ,\vee ,\wedge ,\rightarrow ,\exists ,\forall$ 構成的表示式。一階公式的集合是滿足以下條件的最小集合。

原子公式是一階公式
如果 $\phi$ 和 $\psi$ 是公式， $x$ 是一個變數，則以下也是公式

$(\phi \vee \psi )$
$(\phi \wedge \psi )$
$(\neg \phi )$
$(\phi \rightarrow \psi )$
$(\exists x\phi )$
$(\forall x\phi )$

語義

給定詞彙表上的一個一階結構包含以下內容：

一個域，它是一組元素（也稱為宇宙）
一個對映，它將詞彙表中的每個 $k$ 元關係符號與域上的 $k$ 元關係相關聯，並將每個 $k$ 元函式符號與域上的 $k$ 元函式相關聯。

這些元件賦予符號意義。

例子

關係集 = {

+

: 三元，

\times

: 三元，

\uparrow

: 三元，

=

: 二元，

<

: 二元 }

函式集 = {

next

: 一元，

0

: 常數 }

在這個詞彙表上的一個一階結構是

域：整數集
對映 : $+\rightarrow$ 加法， $\times \rightarrow$ 乘法， $\uparrow \rightarrow$ 冪運算， $<\rightarrow$ 排序， ${\mathit {next}}\rightarrow i+1$

在這個結構中，公式

\exists x\forall y\forall z[\times (y,z,x)\rightarrow ((y=1)\vee (z=1))]

表達了“存在質數”的命題（數字1也滿足該命題）。

這裡要注意 $\times (y,z,x)$ 等價於 $(x=y\times z)$ .

量詞的作用域

在公式 $(\forall x\phi )$ 或 $(\exists x\phi )$ 中， $\phi$ 被稱為變數 $x$ 的量化作用域。公式中變數的出現，如果在該變數的量化作用域內，則稱該出現是約束的，否則稱該出現是自由的。您可以將量詞的用法視為變數宣告。

句子是一個沒有自由變數的公式（即所有變數都是約束的）。句子要麼為真要麼為假。

包含自由變數的公式可以被認為是描述自由變數的屬性。例如， $\phi (x)$ 表示一個包含 $x$ 自由變數的公式，並描述了 $x$ 的屬性。

如果一個句子 $\phi$ 在結構 $I$ 上評估為真，我們說 $I$ 滿足 $\phi$ ，並將其記為 $I\models \phi$ 。

$I\models R(t_{1},t_{2},\ldots ,t_{k})$ 當且僅當 $(t_{1},t_{2},\ldots ,t_{k})\in I(R)$ ，其中 $I(R)$ 是 $R$ 在 $I$ 中的解釋。
$I\models \phi \wedge \psi$ 當且僅當 $I\models \phi$ 且 $I\models \psi$ 。（對於 $\vee$ 類似）。
$I\models \neg \varphi$ 當且僅當 $I\not \models \varphi$ 。
$I\models \exists x\phi (x)$ 如果 $I\models \phi (x\leftarrow c)$ 對於某些 $c$ 在域中。
$I\models \forall x\phi (x)$ 如果 $I\models \phi (x\leftarrow c)$ 對於每個 $c$ 在域中。

注意: $\phi (x\leftarrow c)$ 表示用 $c$ 替換 $x$ 在 $\phi$ 中的所有自由出現的結果。替換將在本章後面進一步討論。

公理化方法

公理是一組句子，旨在區分“期望”模型與其他模型。但通常，也存在“非期望”模型，稱為非標準模型。

例如: 考慮詞彙表 $({\mathit {next}},+,\times ,\uparrow ,0,=,<)$ ，其中符號具有通常的含義（由關於此詞彙表的 FO 句子定義）。這組公理的標準解釋（見本章末尾）是整數，但模 $p$ 的整數集也滿足這些公理。透過將以下句子新增到公理中，可以排除這種可能性: $\forall x(x<{\mathit {next}}(x))$

問題: 所有非標準模型都可以透過公理化排除嗎? 答案是否定的。考慮 [TODO: 匯入圖形] 中所示的模型，該模型的詞彙表僅包含 $0,<,\sigma$ （上行中的所有元素都大於下行中的元素）。

沒有一組一階句子可以區分此模型與自然數。直觀地，原因是，我們無法在一階句子中任意“回溯”（向 $0$ ）。對於上面的完整詞彙表，也可以獲得類似的非標準模型。

評估 FO 句子

給定一階結構 $I$ 和 FO 句子 $\phi$ ，我們能否判斷 $I\models \phi$ ？

對於有限結構，這個問題是可判定的。例如，假設 $E$ 是一個表示圖邊界的二元關係，而給定句子是

\exists x_{1}\exists x_{2}\exists x_{3}(E(x_{1},x_{2})\wedge E(x_{2},x_{3})\wedge E(x_{3},x_{1})\wedge x_{1}\neq x_{2}\wedge x_{2}\neq x_{3}\wedge x_{3}\neq x_{1})

.

我們可以透過嘗試 $x_{1},x_{2}$ 和 $x_{3}$ 的所有可能值來評估這個句子的真值。（樸素評估：“巢狀迴圈”。）這在域大小上是多項式時間，但在公式大小上是指數時間。

在無限域上，我們可能能夠評估句子的真值，也可能不能。在詞彙 $(N,0,\sigma ,<,+)$ 中，其中 $N$ 是自然數集，如果句子為真，則它是可判定的。（這被稱為普雷斯伯格算術。）但是，如果我們包含乘法，則句子的真值將變得不可判定。

FO 的演繹系統

FO 句子的集合 $\Delta$ 是

可滿足的，如果存在某個結構 $I$ 使得 $I\models \Delta$
不可滿足的，如果它不可滿足
有效的，如果對所有結構 $I$ ，都有 $I\models \Delta$

給定一組 FO 句子 $\Sigma$ 和一個句子 $\phi$

$\Sigma$ 蘊涵 $\phi$ （記為 $\Sigma \models \phi$ ），如果每個滿足 $\Sigma$ 的結構也滿足 $\phi$ 。
$\Sigma \models \phi$ 當且僅當 $\Sigma \cup \{\neg \phi \}$ 是不可滿足的。
如果 $\Sigma$ 是有限的，那麼， $\Sigma \models \phi$ 當且僅當 $\neg \Sigma \lor \phi$ 是有效的。
如果公式 $\phi$ 有自由變數 ${\vec {X}}=(x_{1},\ldots ,x_{k})$ ， $\phi$ 是有效的，當且僅當 $\forall {\vec {X}}\phi$ 是有效的。

有效性公理

有效性公理分為三類：

布林有效性公理。這些公理從命題邏輯中繼承而來。
等式公理。
量化公理。

布林有效性

給定一個一階邏輯公式 $\varphi$ ， $\varphi$ 的布林形式是一個命題公式 $\psi$ ，使得 $\varphi$ 是透過將 $\psi$ 中的每個命題變數替換為 $\varphi$ 的子公式得到的。

$\varphi$ 的布林形式集合用 $BF(\varphi )$ 表示。

例子

對於一階邏輯公式 $\forall xP(x)\lor \neg \forall xP(x)$ ，布林形式為 $p\lor \neg p$ 。
如果 $\varphi \equiv \forall xG(x,y)\land \exists xG(x,y)\land (G(z,x)\lor \forall xG(x,y))$ ，那麼 $BF(\varphi )\equiv x_{1}\land x_{3}\land (x_{2}\lor x_{1})$ ，其中 $x_{1}=\forall xG(x,y),x_{2}=G(z,x),x_{3}=\exists xG(x,y)$ 。

斷言: 如果 $\psi \in BF(\varphi )$ 並且 $\psi$ 是有效的，那麼 $\varphi$ 是有效的。

等式公理

令 $t,t_{1},\ldots ,t_{k},t'_{1},\ldots ,t'_{k}$ 是項。以下是一階邏輯的有效公式。

$t=t$
$(t_{1}=t'_{1}\land \cdots \land t_{k}=t'_{k})\rightarrow (f(t_{1},\ldots ,t_{k})=f(t'_{1},\ldots ,t'_{k}))$ , 其中 $f$ 是一個 $k$ 元函式。
$(t_{1}=t'_{1}\land \cdots \land t_{k}=t'_{k})\rightarrow (R(t_{1},\ldots ,t_{k})\rightarrow R(t'_{1},\ldots ,t'_{k}))$ , 其中 $R$ 是一個 $k$ 元關係。

替換

給定一個公式 $\varphi$ ，其中變數 $x$ 出現自由（表示為 $\varphi (x)$ ）和一個項 $t$ ，我們定義將 $t$ 代入 $x$ 的 $\varphi$ ，記為 $\varphi (x\leftarrow t)$ ，為將 $\varphi$ 中每個 $x$ 的自由出現用 $t$ 代替得到的結果公式，但必須滿足約束條件： $t$ 不包含任何在 $\varphi$ 中被量化的變數 $y$ ，使得 $x$ 出現在 $y$ 量化範圍內的自由位置。如果 $x$ 不在 $\varphi$ 中自由出現，那麼 $\varphi (x\leftarrow t)$ 被定義為 $\varphi$ 。

例如：設 $\varphi$ 為

((x=1)\rightarrow \exists x(x=y))

,

那麼

$\varphi (x\leftarrow (y+1))$ 是一個有效的替換
$\varphi (y\leftarrow (x+1))$ 不是一個有效的替換。

量化公理

$\forall x\varphi \rightarrow \varphi (x\leftarrow t)$ ，其中 $t$ 是一個項， $\varphi (x\leftarrow t)$ 是一個有效的替換
$(\forall x(\varphi \rightarrow \psi ))\rightarrow ((\forall x\varphi )\rightarrow (\forall x\psi ))$
$\varphi \rightarrow \forall x\varphi$
$\exists x\varphi \leftrightarrow \neg \forall x\neg \varphi$

總之，有效性的公理是 ${\mathbf {Ax} }$

布林有效性公理。這些公理從命題邏輯中繼承而來。
等式公理。
量化公理。

定義：一個證明是一個序列 $\phi _{1},\phi _{2},\ldots ,\phi _{k}$ 的 FO 語句，使得對於每個 $i\in \{1,\ldots ,k\}$ 或者 $\phi _{i}\in {\mathbf {Ax} }$ 或者 $\exists j,k<i$ 使得 $\phi _{j}\equiv \psi$ 以及 $\phi _{k}\equiv (\psi \rightarrow \phi _{i})$ .

符號: 如果存在使用 ${\mathbf {Ax} }$ 的 $\phi$ 的證明，我們用 $\vdash _{\mathbf {Ax} }\phi$ 來表示這個事實。

事實 (可靠性): 如果 $\vdash _{\mathbf {Ax} }\phi$ ，那麼 $\phi$ 是有效的。

備註: 可以證明有效的公式集是遞迴可列舉的。

示例: 公式 $\forall x(\phi \land \psi )\rightarrow (\forall x\phi \land \forall x\psi )$ 的證明

\forall x(\phi \land \psi )

\forall x(\phi \land \psi )\rightarrow (\phi \land \psi )(x\leftarrow x)

\phi \land \psi

\phi

\forall x(\phi \land \psi )\rightarrow \phi

\forall x(\forall x(\phi \land \psi )\rightarrow \phi )

\forall x\forall x(\phi \land \psi )\rightarrow \forall x\phi

\forall x(\phi \land \psi )\rightarrow \forall x\phi

\forall x\phi

$\forall x\psi$ 的證明是對稱的。

\forall x\phi \land \forall x\psi

\forall x(\phi \land \psi )\rightarrow (\forall x\phi \land \forall x\psi )

有用的等價關係

$\forall x(\phi \land \psi )\leftrightarrow (\forall x\phi )\land (\forall x\psi )$
$\forall x(\phi \lor \psi )\not \leftrightarrow (\forall x\phi )\lor (\forall x\psi )$ 例如 $\phi (x)\approx$ "x 是偶數" 以及 $\psi (x)\approx$ "x 是奇數"
$\forall x(\phi (x)\lor \neg \phi (x))\not \leftrightarrow (\forall x\phi (x)\lor \forall x\neg \phi (x))$
$\exists x(\phi \lor \psi )\leftrightarrow (\exists x\phi )\lor (\exists x\psi )$
$\neg \exists x\phi \leftrightarrow \forall x\neg \phi$
$\neg \forall x\phi \leftrightarrow \exists x\neg \phi$

前束正規化

斷言：每個 FO 語句都等價於一個形如 $Q_{1}x_{1}\cdots Q_{k}x_{k}\phi$ 的 FO 語句，其中 $Q_{i}\in \{\exists ,\forall \}$ 且 $\phi$ 是無量詞的。

這是透過使用量詞的分配律證明的。可能需要重新命名變數，以避免歧義。雖然你總是可以將所有量詞移動到左側，但所得公式的大小實際上可能比原始公式大很多倍。

例子:

\phi \equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y)))\land G(x,0)

\equiv (\forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y))))\land G(w,0)

\equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y))\land G(w,0))

\equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x(G(x,x)\land \forall y(G(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x\forall y(G(x,x)\land (G(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x\forall y(G(x,x)\land \exists z(G(x,y)\lor \neg G(z,z))\land G(w,0))

\equiv \forall x\forall y\exists z(G(x,x)\land (G(x,y)\lor \neg G(z,z))\land G(w,0))

回顧公理方法

使用一個（可能是無限的，但遞迴的）公理集 $\Delta$ （一階句子）儘可能詳細地描述所需模型。

使用演繹證明事物。

符號: 我們說 $\phi$ 是 $\Delta$ 的有效推論（記為 $\Delta \models \phi$ ），如果每個滿足 $\Delta$ 的模型也滿足 $\phi$ 。

事實: $\Sigma \models \phi$ 當且僅當 $\Sigma \cup \{\neg \phi \}$ 不可滿足。

旁註: 數論的非邏輯公理

以下十四個一階公理描述了算術和數字的性質，即加法 ( $+$ )，乘法 ( $\times$ )，冪運算 ( $\uparrow$ ，相等 ( $=$ )，排序 ( $<$ )，後繼函式 ( $\sigma$ ) 和餘數 (mod)。這個例子展示了一階語句的表達能力，最初人們希望它能為“唯一真正的數學”提供基礎。