一阶逻辑的语法与语义

一个数学定理是由公理出发经过正确的逻辑推导得出的一个结论。我们希望这整个过程是尽可能精确而严格的，因此这整个过程最好是能够被形式化(formalize)的。为此我们要定义一套形式语言来描述公理、证明与定理。

一阶逻辑的语法

我们将会建立的这套形式语言称为一阶语言(first-order language)或一阶逻辑(first-order logic)。对于一个集合，我们把集合的元素(elements)称为一阶对象(first-order objects)，它们是构成集合的最基本要素。一阶对象的集合也即集合子集称为二阶对象(second-order objects)，相应地二阶对象的集合构成三阶对象，等等。一阶语言规定我们在存在量词中只能提到一阶对象，例如我们可以说“对于集合$A$中的每个元素，……”，但不能直接说“对于集合$A$的每个子集，……”。这意味着一阶逻辑能够直接表达的数学定理是有限的，有许多涉及高阶两次的数学定理是不能直接翻译为一阶逻辑的。然而，通过一些基于集合论的转化，我们原则上可以用一阶逻辑表达当今世界上的所有数学定理，也就是说本质上对一阶逻辑的讨论就是对所有数学定理的讨论，我们之后会看到如何做到这一点。

一阶逻辑的字母表

在形式语言中，一切讨论的对象都要用符号串(word)，符号串就是由字符集(alphabet)中的字符连接而成的字符串。首先定义一阶逻辑的alphabet。一阶逻辑的alphabet包括以下内容：变量（一般记为$v_0,v_1,\cdots$，一阶逻辑能够使用的变量必须是可数的）；逻辑符号——否定（$\neg$），与（$\and$），或（$\or$），推出（$\to$），等价（$\leftrightarrow$）；存在量词（$\forall,\exists$）；等号（$\equiv$）；逗号（,）；$n$元关系符号（可以为空）；$n$元函数符号（可以为空）；常数符号（可以为空）。最后三者比较特殊，我们把他们统称为符号集，记为$S$。所有一阶逻辑的形式系统的alphabet只有$S$集是不同的，其它都是相同的。注意以上所有符号都是未被赋予任何含义的，等号的含义可能与我们经验中的等号的含义完全相反或完全不同。我们完全可以把等号换成苹果，否定换成香蕉，因为我们只是完全形式化地写出了这一些符号罢了。

将一阶逻辑的字符连接成字符串是要遵循一定规则的，这些规则就称为一阶逻辑的语法。对于固定的$S$，我们定义一阶逻辑的term：term只有三种，单个变量$v_i$，单个常数$v_i$，以及归纳地以term作为自变量的$n$元函数$f(t_1,t_2,\cdots,t_n)$。我们定义一阶逻辑的formula：用等号连接地两个term（$t_1\equiv t_2$）；以term作为自变量的$n$元关系$R(t_1,\cdots,t_n)$；归纳地，如果$\varphi$是formula，$\neg \varphi$、$\forall \varphi$、$\exists \varphi$也是formula；归纳地，如果$\varphi,\psi$是formula，$\varphi \land \psi$、$\varphi\or\psi$、$\varphi\to \psi$、$\varphi \leftrightarrow \psi$也是formula。我们依然要注意到term和formula也是没有任何意义的，它们只是按照我们定义的语法连接而成的字符串。

为了今后讨论的方便，还要引入一些概念来方便称呼。 在一个formula中，不出现在存在量词中的那些变量称为自由变元（free variable），它类似于程序中的全局变量。例如$\forall v_1 \neg v_1\equiv v_2$中的$v_2$是自由变元而$v_1$不是（因为按照我们的理解$v_1$的取值其实是被预先fix的，也即它不是自由的）如果一个formula中不存在任何自由变元，就把这个formula称为一个sentence。（可以设想只有sentence这样的formula才刻画某种真正的具有一般性的数学性质。 ）

一阶逻辑的语义

根据我们定义的一阶逻辑的语法，我们能写出许多term，term可以组成formula。现在我们要赋予term和formula以“意义”，这意味着我们要对一阶逻辑的所有符号和符号的组合给出“解释”。

