形式逻辑/谓词逻辑/满足

← 模型

↑ 谓词逻辑

真值 →

满足

为 ${\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} )\ .\,\!$