形式邏輯/謂詞邏輯/滿足

← 模型

↑ 謂詞邏輯

真值 →

滿足

為 ${\mathcal {L_{P}}}\,\!$ 的句子分配真值的規則應該說，實際上，

$\forall \alpha \,\varphi \,\!$

當且僅當 $\varphi \,\!$ 對域中的每個物件都為真。 這裡有兩個問題。 首先，$\varphi \,\!$ 通常可能具有自由變數。 特別是，$\alpha \,\!$ 通常將是自由的（否則說“對所有 $\alpha \,\!$ …” 是無關緊要的）。 但是具有自由變數的公式不是句子，也沒有真值。 其次，我們還沒有一種精確的方法來說明 $\varphi \,\!$ 對域中的每個物件都為真。 這些問題的解決方案分為兩部分

• 將域中的物件分配給每個變數，

• 指定模型是否滿足具有特定變數賦值的公式。

然後我們可以根據滿足度來定義模型中的真值。

變數賦值

給定模型 ${\mathfrak {M}}\,\!$，一個變數賦值，記為 $\mathrm {s} \,\!$，是一個函式，將域 $|{\mathfrak {M}}|\,\!$ 的一個成員分配給 ${\mathcal {L_{P}}}\,\!$ 中的每個變數。例如，如果 $|{\mathfrak {M}}|\,\!$ 包含自然數，則 $\mathrm {s} \,\!$ 應用於變數 $x$ 的結果可以是 $\mathrm {s} (x)=7$。

除了變數賦值，我們還有模型的解釋函式 $I_{\mathfrak {M}}\,\!$ 將域成員分配給常數符號。我們將這些資訊結合起來，為任意項（包括常數符號、變數和由運算子字母作用於其他項形成的複雜項）生成域成員的賦值。這是透過一個擴充套件變數賦值來完成的，記為 ${\overline {\mathrm {s} }}\,\!$，其定義如下。回顧一下，解釋函式 $I_{\mathfrak {M}}\,\!$ 將語義值分配給 ${\mathcal {L_{P}}}\,\!$ 的運算子字母和謂詞字母。

擴充套件變數賦值 ${\overline {\mathrm {s} }}\,\!$ 是一個函式，它從 $|{\mathfrak {M}}|\,\!$ 中分配值，如下所示。

如果 $\alpha \,\!$ 是一個變數，那麼

${\overline {\mathrm {s} }}(\alpha )\ =\ \mathrm {s} (\alpha )\,\!$

如果 $\alpha \,\!$ 是一個常數符號（即 0 階運算子字母），那麼

${\overline {\mathrm {s} }}(\alpha )\ =\ I_{\mathfrak {M}}(\alpha )\,\!$

如果 $\zeta \,\!$ 是一個 *n*-元運算子 ( *n* 大於 0) 並且 $\alpha _{1},\ \alpha _{2},\ \ldots ,\ \alpha _{n}\,\!$ 是 **項**，那麼

${\overline {\mathrm {s} }}{\big (}\,\zeta (\alpha _{1},\,\alpha _{2},\,\ldots ,\,\alpha _{n})\,{\big )}\ =\ I_{\mathfrak {M}}(\zeta )\,{\big (}\ {\overline {\mathrm {s} }}(\,\alpha _{1}),\,{\overline {\mathrm {s} }}(\alpha _{2}),\,\ldots ,\,{\overline {\mathrm {s} }}(\alpha _{n})\,{\big )}\,\!$

一些例子可能會有所幫助。假設我們有模型 $I_{\mathfrak {M}}\,\!$ 其中

$|{\mathfrak {M}}|\ =\ \{1,\,2,\,3\}\ .\,\!$

$I_{\mathfrak {M}}(a_{0}^{0})\ =\ 0\ .\,\!$

$I_{\mathfrak {M}}(b_{0}^{0})\ =\ 1\ .\,\!$