意义取决于我们讨论的背景。当我们讨论自然数上的数学命题时，变量自然只能取自然数；如果我们讨论实数上的数学命题时，变量允许取全体实数。因此关于意义的第一个要素就是universe（论域），记为$\mathcal{A}$。确定了universe以后，$n$元关系就是$\mathcal{A}^n$的子集，函数就是$\mathcal{A}^n\to\mathcal{A}$的映射，常量符号是固定的$\mathcal{A}$中的元素。后三者可以看作从关系符号、函数符号到对应的universe上的映射$\mathfrak{a}$，这样我们就对变量和符号集S做出了解释。这个解释可以看作二元组$\mathfrak{A}=(A,\mathfrak{a})$，称为S上的一个structure（结构）。Structure没有对变量和函数关系给出具体的解释，但限制了我们讨论变量和函数关系的范围。

现在我们要更具体地对term和formula做出解释，就需要给每个变量赋值。当我们暂时不考虑有存在量词的情况时（所有变量都是free的），可以简单地理解为每个变量有一个特定的取值。于是我们定义函数$\beta:v_i \to \mathcal{A}$，这样就给每个变量赋予了一个解释，这称为assignment。把structure和assignment结合起来称为interpretation，记为$\mathfrak{I}=(\mathfrak{A},\beta)$。（注意到我们还没对一阶逻辑的其他符号给出意义，这些解释被包括在interpretation对term和formula的解释当中）。

下面定义对term的interpretation。对于单个变量，规定$\mathfrak{I}(v_i)=\beta(v_i)$；对于单个常量，规定$\mathfrak{I}(c_i)=c^{\mathfrak{A}}$；对于函数，归纳地规定$\mathfrak{I}(f(t_1,\cdots,t_n))=$ $f^\mathfrak{A}(\mathfrak{I}(t_1),\cdots,\mathfrak{I}(t_n))$。

对于formula，我们引入符号$\models$，$\mathfrak{I} \models \varphi$表示在$\mathfrak{I}$这一解释下$\varphi$是真命题。对于等号，规定$\mathfrak{I}\models t_1\equiv t_2$当且仅当$\mathfrak{I}(t_1)=\mathfrak{I}(t_2)$；对于关系符号，规定$\mathfrak{I}\models R(t_1,\cdots,t_n)$当且仅当$R^\mathfrak{A}(\mathfrak{I}(t_1),\cdots,\mathfrak{I}(t_n))$成立；对于非，归纳地规定$\mathfrak{I} \models \neg \varphi$当且仅当$\mathfrak{I}\models \varphi$不成立，记为$\mathfrak{I} \not\models \varphi$；对于与，归纳地规定$\mathfrak{I} \models \varphi\land \psi$当且仅当$\mathfrak{I}\models \varphi$成立且$\mathfrak{I}\models \psi$成立；对于或，归纳地规定$\mathfrak{I} \models \varphi\or \psi$当且仅当$\mathfrak{I}\models \varphi$成立或$\mathfrak{I}\models \psi$成立；对于推出，归纳地规定$\mathfrak{I} \models \varphi\to \psi$当且仅当$\mathfrak{I}\models \varphi$成立能推出$\mathfrak{I}\models \psi$成立；对于等价，归纳地规定$\mathfrak{I} \models \varphi\leftrightarrow \psi$当且仅当$\mathfrak{I}\models \varphi$成立等价于$\mathfrak{I}\models \psi$成立。存在量词的情况比较复杂，我们想直观上这样定义：$\mathfrak{I} \models\exists x \varphi$的含义是存在一个universe $\mathcal{A}$中的元素$a$，把$\varphi$中的$x$都用$a$代入以后成立。为此我们引入记号$\mathfrak{I}\dfrac{a}{x}$，表示在$\mathfrak{I}$的assignment中强制规定$\beta(x)=a$。所以我们定义$\mathfrak{I} \models \exists x\varphi$当且仅当存在$a \in \mathcal{A}$使得$\mathfrak{I}\dfrac{a}{x}\models \varphi$；定义$\mathfrak{I} \models \forall x\varphi$当且仅当对于所有的$a \in \mathcal{A}$都有$\mathfrak{I}\dfrac{a}{x}\models \varphi$。

