定义 4.7 的详解
这个定义描述了一阶语言 $L$ 在一个解释 $I$ 下是如何具体化的，也就是说，如何给出语言中符号的含义。我们先简单介绍一些背景知识，然后详细解释定义的每一部分。
一阶语言（First-Order Language）
一阶语言是一种形式化语言，用来描述和推理关于对象及其关系。它由以下几部分组成：
- 常项符号：表示某些特定的对象。
- 函数符号：表示从对象到对象的映射（即函数）。
- 谓词符号：表示对象之间的关系（例如“等于”、“大于”）。
- 变项符号：表示对象中的某个未知值（类似于变量）。
解释（Interpretation）
在形式逻辑中，解释 $I$ 是赋予一阶语言中的符号具体含义的规则。通过解释，我们可以将抽象的符号系统与真实的对象或概念联系起来。解释告诉我们常项符号代表什么，函数符号如何作用，以及谓词符号表示哪些关系。
现在我们来看定义 4.7 的每个部分。
1. 非空个体域 $D_I$
(a) 非空个体域 $D_I$
个体域是解释 $I$ 中所有可能的个体或对象的集合。这个集合不能是空的，必须至少包含一个对象。所有语言符号（常项符号、函数符号、谓词符号等）都在这个域上进行解释。
- 个体域 $D_I$：是解释中所有可能对象的集合。
- 非空性：确保我们讨论的语言总是关于某些实际的对象。
- 例子：如果我们讨论的是自然数，那么个体域 $D_I$ 可以是自然数的集合 $\lbrace 0, 1, 2, 3, \dots \rbrace$。
2. 常项符号的解释
(b) 对每一个个体常项符号 $a \in L$，有一个 $d_a \in D_I$，称 $d_a$ 为 $a$ 在 $I$ 中的解释。
常项符号是语言中表示特定个体的符号。例如，如果 $a$ 是一个常项符号，解释 $I$ 将为 $a$ 赋予个体域 $D_I$ 中的某个具体对象。
- 解释规则：解释将常项符号与个体域中的某个特定元素 $d_a \in D_I$ 关联起来。
- 例子：如果 $a$ 是常项符号，代表数字 $0$，而个体域是自然数，那么 $d_a$ 就是 $0$ 这个数。
3. 函数符号的解释
(c) 对每一个 $n$ 元函数符号 $f \in L$，有一个定义在 $D_I$ 上的 $n$ 元函数 $f_I: D_I^n \to D_I$，称 $f_I$ 为 $f$ 在 $I$ 中的解释。
函数符号表示将 $n$ 个对象映射到另一个对象的函数。解释 $I$ 为每个函数符号指定一个具体的函数，作用于个体域 $D_I$ 中的对象。
- 函数符号 $f$：表示 $n$ 元函数，即从 $D_I$ 中取 $n$ 个对象，然后映射到 $D_I$ 中的另一个对象。
- 解释规则：每个函数符号 $f$ 都有一个具体的函数 $f_I$，这个函数是从 $D_I^n$ 到 $D_I$ 的映射。
- 例子：如果 $f$ 是加法符号 $+$，而个体域是自然数，那么 $f_I$ 就是通常的自然数加法函数，即 $f_I(2, 3) = 5$。
4. 谓词符号的解释
(d) 对每一个 $n$ 元谓词符号 $F \in L$，有一个定义在 $D_I$ 上的 $n$ 元谓词 $F_I \subseteq D_I^n$，称 $F_I$ 为 $F$ 在 $I$ 中的解释。
谓词符号表示对象之间的关系。解释 $I$ 为每个谓词符号指定一个具体的谓词（即关系），它是从个体域 $D_I$ 中的对象到布尔值（真或假）的映射。换句话说，谓词符号表示哪些对象之间的关系成立。
- 谓词符号 $F$：表示 $n$ 元关系，即在 $D_I$ 中取 $n$ 个对象，判断它们之间的关系是否成立。
- 解释规则：每个谓词符号 $F$ 都有一个具体的谓词 $F_I$，这是 $D_I$ 上的一个 $n$ 元关系。
- 例子：如果 $F$ 是谓词符号 $=$ （表示相等关系），而个体域是自然数，那么 $F_I$ 表示通常的自然数相等关系，即 $F_I(3, 3) = \text{True}$，而 $F_I(2, 3) = \text{False}$。
5. 赋值 $\sigma$
解释 $I$ 中还有一个赋值函数 $\sigma$，用于处理个体变项符号（变量）。每个变量 $x$ 都被解释为个体域中的某个具体对象 $\sigma(x)$。
- 赋值 $\sigma$：为每个变量符号 $x$ 分配个体域 $D_I$ 中的一个具体对象。
- 作用：通过赋值，可以对一阶语言中的量词公式进行具体解释，例如“对于所有 $x$”和“存在 $x$”这样的表达式。
- 例子：如果 $x$ 是一个变量，而个体域 $D_I$ 是自然数集，那么赋值 $\sigma(x)$ 可以是 $2$，表示当前 $x$ 的值是 $2$。
总结
定义 4.7 描述了一阶语言在解释 $I$ 下的具体含义。解释为语言中的常项符号、函数符号和谓词符号赋予了个体域中的具体含义，同时通过赋值 $\sigma$ 解释了变量的具体取值。这种解释方法将形式语言与实际对象、函数和关系联系起来，使得我们可以用形式语言来描述和推理实际问题。