$I_{\mathfrak {M}}(f_{0}^{2})\ =\ {\mathfrak {f}}_{0}^{2}\ {\mbox{such that:}}\quad {\mathfrak {f}}_{0}^{2}(0,\,0)=2,\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1,\ {\mathfrak {f}}_{0}^{2}(0,\,2)=0,\,\!$

${\mathfrak {f}}_{0}^{2}(1,\,0)=1,\ {\mathfrak {f}}_{0}^{2}(1,\,1)\ =\ 0,\ {\mathfrak {f}}_{0}^{2}(1,\,2)=2,\ {\mathfrak {f}}_{0}^{2}(2,\,0)=0,\,\!$

${\mathfrak {f}}_{0}^{2}(2,\,1)=2,\ {\mbox{and}}\ {\mathfrak {f}}_{0}^{2}(2,\,2)=1\ .\,\!$

在前一頁中，我們注意到我們想要以下結果

$f(a,b)\ {\mbox{resolves to}}\ 1\ \mathrm {in} \ {\mathfrak {M}}\ .\,\!$

我們現在已經實現了這一點，因為我們對定義在$I_{\mathfrak {M}}\,\!$上的任何$\mathrm {s} \,\!$都

${\overline {\mathrm {s} }}(f(a,b))\ =\ I_{\mathfrak {M}}(f)\,(\ {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\ )\ =\ {\mathfrak {f}}_{0}^{2}(\ {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\ )\,\!$

$=\ {\mathfrak {f}}_{0}^{2}(\ I_{\mathfrak {M}}(a),\,I_{\mathfrak {M}}(b)\ )\ =\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1\ .\,\!$

假設我們也擁有一個變數分配 $\mathrm {s} \,\!$，其中

$\mathrm {s} (x_{0})\ =\ 0\ .\,\!$

$\mathrm {s} (y_{0})\ =\ 1\ .\,\!$

然後我們得到

${\overline {\mathrm {s} }}(f(x,y))\ =\ I_{\mathfrak {M}}(f)\,(\ {\overline {\mathrm {s} }}(x),\,{\overline {\mathrm {s} }}(y)\ )\ =\ {\mathfrak {f}}_{0}^{2}(\ {\overline {\mathrm {s} }}(x),\,{\overline {\mathrm {s} }}(y)\ )\,\!$

$=\ {\mathfrak {f}}_{0}^{2}(f)\,(\ \mathrm {s} (x),\,\mathrm {s} (y)\ )\ =\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1\ .\,\!$

滿足

一個模型，連同變數分配，可以滿足（或不滿足）一個公式。然後我們將使用變數分配的滿足概念來定義模型中句子的真值。我們可以使用以下方便的符號來說明解釋 ${\mathfrak {M}}\,\!$ 滿足（或不滿足） $\varphi \,\!$ 使用 $\mathrm {s} \,\!$.

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \varphi \,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \not \vDash \,\varphi \,\!$

我們現在定義 *模型在變數賦值下對公式的滿足*。在下文中，'iff' 代表'當且僅當'。

${\mbox{i.}}\quad {\mbox{For}}\ \sigma \ {\mbox{a sentence letter:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \sigma \quad {\mbox{iff}}\quad I_{\mathfrak {M}}(\sigma )\ =\ \mathrm {True} \ .\,\!$

${\mbox{ii.}}\quad {\mbox{For}}\ \pi \ {\mbox{an}}\ n{\mbox{--place predicate letter and for}}\ \alpha _{0},\,\alpha _{1},\,\ldots ,\,\alpha _{n}\ {\mbox{any terms:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \pi (\alpha _{0},\,\alpha _{1},\,\ldots ,\,\alpha _{n})\quad {\mbox{iff}}\ \langle {\overline {\mathrm {s} }}(\alpha _{0}),\,{\overline {\mathrm {s} }}(\alpha _{1}),\,\ldots ,\,{\overline {\mathrm {s} }}(\alpha _{n})\rangle \ \in \ I_{\mathfrak {M}}(\pi )\ .\,\!$

${\mbox{iii.}}\quad {\mbox{For}}\ \varphi \ {\mbox{a formula:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \lnot \varphi \quad {\mbox{iff}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \not \vDash \varphi \ .\,\!$

${\mbox{iv.}}\quad {\mbox{For}}\ \varphi \ {\mbox{and}}\ \psi \ {\mbox{formulae:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\varphi \land \psi )\quad {\mbox{iff}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \varphi \ \ {\mbox{and}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \psi \ .\,\!$

${\mbox{v.}}\quad {\mbox{For}}\ \varphi \ {\mbox{and}}\ \psi \ {\mbox{formulae:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\varphi \lor \psi )\quad {\mbox{iff}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \varphi \ \ {\mbox{or}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \psi \ {\mbox{(or both)}}\ .\,\!$

${\mbox{vi.}}\quad {\mbox{For}}\ \varphi \ {\mbox{and}}\ \psi \ {\mbox{formulae:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\varphi \rightarrow \psi )\quad {\mbox{iff}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \not \vDash \varphi \ \ {\mbox{or}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \psi \ {\mbox{(or both)}}\ .\,\!$

${\mbox{vii.}}\quad {\mbox{For}}\ \varphi \ {\mbox{and}}\ \psi \ {\mbox{formulae:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\varphi \leftrightarrow \psi )\quad {\mbox{iff}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\varphi \land \psi )\ \ {\mbox{or}}\ \langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash (\lnot \varphi \land \lnot \psi )\ {\mbox{(or both)}}\ .\,\!$

${\mbox{viii.}}\quad {\mbox{For}}\ \varphi \ {\mbox{a formula and}}\ \alpha \ {\mbox{a variable:}}\,\!$$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \forall \alpha \,\varphi \quad {\mbox{iff}}\ \ {\mbox{for every}}\ \mathrm {d} \ \in |{\mathfrak {M}}|,\ \langle {\mathfrak {M}},\ \mathrm {s[\alpha \!:\,d]} \rangle \ \vDash \varphi \ .\,\!$

${\mbox{where}}\ \mathrm {s[\alpha \!:\,d]} \ {\mbox{differs from}}\ \mathrm {s} \ {\mbox{only in assigning}}\ \mathrm {d} \ {\mbox{to}}\ \alpha \ .\,\!$.

${\mbox{ix.}}\quad {\mbox{For}}\ \varphi \ {\mbox{a formula and}}\ \alpha \ {\mbox{a variable:}}\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \exists \alpha \,\varphi \quad {\mbox{iff}}\ \ {\mbox{for at least one}}\ \mathrm {d} \in |{\mathfrak {M}}|,\ \langle {\mathfrak {M}},\ \mathrm {s[\alpha \!:\,d]} \rangle \ \vDash \varphi \ .\,\!$

${\mbox{where}}\ \mathrm {s[\alpha \!:\,d]} \ {\mbox{differs from}}\ \mathrm {s} \ {\mbox{only in assigning}}\ \mathrm {d} \ {\mbox{to}}\ \alpha \ .\,\!$.

示例

以下繼續使用在描述擴充套件變數分配時使用的示例。它們基於上一頁的示例。

用於示例的模型和變數分配

假設我們有模型$I_{\mathfrak {M}}\,\!$ 其中

$|{\mathfrak {M}}|\ =\ \{0,\,1,\,2\}\ .\,\!$

$I_{\mathfrak {M}}(a_{0}^{0})\ =\ 0\ .\,\!$

$I_{\mathfrak {M}}(b_{0}^{0})\ =\ 1\ .\,\!$

$I_{\mathfrak {M}}(c_{0}^{0})\ =\ 2\ .\,\!$

$I_{\mathfrak {M}}(f_{0}^{2})\ =\ {\mathfrak {f}}_{0}^{2}\ {\mbox{such that:}}\quad {\mathfrak {f}}_{0}^{2}(0,\,0)=2,\ {\mathfrak {f}}_{0}^{2}(0,\,1)\ =\ 1,\ {\mathfrak {f}}_{0}^{2}(0,\,2)=0,\,\!$

${\mathfrak {f}}_{0}^{2}(1,\,0)=1,\ {\mathfrak {f}}_{0}^{2}(1,\,1)\ =\ 0,\ {\mathfrak {f}}_{0}^{2}(1,\,2)=2,\ {\mathfrak {f}}_{0}^{2}(2,\,0)=0,\,\!$

${\mathfrak {f}}_{0}^{2}(2,\,1)=2,\ {\mbox{and}}\ {\mathfrak {f}}_{0}^{2}(2,\,2)=1\ .\,\!$

$I_{\mathfrak {M}}(\mathrm {F_{0}^{2}} )\ =\ \{\langle 0,\ 1\rangle ,\ \langle 1,\ 2\rangle ,\ \langle 2,\ 1\rangle \}\ .\,\!$

假設我們有一個變數賦值$\mathrm {s} \,\!$ 其中

$\mathrm {s} (x_{0})\ =\ 0\ .\,\!$

$\mathrm {s} (y_{0})\ =\ 1\ .\,\!$

$\mathrm {s} (z_{0})\ =\ 2\ .\,\!$

我們已經看到，以下兩種情況都解析為 1

$f(a,b)\,\!$

$f(x,y)\,\!$

無量詞示例

給定模型${\mathfrak {M}}\,\!$，上一頁 提到了以下進一步的目標

$(1)\quad \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ {\mbox{are True in}}\ {\mathfrak {M}}\ .\,\!$

$(2)\quad \mathrm {F} (a,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!$

$(3)\quad \mathrm {F} (a,f(a,b))\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!$

$(4)\quad \mathrm {F} (f(a,b),a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!$

$(5)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (a,b)\ {\mbox{is True in}}\ {\mathfrak {M}}\ .\,\!$

$(6)\quad \mathrm {F} (c,b)\rightarrow \mathrm {F} (b,a)\ {\mbox{is False in}}\ {\mathfrak {M}}\ .\,\!$

我們還沒有準備好評估真假，但我們可以透過觀察這些句子是否滿足於 ${\mathfrak {M}}\,\!$ 來朝著這個方向邁出一步，其中 $\mathrm {s} .\,\!$ 是一個變數賦值。事實上，$\mathrm {s} \,\!$ 的具體細節不會影響到我們確定哪些句子是滿足的。因此，${\mathfrak {M}}\,\!$ 對於任何變數賦值，都會滿足（或不滿足）它們。正如我們將在下一頁看到的，這是在 ${\mathfrak {M}}\,\!$ 中判斷真（或假）的標準。

對應於（1），

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \mathrm {F} (a,b),\ \mathrm {F} (b,c),\ {\mbox{and}}\ \mathrm {F} (c,b)\ .\,\!$

特別地

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \mathrm {F} (a,b)\ \ {\mbox{because}}\ \langle {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(b)\rangle \ =\ \langle 0,\,1\rangle \ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \mathrm {F} (b,c)\ \ {\mbox{because}}\ \langle {\overline {\mathrm {s} }}(b),\,{\overline {\mathrm {s} }}(c)\rangle \ =\ \langle 1,\,2\rangle \ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \vDash \mathrm {F} (c,b)\ \ {\mbox{because}}\ \langle {\overline {\mathrm {s} }}(c),\,{\overline {\mathrm {s} }}(b)\rangle \ =\ \langle 2,\,1\rangle \ \in \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!$

分別對應 (2) 到 (6)

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \not \vDash \mathrm {F} (a,a))\ \ {\mbox{because}}\ \langle {\overline {\mathrm {s} }}(a),\,{\overline {\mathrm {s} }}(a)\rangle \ =\ \langle 0,\,0\rangle \ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!$

$\langle {\mathfrak {M}},\ \mathrm {s} \rangle \ \not \vDash \mathrm {F} (f(a,b),a)\ \ {\mbox{because}}\ \langle {\overline {\mathrm {s} }}(f(a,b),\,{\overline {\mathrm {s} }}(a)\rangle \ =\ \langle 1,\,0\rangle \ \notin \ I_{\mathfrak {M}}(\mathrm {F} )\ .\,\!$