对于$\models$符号，我们额外规定formula集合的情况。对于formula集合$\Phi$，如果对于所有的$\varphi \in \Phi$都有$\mathfrak{I}\models \varphi$，就简记为$\mathfrak{I} \models \Phi$。如果对于任何的$\mathfrak{I}$，只要$\mathfrak{I} \models \Phi_1$就有$\mathfrak{I} \models \Phi_2$，就简记为$\Phi_1 \models \Phi_2$。如果对于任何的$\mathfrak{I}$都成立$\mathfrak{I} \models \varphi$，就简记为$\models \varphi$。如果存在$\mathfrak{I}$使得$\mathfrak{I} \models \varphi$，就称$\varphi$是satisfiable的（可满足的）。

语义等价

对于两个命题$\varphi,\psi$，如果$\varphi \models \psi$和$\psi \models \varphi$都成立，就称它们是逻辑等价的。逻辑等价意味着它们在语义上的成立是当且仅当的。通过冗长但并不复杂的结构归纳（Homework3），我们发现$\varphi \land \psi$等价于$\neg(\neg\varphi \or \neg\psi)$（我们熟知的De Morgan's Law）；$\varphi\to\psi$等价于$\neg \varphi \or \psi$（前者成立时后者成立，或者前者不成立，综合起来就是前者不成立或者后者成立）；$\varphi \leftrightarrow \psi$等价于$\neg(\varphi\or \psi)\or \neg(\neg \varphi \or \neg\psi)$（同时成立或同时不成立）；$\forall x \varphi$等价于$\neg \exists x\neg \varphi$（对任意成立，等价与存在一个不成立的否定）。通过等价变换我们发现逻辑符号中，$\and,\forall,\to,\leftrightarrow$本质上是可以被抛弃的，因此我们只需要$\neg,\or,\exists$这三个符号就够了。在今后的关于语义的结构归纳中，也只需要对这三个符号做归纳。

现在我们想知道对于两个interpretation $\mathfrak{I}_1,\mathfrak{I}_2$，什么时候它们对一个term $t$的解释是相同的（$\mathfrak{I}_1(t)=\mathfrak{I}_2(t)$）？容易发现，如果$\mathfrak{I}_1$和$\mathfrak{I}_2$对每个变量都有相同的解释，对每个常量有相同的解释，对每个函数符号也有相同的解释， 那么就一定满足$\mathfrak{I}_1(t)=\mathfrak{I}_2(t)$。同样的，什么时候它们对一个formula $\varphi$的解释是相同的（$\mathfrak{I}_1\models \varphi \iff \mathfrak{I}_2\models \varphi$）？归纳地，我们发现我们只要对每个变量、常量以及关系符号有相同的解释就可以保证这一点。但对于formula的情形，我们还必须考虑自由变元的问题，这里我们发现formula的情形我们并不关系不自由的变元上的解释（理应如此），因此只需要求对所有自由变元有相同的解释。我们可以把以上两点总结成一条定理，称为The Coincidence Lemma：如果$\mathfrak{I}_1$和$\mathfrak{I}_2$有相同的universe $\mathcal{A}$，在共同的符号集上对符号都有相同的解释，那么如果$\mathfrak{I}_1$、$\mathfrak{I}_2$在所有$t$的变量上有相同解释就成立$\mathfrak{I}_1(t)=\mathfrak{I}_2(t)$，如果$\mathfrak{I}_1$、$\mathfrak{I}_2$在$\varphi$的所有自由变元上有相同解释就成立$\mathfrak{I}_1\models \varphi \iff \mathfrak{I}_2 \models \varphi$。

The Coincidence Lemma描述了interpretation对term和formula等价的条件，它的核心条件是两个interpretation对自由变元有相同的解释。现在考虑sentence的等价条件，这样我们就可以抛弃所有对自由变元的解释，也即可以不考虑assignment而回退到structure的情形了。对于sentence $\varphi$，如果两个structure $\mathfrak{A},\mathfrak{B}$是isomorphic（同构的），那么成立$\mathfrak{A} \models\varphi \iff \mathfrak{B}\models \varphi$，这称为The Isomorphism Lemma。其中，isomorphism定义为，对于$\mathfrak{A}$和$\mathfrak{B}$，在universe上存在一个$\mathcal{A}\to\mathcal{B}$的双射$\pi$，并且满足$(a_1,\cdots,a_n)\in R^\mathfrak{A}$ $\iff (\pi(a_1),\cdots,\pi(a_n))$ $\in R^\mathfrak{B}$（映射前后关系符号在各自的解释下的成立是当且仅当的），$\pi(f^\mathfrak{A}(a_1,\cdots,a_n))=f^\mathfrak{B}(\pi(a_1),\cdots,\pi(a_n))$（函数符号映射后相等），$\pi(c^\mathfrak{A})=c^\mathfrak{B}$（对常数解释相等）。（容易证明isomorphism关系是一种等价关系，也即满足自反、对称、传递三条性质）。

