第三章：一阶逻辑¶

定义：项(term)

递归定义如下：

• 变元和常元是项
• 对每一个 \(n\) 元函数 \(f\), 如果 \(t_1, \cdots, t_n\) 都是项，则 \(f(t_1, \cdots, t_n)\) 也是项。

定义：原子公式(atomic formula)

递归定义如下：

• \(\top\) 和 \(\bot\) 是原子公式
• 对每一个 \(n\) 元谓词 \(p\)，如果 \(t_1, \cdots, t_n\) 都是项，则 \(p(t_1, \cdots, t_n)\) 是原子公式

定义：一阶逻辑的解释（interpretation）

解释 \(\mathcal M=(\mathcal D,\mathcal I)\) 中，论域 \(\mathcal D\) 是希望讨论的元素，解释函数 \(\mathcal I\) 满足下列要求：

• 规定常元 \(c\) \(\mapsto\) \(d \in \mathcal D\) (\(\forall c \in \mathcal C\))
• 规定 \(n\) 元函数符号 \(f\) 为 \(f_{\mathcal I}: \mathcal D^n \mapsto \mathcal D\)
• 规定 \(n\) 元谓词符号 \(p\) 为 \(p_{\mathcal I} \subseteq \mathcal D^n\)

定义：赋值(assignment)

公式 \(\varphi\) 的自由变元集合 \(FVar(\varphi)\) ，赋值是 \(\rho:FVar(\varphi) \to \mathcal D\)【给自由变元赋值】

定义：取值

项 \(t\), 解释 \(\mathcal M\), 赋值 \(\rho\)，定义取值 \(\llbracket t \rrbracket_{\mathcal M, \rho}\):

1. 常元 \(\llbracket c \rrbracket_{\mathcal M, \rho} = \mathcal I(c)\)
2. 变元 \(\llbracket v \rrbracket_{\mathcal M, \rho} = \rho(v)\)
3. 函数项 \(\llbracket f(t_1, \dots, t_n) \rrbracket_{\mathcal M, \rho} = \mathcal I(f)(\llbracket t_1 \rrbracket_{\mathcal M, \rho}, \dots, \llbracket t_n \rrbracket_{\mathcal M, \rho})\)

定义: 语义蕴含

\(\forall (M, \rho). \llbracket \varphi \rrbracket_{\mathcal M, \rho} \to \llbracket \psi \rrbracket_{\mathcal M, \rho}\)

以上记作 \(\varphi \Rightarrow \psi\)