写在前面

命题逻辑（或者 零阶逻辑）到一阶逻辑的变化，在于描述的粒度。命题逻辑只能描述命题之间的关系，以及它们如何构成更大的结构（新的命题）。在一阶逻辑中我们可以深入原子命题的内部，讨论命题的构成——比如说含有运算和函数的等式、不等式。

为了做到这一点，需要引入集合上的n元关系。从集合论作为基础的角度看，这么做是比较和谐的。

命题逻辑

n元关系

定义集合 \(D\) 上的n元关系为n元函数 \(f\colon D^n\mapsto \left\{T,F\right\}\)，取 \(P=\left\{x\mid x\in D,f(x)=T\right\}\)，那么就可以仅用集合来表示n元关系。

特别的，\(<\) 是一个二元关系。它同时是 \(\mathbb R,\mathbb N,\mathbb Z\) 上的二元关系，因此可以看出n元关系的定义还要看其定义域，此处即论域

语法

记 \(\scr P,A,V\) 分别为 谓词、常量、变量 符号的可数集，规定每个谓词都有arity（有多少参数）n

规定量词 \(\forall,\exists\) 分别读作 任意 和 存在

原子公式

形如 \(p(t_1,t_2\ldots t_n)\) 的公式，其中 \(p\) 是n元谓词，\(t_i\) 要么是变量，要么是常量

公式

给出BNF

\[\begin{aligned} formula &:= atomic\_formula\;|\; \neg formula\;|\;formula\vee formula\;|\;formula\wedge formula \\ formula &:= \exists x\,formula\;|\;\forall x\,formula \end{aligned} \]

一阶逻辑是对命题逻辑的简单拓展，仍然保持了树状结构，之前的证明套路仍然适用。

在一阶逻辑中既然有变量就同样有作用域的问题。具体的定义类似\(\lambda\)-演算：

1. 公式 \(\forall x\, F\)，\(\exists x\, F\) 中，\(x\) 的作用域为公式 \(F\)，\(F\) 不要求有 \(x\) 出现
2. 称变量 \(x\) 是公式 \(F\) 中的自由变量，当且仅当 \(x\) 在 \(F\) 中出现，且不在限定 \(x\) 的任何作用域中。
3. 非自由变量就称其为约束变量。
4. 若公式 \(F\) 中，任意变量都是约束变量，则称 \(F\) 为封闭公式（Closed Formula）

语义

命题逻辑的语义由解释给出，在一阶逻辑则不够

回忆命题逻辑中解释的定义：\(\scr I\) 是函数 \(U_A\mapsto \left\{T,F\right\}\)，其中 \(U_A\) 表示公式 \(A\) 中全部原子命题构成的集合

为了实现类似的效果，我们需要

1. 给常量赋予含义
2. 给变量赋予含义
3. 给谓词赋予含义

解释

规定公式 \(A\) 的解释是一个三元组 \((D,\left\{R_1\ldots R_m\right\},\left\{d_1\ldots d_k\right\})\)

其中 \(D\) 是论域，\(R_i\) 是论域 \(D\) 上的关系，\(d_j\) 是 \(D\) 中的元素，其赋予了 \(A\) 中常量含义。

一个例子是 \(\bold 1<\bold 2\) 和 \(壹<贰\)，此处的 \(\left\{壹，贰\right\}\) 都是常量，在规定解释为 \((\mathbb N,\left\{<\right\},\left\{1,2\right\})\) 时才能说等式成立（讨论其真值）。可能存在这么一个神奇的国度，它们把 \(1\) 写作 \(\bold 2\)，把 \(2\) 写作 \(\bold 1\)，那么式1在它们的国度（特定解释下）就不成立了。

但这是不够的。考虑公式 \(x，其在任意解释下都不能讨论真值，因为自由变量 \(x\) 的值无法确定，由此引入赋值的定义。

赋值

记 \({\scr I}_A\) 是公式 \(A\) 的解释，\(A\) 的赋值 \(\sigma_{{\scr I}_A}\) 是函数 \({\scr V}\mapsto D\)，其赋予了 \(A\) 中所有自由变量唯一的论域中的元素作为值。

可以通过类似于 \(\sigma_{{\scr I}_A}\left\{x\rightsquigarrow v\right\}\) 来对映射进行单点修改，非常熟悉的味道

有了解释和赋值就可以对公式的真值进行讨论了，只需要沿着树形结构递归构造就好了。

吃饭，咕咕咕咕