Isomorphism Lemma反向是不对的，不能由$\mathfrak{A} \models\varphi \iff \mathfrak{B}\models \varphi$推出$\mathfrak{A},\mathfrak{B}$是isomorphic的。然而这一点在$S$有限时是正确的，也即$S$有限时Isomorphism Lemma是充分必要的（见Hw4Ex2，需要构造一个能精准刻画structure的sentence。）

Substitution

现在我们要讨论substitution（代入）这一操作。在形式系统中，substitution可以发生在语法上，也可以发生在语义上。语法上的substitution是机械地按照term的formula的结构归纳做字符串上的替换操作，语义上的substitution是对assignment函数$\beta$做修改。下面严格地定义这两种substitution。

首先定义对term的语法替换。如果对于term $t$，我们要在语法上同时代入$x_1=t_1,\cdots,x_r=t_r$，那么把这一操作记为$t\dfrac{t_1,\cdots,t_r}{x_1,\cdots,x_r}$，它归纳地定义为：如果$t$就是单个变量，那么如果它是某个$x_i$那么就直接替换成给定的$t_i$，否则不变；如果它是常量则不变；如果它是函数$f(t_1',\cdots,t_n')$，那么对每个$t_i'$归纳地代换为$t_i'\dfrac{t_1,\cdots,t_2}{x_1,\cdots,x_r}$。

接着定义对formula的语法替换。同样的， 我们把这一操作记为$\varphi\dfrac{t_1,\cdots,t_r}{x_1,\cdots,x_r}$对于等号和关系符号这两种基本情形，直接对每个term做替换$t\dfrac{t_1,\cdots,t_r}{x_1,\cdots,x_r}$；对于$\neg,\and,\or,\to,\leftrightarrow$，对每个formula归纳地替换；对于$\exists x\varphi$，我们只考虑$x_1,\cdots,x_r$中那些在$\exists x\varphi$中作为自由变元的变量（这么规定的直观在于，对非自由的变量替换是没有意义的）， 只对这些归纳地做替换，同时为了考虑到替换后如果在$t_i$中出现$x$，这一变量会存在歧义，此时我们要把$x$替换成一个在$\exists x\varphi$的任何地方都从未出现过的变量（这总是做得到的，因为变量的个数是无穷的）。$\forall$的情形是相同的。

下面定义语义上的替换。如果我们要在某个interpretation $\mathfrak{I}=(\mathfrak{A},\beta)$上把$x_1,\cdots,x_r$替换成universe中的$a_1,\cdots,a_r$，那么我们直接把这一操作修改到$\beta$上，记为$\beta\dfrac{a_1,\cdots,a_r}{x_1,\cdots,x_r}$。对于$\beta\dfrac{a_1,\cdots,a_r}{x_1,\cdots,x_r}(v)$，如果$v=x_i$那么函数值为$a_i$，否则依然返回$\beta(v)$。记$\mathfrak{I}\dfrac{a_1,\cdots,a_r}{x_1,\cdots,x_r}=(\mathfrak{A},\beta\dfrac{a_1,\cdots,a_r}{x_1,\cdots,x_r})$。

重要的问题是，语法上的替换是否等价于语义上的替换？The Substitution Lemma回答了这个问题：对于term $t$，始终成立$\mathfrak{I}(t\dfrac{t_1,\cdots,t_r}{x_1,\cdots,x_r})=$ $\mathfrak{I}\dfrac{\mathfrak{I}(t_1),\cdots,\mathfrak{I}(t_r)}{x_1,\cdots,x_r}(t)$；对于formula $\varphi$，始终成立$\mathfrak{I} \models\varphi\dfrac{t_1,\cdots,t_r}{x_1,\cdots,x_r} \iff$ $\mathfrak{I}\dfrac{\mathfrak{I}(t_1),\cdots,\mathfrak{I}(t_r)}{x_1,\cdots,x_r}\models \varphi$。换言之，对于某个interpretation，我们先在语法上做替换再做解释，与我们先做语义上的解释修改再重新解释，效果是等价的。（证明依据结构归纳）